Title :
Temporal logics and model checking algorithms for ZIAs
Author_Institution :
Nat. Key Lab. of Sci. & Technol. on Avionics Syst. Integration, Shanghai, China
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;
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
