Title :
Abstract model checking and refinement of temporal logic in αSPIN
Author :
Gallardo, Maria Del Mar ; Martínez, Jesus ; Merino, Pedro ; Pimentel, Ernesto
Author_Institution :
Comput. Sci. Dept., Malaga Univ., Spain
Abstract :
We give an overview of the features offered by the tool αSPIN in order to perform abstract model checking of LTL formulas. Shortly, these features are: construction of over-approximated PROMELA models, checking satisfaction of universal formulas, checking refutation of existential formulas, and on-the-fly refinement of the model by means of a refinement of the temporal formula to be verified.
Keywords :
formal verification; refinement calculus; temporal logic; αSPIN; LTL formula; PROMELA model; abstract model checking; on-the-fly refinement; temporal logic; Automata; Chromium; Concrete; Explosions; Logic;
Conference_Titel :
Application of Concurrency to System Design, 2003. Proceedings. Third International Conference on
Print_ISBN :
0-7695-1887-7
DOI :
10.1109/CSD.2003.1207725
