Research On The Clock-constraint-based Dyanmic Logic Syatem For Synchronous Systems

Reactive systems like real-time systems and embedded systems are always ‘synchronous',i.e.,the communication between modules is assumed to be simultaneous,and more than one signals can happen at the same time.As the foundation of synchronous programming languages(such as Esterel,Signal,etc),synchronous system model has been widely applied in the modelling of reactive systems,especially embedded systems.With the development of distributed Real-Time Embedded Systems(RTESs)like Internet of Things and Cyber-Physical Systems recent years,the modelling,specification and verification of synchronous systems are becoming more and more important.In synchronous systems,the ‘clock-constraint-based' system specifications have played a crucial role in systems' safety and reliability.The Clock Constraint Specification Language(CCSL)is a formal specification language based on ‘clock' and ‘clock constraint'.It has been widely used in the specification and verification of synchronous systems.Previous verification techniques for CCSL specification are mainly based on model checking.Because of the limitation of model checking,these techniques do not support the verification of infinite-state CCSL(also called ‘unsafe' CCSL)specifications.For systems with large state space,state-explosion is a problem in the model-checking-based verification techniques.Dynamic Logic(DL)is a type of modal logic for describing and reasoning the dynamic behaviour of programs,whose verification technique is mainly based on theorem proving and SMT checking.DL can model system behaviour at an abstract level,and specify/verify system properties with dynamic formulas.Compared with model-checking-based verification techniques,theorem-proving-based verification technique is able to verify infinite-state systems,and avoid the enumeration of state space by its verification methods.This thesis combines CCSL and DL,and proposes a Clock-constraint-based Dynamic Logic(CDL)System,which applies DL in the modelling and verification of synchronous systems.CDL system supports modelling synchronous systems,describing and verifying clock-constraint-based specifications of synchronous systems.It supports the ‘modular'verification method based on theorem proving,which can verify ‘unsafe' CCSL specifications.CDL system provides a modelling/verification framework for synchronous systems based on theorem proving.The main contributions of this thesis are listed as follows:1.We propose a sequential Clock-constraint-based Dynamic Logic(sCDL),define its syntax and semantics,and build its proof system.Based on the First-Order Dynamic Logic(FODL)system,sCDL system is enriched with ‘signal' and ‘CCSL clock relation' and extends the proof system of FODL.sCDL supports modelling the behaviour of sequential synchronous systems,specifying and verifying a type of ‘simple' CCSL clock-constraint relations of sequential synchronous systems.2.By extending sCDL with ‘parallel programs',we propose the Clock-constraintbased Dynamic Logic(CDL),define its syntax and semantics,and build its proof system.Based on sCDL,CDL imports ‘parallel operator' and ‘parallel communication mechanism',and extends the proof system of sCDL.CDL realizes modelling the behaviour of(parallel)synchronous systems,specifying and verifying the clockconstraint-based CCSL specifications of synchronous systems.3.We analyze the soundness and completeness of the sCDL system,and we prove the soundness theorem and the relative completeness theorem of sCDL system.4.Trough two examples of synchronous systems — the Digital Filter System and the Power Window System,we analyze the application of CDL in synchronous systems.We use CDL to model synchronous systems,describe and prove their CCSL specifications.The result shows that our proposed method is reasonable and valid.