TMSVL Language And Its Applications In Verification Of Real-time Systems

MS VL(Modeling,Simulation and Verification Language)is a temporal logic programming language.It is an executable subset of Projection Temporal Logic(PTL).It is mainly used for formal modeling and verification of concurrent systems and interactive systems.It fails to effectively model time constraints and interruptions in real-time systems as well as specify properties with time constraints.Therefore,the MSVL language is extended and a timed version of it,namely,TMSVL(Timed MSVL)is obtained.An interpreter(model checking tool)for TMSVL is developed.Using TMSVL,modeling,simulation and verification of the schedulability of Rate-Monotonic Scheduling(RMS)algorithm,real-time systems based on ?C/OS-III,artificial intelligence systems based on ROS(Robot Operating Systems)and multi-level interruption systems are realized.This paper focuses on the logic used to define TMSVL,the semantics,tool implementation,and applications of the language.The main work is summarized as follows:First,we extend PTL to define time constraints and forced terminations or timeouts from the following aspects:(I)we add variables T and Ts to PTL to model time,where T represents time,Ts denotes the length of time,and they are ranged over non-negative reals;(2)we define a time constraint to constrain time lengths of formulas;(3)we define a cut operation to express forced terminations or timeouts.Next,we present and prove logic laws of for-mulas that include time constraints and the cut operation in TPTL.The timed extension of PTL,namely TPTL,provides formal(model)semantics for defining a formal language for modeling and verifying real-time systems.Second,we define the extended MSVL language,namely TMSVL,with TPTL to model,simulate,and verify real-time systems.It includes not only all statements in MSVL,but also the clock statement,delay statement,cut statement,timeout statement,and interrupt statement.Next,we prove that all TMSVL programs can be transformed into normal form,and propose an approach to transforming a TMSVL program into its normal form.Further,we study the operational semantics of TMSVL,present the evaluation rules of TMSVL expressions,and the semantic equivalent rules of extended statements.The correctness of the operational semantics is ensured by proving the consistency between the operational semantics and model semantics in TMSVL.With TMSVL,we can model time-constraintbehaviors such as delays,timing responses,task deadlines,forced terminations,timeouts,and interruptions in real-time systems.Third,based on the operational semantics,we develop an interpreter for the TMSVL lan-guage to automate the modeling,simulation and verification processes.The tool is obtained by extending the MSVL interpreter and enabling it to support the lexical analysis,syntax analysis,and state reduction of clock statements,statements with delay and timeout con-straints,cut statements,and interruption statements.It has three work modes:with the modeling mode,an LNFG(Labelled Normal Form Graph)is constructed,which illustrates the state space of a program;with the simulation mode,an execution path of the program is conducted;with the verification mode,we can verify whether the program satisfies a de-sired property.The TMSVL interpreter provides a tool support for model checking real-time systems.Fourth,it is critical and intricate to ensure timeliness of real-time tasks and safety of in-terruption handling.We take classic scheduling algorithm RMS as an example and apply TMSVL language to check the schedulability of task sets scheduled in RMS algorithm.This approach provides a sufficient and necessary condition to check the feasibility of RM-S algorithm.Moreover,it can solve a series of problems for checking schedulability of real-time task sets based on different scheduling policies.In addition,we apply TMSVL to verify the reliability of real-time systems based on ?C/OS-III.Taking real-time systems based on ?C/OS-III as case studies,TMSVL is used to model a real-time system with syn-chronization of multi-tasks and a multi-task real-time system with an interruption,the safety and timeliness properties of these systems are verified successfully.Then,we study how to apply the TMSVL language and its model checking approach to modeling and verifying ROS based artificial intelligence systems.Finally,we study how to formalize a multi-level interruption system with TMSVL.An approach to modeling multi-level interruption sys-tems is proposed based on the interruption statement in TMSVL.The approach provides a formal semantics for multi-level interruption systems,making it possible to perform model checking on such systems.Thus timeliness and safety properties can be formally verified in multi-level interruption systems.