DocumentCode
525738
Title
Temporal logics and model checking algorithms for ZIAs
Author
Cao, Zining
Author_Institution
Nat. Key Lab. of Sci. & Technol. on Avionics Syst. Integration, Shanghai, China
fYear
2010
fDate
23-25 June 2010
Firstpage
57
Lastpage
62
Abstract
In this paper, we first propose a specification approach combining interface automata and Z language. This approach can be used to describe temporal properties and data properties of software components. A branching time logic for ZIAs is presented. We then give an algorithm for model checking this logic on ZIAs with finite domain. Furthermore, we present a mu-calculus logic for ZIAs, and give a model checking algorithm for this logic.
Keywords
Aerospace electronics; Automata; Computer interfaces; Computer science; Formal specifications; Laboratories; Logic; Set theory; Software systems; Specification languages; Z notation; interface automata; model checking; temporal logic;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Engineering and Data Mining (SEDM), 2010 2nd International Conference on
Conference_Location
Chengdu, China
Print_ISBN
978-1-4244-7324-3
Electronic_ISBN
978-89-88678-22-0
Type
conf
Filename
5542952
Link To Document