| Full text | |
| Author(s): |
Cunha, E.
;
Custodio, M.
;
Rocha, H.
;
Barreto, R.
;
IEEE Comp Soc
Total Authors: 5
|
| Document type: | Journal article |
| Source: | 2011 BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEM ENGINEERING (SBESC); v. N/A, p. 7-pg., 2011-01-01. |
| Abstract | |
This paper shows a method for translating UML sequence diagrams to Petri nets and verifying deadlock-freeness, reachability, safety and liveness properties by using a model checker. In this proposed method, the user has not to know about temporal logics to describe the property to be verified. Instead, the user may adopt a high-level properties specification interface, which is automatically translated to a suitable temporal logic. We show the application of the proposed method in an embedded control application that consists of a sensory device mounted on a motorized platform that must detect and track specific objects in the environment. (AU) | |
| FAPESP's process: | 08/57870-9 - Critical Embedded Systems Institute |
| Grantee: | Jose Carlos Maldonado |
| Support Opportunities: | Research Projects - Thematic Grants |