| Texto completo | |
| Autor(es): |
Cunha, E.
;
Custodio, M.
;
Rocha, H.
;
Barreto, R.
;
IEEE Comp Soc
Número total de Autores: 5
|
| Tipo de documento: | Artigo Científico |
| Fonte: | 2011 BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEM ENGINEERING (SBESC); v. N/A, p. 7-pg., 2011-01-01. |
| Resumo | |
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) | |
| Processo FAPESP: | 08/57870-9 - Instituto de Sistemas Embarcados Críticos (ISEC) |
| Beneficiário: | Jose Carlos Maldonado |
| Modalidade de apoio: | Auxílio à Pesquisa - Temático |