Formal Verification of UML Sequence Diagrams in the Embedded Systems Context
Resumo
This paper shows a method for translating UML sequence diagrams to Petri nets and verifying deadlockfreeness, 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.
Referências
L. Amorim R. Barreto P. R. M. Maciel E. Tavares M. O. Jr. A. Bessa and R. M. F. Lima "A methodology for software synthesis of embedded real-time systems based on TPN and LSC " in ICESS 2005 pp. 50-62. (Pubitemid 43846822)
M. DiNatale and J. A. Stankovic "Dynamic end-to-end guarantees in distributed realtime systems " in IEEE Real-Time Systems Symposium 1994 pp. 216-227.
R. Eshuis "Symbolic model checking of uml activity diagrams " ACM Trans. Softw. Eng. Methodol. vol. 15 no. 1 pp. 1-38 January 2006. (Pubitemid 43943431)
J. M. Fernandes S. Tjell J. B. Jorgensen and O. Ribeiro "Designing tool support for translating use cases and uml 2.0 sequence diagrams into a coloured petri net " in International Workshop on Scenarios and State Machines. IEEE 2007 pp. 2-11.
M. D. Jeng and W. Z. Lu "Extension of uml and its conversion to petri nets for semiconductor manufacturing modeling " in IEEE International Conference on Robotics and Automation (ICRA'02) 2002 pp. 3175-3180. (Pubitemid 34916369)
T. Murata "Petri nets: Properties analysis and applications " Proceedings of the IEEE vol. 77 no. 4 pp. 541-580 April 1989.
S. Yao and S. M. Shatz "Consistency checking of uml dynamic models based on petri net techniques " in International Conference on Computing 2006 pp. 289-297.
M. DiNatale and J. A. Stankovic "Dynamic end-to-end guarantees in distributed realtime systems " in IEEE Real-Time Systems Symposium 1994 pp. 216-227.
R. Eshuis "Symbolic model checking of uml activity diagrams " ACM Trans. Softw. Eng. Methodol. vol. 15 no. 1 pp. 1-38 January 2006. (Pubitemid 43943431)
J. M. Fernandes S. Tjell J. B. Jorgensen and O. Ribeiro "Designing tool support for translating use cases and uml 2.0 sequence diagrams into a coloured petri net " in International Workshop on Scenarios and State Machines. IEEE 2007 pp. 2-11.
M. D. Jeng and W. Z. Lu "Extension of uml and its conversion to petri nets for semiconductor manufacturing modeling " in IEEE International Conference on Robotics and Automation (ICRA'02) 2002 pp. 3175-3180. (Pubitemid 34916369)
T. Murata "Petri nets: Properties analysis and applications " Proceedings of the IEEE vol. 77 no. 4 pp. 541-580 April 1989.
S. Yao and S. M. Shatz "Consistency checking of uml dynamic models based on petri net techniques " in International Conference on Computing 2006 pp. 289-297.
Publicado
07/11/2011
Como Citar
CUNHA, E.; CUSTODIO, M.; ROCHA, H.; BARRETO, R..
Formal Verification of UML Sequence Diagrams in the Embedded Systems Context. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SISTEMAS COMPUTACIONAIS (SBESC), 1. , 2011, Florianópolis.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2011
.
p. 39-45.
ISSN 2237-5430.
