DocumentCode :
2806017
Title :
Formal Verification of UML Sequence Diagrams in the Embedded Systems Context
Author :
Cunha, E. ; Custódio, M. ; Rocha, H. ; Barreto, R.
Author_Institution :
Depto de Cienc. da Comput., Univ. Fed. do Amazonas (UFAM), Manaus, Brazil
fYear :
2011
fDate :
7-11 Nov. 2011
Firstpage :
39
Lastpage :
45
Abstract :
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.
Keywords :
Petri nets; Unified Modeling Language; embedded systems; formal verification; reachability analysis; temporal logic; Petri nets; UML sequence diagrams; deadlockfreeness verification; embedded control application; embedded systems context; formal verification; high-level properties specification interface; liveness properties; model checker; motorized platform; reachability; safety; sensory device; temporal logic; Computational modeling; Mathematical model; Petri nets; Process control; Program processors; Synchronization; Unified modeling language; Petri nets; SMV; UML sequence diagrams; model-checker; properties verification;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computing System Engineering (SBESC), 2011 Brazilian Symposium on
Conference_Location :
Florianopolis
Print_ISBN :
978-1-4673-0427-6
Type :
conf
DOI :
10.1109/SBESC.2011.18
Filename :
6114883
Link To Document :
بازگشت