Title :
Verification of reactive system specifications with outer event conditional formula
Author :
Aoshima, Takenobu ; Yonezaki, Naoki
Author_Institution :
Dept. of Comput. Sci., Tokyo Inst. of Technol., Japan
Abstract :
We introduce an efficient tableau-based satisfiability checking procedure for a specification which consists of several modules. This method extracts reduced constraints from each module and verifies a property with them. We also show that this method is applicable to the decision procedure for strong satisfiability and stepwise satisfiability. Finally, we show the experimental results of the method
Keywords :
computability; formal verification; subroutines; temporal logic; decision procedure; formal verification; modules; outer event conditional formula; propositional linear temporal logic; reactive system specifications; reduced constraint extraction; stepwise satisfiability; strong satisfiability; tableau-based satisfiability checking procedure; Computational efficiency; Computer science; Data mining; Formal languages; Information science; Logic; Specification languages;
Conference_Titel :
Principles of Software Evolution, 2000. Proceedings. International Symposium on
Conference_Location :
Kanazawa
Print_ISBN :
0-7695-0906-1
DOI :
10.1109/ISPSE.2000.913238
