The Community for Technology Leaders
2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering (2010)
Taipei, Taiwan
Aug. 25, 2010 to Aug. 27, 2010
ISBN: 978-0-7695-4148-8
pp: 87-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.
INDEX TERMS
axiomatic semantics, verification, temporal logic programs, safety
CITATION

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.
doi:10.1109/TASE.2010.10
95 ms
(Ver 3.3 (11022016))