DocumentCode
2992243
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
fYear
2000
fDate
2000
Firstpage
189
Lastpage
193
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Principles of Software Evolution, 2000. Proceedings. International Symposium on
Conference_Location
Kanazawa
Print_ISBN
0-7695-0906-1
Type
conf
DOI
10.1109/ISPSE.2000.913238
Filename
913238
Link To Document