Formal Semantics And Verification Of Cyber-Physical Systems With Shared-variable Concurrency

With the increasing interaction between the cyber and the physical,Cyber-Physical Systems（CPS）have emerged.CPS are complex systems that comprise both discrete behaviors of the cyber and continuous behaviors of the physical.Recently,CPS have been widely applied in the fields of industrial control,energy management,intelligent transportation,smart medical care,etc.Related research and applications of CPS have flourished.However,the widespread use of CPS also signals the significance to ensure the security and reliability.Based on mathematics,formal methods can support the de-scription,analysis,modeling and verification of hardware or software systems.Formal methods are now playing an important role in the quality assurance of the safety-critical areas.Therefore,under the guidance of formal methods,this thesis investigates CPS from the perspectives of theory and application.Specifically,the deep combination of the physical and the cyber can cause hardship for the modeling of CPS.Therefore,from the theoretical view,it is vital to provide a language and its unambiguous formal se-mantics.This thesis focuses on CPSL^sc（Cyber-Physical Systems Modeling Language with Shared-Variable Concurrency）which is a modeling language for CPS based on shared variables.For this language,this thesis formalizes message exchange between programs through the trace model.This thesis studies its formal semantics with the help of the Unifying Theories of Programming（UTP）approach,including operational semantics,algebraic semantics,denotational semantics,and proof system.From the ap-plication point of view,with the proposed formal semantics as a theoretical guidance,this thesis carries out translation,simulation and formal verification of CPS in the cor-responding model checkers.The formal semantics presented in this thesis provide the theoretical basis for formal verification.Conversely,the formal verification conducted in this thesis is the application embodiment of formal semantics.In summary,the main contents and contributions of this thesis include:·Theory:Formal semantics of CPS based on the UTP approach（1）Proposes the operational,denotational and algebraic semantics for CPSL^sc.First,to portray the execution steps of the program,this thesis proposes transition rules for CPSL^scbased on the classical structural operational semantics.Then,the algebraic semantics of CPSL^scis explored by introducing the concept of guarded choices.The proposed algebraic semantics indicates that any program of this language can be transformed into the guarded choice form.Also,it implies that a parallel program with continuous behaviors can be sequentialized through these algebraic semantics.Additionally,the denotational semantics of CPSL^scis studied based on the trace model and healthiness condition.（2）Proposes the proof system for CPSL^sc.To avoid the interference caused by shared variables in the parallel composition,this thesis extends classical Hoare triples and introduces the trace model into the proof system.This thesis presents the proof rules of this language,and provides the example of a battery management system for an intuitive demonstration of this proof system’s applicability.·Application:Formal verification of CPS based on model checking （1）Implements the translation and formal verification of CPSL^scbased on operational semantics.Operational semantics is based on the state machine,so the translation from the processes to the automata is implemented in the model checker Space Ex whose theoretical basis is hybrid automata.In addition,this thesis employs an autonomous emergency braking system as a case study to conduct formal verification.（2）Implements the simulation and formal verification of CPSL^scbased on algebraic semantics.Since the algebraic laws in algebraic semantics can be regarded as left-to-right rewrite rules,this thesis formalizes the algebraic semantics in the rewriting engine Real-Time Maude.Then,this thesis con-ducts simulation and formal verification for CPS in Real-Time Maude from the perspective of algebraic semantics.To illustrate the usage of the algebraic semantics and mechanization in Maude intuitively,a case study of a battery management system is presented.