2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering (2010)
Aug. 25, 2010 to Aug. 27, 2010
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2010.10
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.
axiomatic semantics, verification, temporal logic programs, safety
X. Yang and Z. Duan, "Axiomatic Temporal Logic Programs Verification," 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE), Taipei, Taiwan, 2010, pp. 87-94.