For verification and analysis of software systems in a rigorous way, formal semanticsis an important theoretical foundations and an essential prerequisite. The semantics ofprogramming languages enable us to understand, execute and analyze a software sys-tem. Operational semantics can help us to interpret and execute a language, axiomaticsemantics has great facility in verification, and denotational semantics o?ers a powerfulformalism for semantic specifications.Temporal logic programming is a new paradigm for describing concurrent systems,in which the implementation of systems and property of systems can be specified in onelogic. Though researchers developed interpreters to execute temporal logic programs,and temporal logic and its executed subsets are widely applied to the areas of concurrentprograms verification, however, there has not formalized an integrated formal semanticsfor temporal logic programs, at least for interval temporal logic programming languages.Therefore, we are motivated to investigate the formal semantics of interval temporal logicprogramming language MSVL, including its minimal model, operational and axiomaticsemantics.This thesis first investigates the minimal model semantics of MSVL. Since fram-ing destroys monotonicity, canonical models used to define the semantics of non-framedprograms are no longer appropriate. To deal with this, a minimal model theory is devel-oped, by which the temporal semantics of MSVL programs is captured. The existenceof a minimal model for a given framed program is proved.This thesis then investigates the operational semantics of MSVL. A new configu-ration with intervals for MSVL programs is defined. The evaluation rules for both thearithmetic and boolean expressions with temporal operators are defined. The semanticequivalence rules for the reduction of a program within a state is formalized. Further-more, the transition rules within a state and transition rules over an interval betweenconfigurations are also specified. Thus, the executable behavior of framed programs canbe captured in an operational way. In addition, the consistency between the operationalsemantics and the minimal model semantics based on model theory is proved in detail.Based on the operational semantics proposed in this thesis, an interpreter for modeling,simulating and verifying concurrent systems, has been developed.Thirdly, for the purpose of verifying the properties of concurrent programs in aunified notation, This thesis investigates the axiomatic semantics of MSVL. With thismethod, a system is first modeled using MSVL language. Further, a property of the sys- tem is specified by Propositional Projection Temporal Logic (PPTL). Thus, the modeland property of a system are written in the same logic Projection Temporal Logic (PTL).Moreover, a set of state axioms and state inference rules is given to deduce a programinto its normal form, and a set of axioms and inference rules over intervals is formalizedto transform a program from one state to another. In addition, a formal proof of thesoundness and relative completeness of the system with respect to an operational modelof MSVL is given. Finally, an example is given to illustrate how to use the axiomaticsystem to prove a full regular property of programs.
|