Font Size: a A A

Mechanical Verification Of Formal Semantics Based On Theorem Proof Assistant Coq

Posted on:2020-12-26Degree:DoctorType:Dissertation
Country:ChinaCandidate:F ShengFull Text:PDF
GTID:1368330623961079Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
Modern software systems have tremendous impact on society and human lives.However,developing trustworthy hardware and software systems has become a huge challenge.Through mathematically provable specifications,formal methods make it possible for designers to describe,verify and validate systems in a rigorous way.Formal methods are a particular kind of mathematically based techniques for the specification,development and verification of software and hardware systems.One of the interesting researches is applying the interactive theorem assistant into the mechanical definition and verification of software systems.The problems and drawbacks of models can be avoided and the reliability of software systems can be improved through the mechanical verification of the systems' properties in the theorem assistant.The work in this thesis describes the mechanical verification of formal semantics at different levels in the software development.In particular,we explore the idea of using the state-of-the-art theorem proof assistant Coq to perform the mechanical verification both in Multithreaded Discrete Event Simulation Language(MDESL)and Unified Modeling Language(UML).MDESL is a hardware description language,similar to the Verilog.We apply Coq to derive the operational semantics from algebraic semantics.Meanwhile,the soundness and completeness of derived operational semantics is also verified via the mechanical approach in Coq.Besides,the UTP-based denotational semantics of MDESL is formally defined using high-order logic and the correctness of algebraic laws is mechanically verified in Coq.UML is a general-purpose modeling language.We implement the mechanical semantics of class diagrams in Coq.The refinement relations of class diagrams and the consistencies of UML static diagrams are both mechanically depicted in Coq.A machine-checkable UML framework based on Coq is proposed.The main contributions of this thesis can be summarized as follows: We propose the mechanical process deriving the operational semantics from algebraic semantics of MDESL in Coq,and mechanically verify the soundness and completeness of the derived operational semantics.Every program can be expressed as a guarded choice with location status.The derivation strategy is presented based on the guarded choice.The derived transition system that can be regarded as operational semantics is presented as theorems.The inductive types,functions and inductive predicates are used to denote the guarded choice,head normal form and derivation strategy.The soundness and completeness of the derived operational semantics is verified in Coq.We use the mechanical approach to implement the semantic linking that has been proved manually. We present the mechanical definition of the UTP-based denotational semantics of MDESL and the correctness of algebraic laws is mechanically verified in Coq.According to the Unifying Theories of Programming,an observation-oriented denotational semantics can be expressed using the discrete time semantical model and healthy formula.The observation,healthy formula and denotational semantics are presented by inductive predicates and high-order logic in Coq.The correctness of algebraic laws is verified innovatively in Coq,which also reveals the correctness of denotational semantics.The high-order logic proof system effectively reduces the difficulty of proof and promotes the development of UTP theory. We demonstrate how to implement the mechanical semantics of UML static models in Coq,and perform the mechanical verification of the refinement relations of class diagrams and consistencies of static models.First,we use the inductive types to denote the syntax of class diagrams and object diagrams.The well-formed rules and refinement relations of class diagrams are defined as predicates and propositions in Coq.With the help of automatic conversion tool,we propose a machinecheckable UML framework based on Coq.The framework provides a mechanical method for formalizing the semantics of UML models and supports for the mechanical verification of the reliability and correctness of systems,which is a basis of formal verification of Model-Driven Engineering.
Keywords/Search Tags:Mechanized Semantics, Unifying Theoriesof Programming, Multithreaded Discrete Event Simulation Language, Unified Modeling Language, Theorem Proof Assistant Coq
PDF Full Text Request
Related items