DocumentCode :
2346960
Title :
Axiomatic Temporal Logic Programs Verification
Author :
Yang, Xiaoxiao ; Duan, Zhenhua
Author_Institution :
ISN Lab., Xidian Univ., Xi´´an, China
fYear :
2010
fDate :
25-27 Aug. 2010
Firstpage :
87
Lastpage :
94
Abstract :
In this paper, we investigate the axiomatic system of Modeling Simulation and Verification Language (MSVL). To this end, a set of state axioms and state inference rules is given. They are useful to deduce a program into its normal form. Further, a propositional projection temporal logic is used as assertion language to describe the required property of a program. Moreover, to deduce a program over an interval, a set of rules in terms of triple like Hoare logic is formalized. These rules enable us to deduce a program in its normal form at the current state to the next one and to verify safety, liveness properties over an interval.
Keywords :
formal languages; inference mechanisms; program verification; software engineering; specification languages; temporal logic; Hoare logic; assertion language; axiomatic system; modeling simulation and verification language; prepositional projection temporal logic; program verification; state inference rules; Computational modeling; Laboratories; Logic programming; Semantics; Software; Writing; axiomatic semantics; safety; temporal logic programs; verification;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2010 4th IEEE International Symposium on
Conference_Location :
Taipei
Print_ISBN :
978-1-4244-7847-7
Type :
conf
DOI :
10.1109/TASE.2010.10
Filename :
5587722
Link To Document :
بازگشت