Rewriting-Based Modeling And Verification Of Embedded Systems

Embedded systems are increasingly used in the modern society,becoming embedded in our lives.Due to the importance of their reliability and safety,formal methods for verifying the correctness of embedded systems are in great demand.As the heart of formal verification methods,formal models are the key to their application on embedded systems.Multithreading techniques are deployed in the modern systems,and there exists complicated interaction between embedded systems and their environment.Both will raise new challenges to the formal models about their abilities to model and verify.Recently,rewrite systems have won attention for formal verification,given the facts that they are suitable for modeling the behaviors of multithreads and they support multiple verification techniques such as model checking and theorem proving.To apply rewrite systems on realistic verification projects for embedded systems,we need to answer two questions:(1)How do we capture sequential behaviors via rewrite systems inheriting non-determinism?(2)How do we enhance the usability of rewrite systems to ease the modeling process? To answer these questions,this dissertation introduces a new formal model named normalization conditional rewrite systems.Based on the new model,we develop a methodology for modeling embedded systems and a termination prover CeagleTerm for C programs:1.Aimed at the limitation of rewrite systems for expressing sequential behaviors, his dissertation introduces normalization conditional rewrite systems,which are ble to describe deterministic behaviors.Normalization conditional rewrite sys-tems support user-defined data types and the expressivity for state equivalence and conditional branching.They can also model and distinguish the semantics of non-deterministic behaviors,such as those concurrently in hardware,and of deterministic behaviors,such as those sequentially in software.2.Aimed at the usability of the model,focusing on modeling methodologies,this dis-sertation proposes a methodology which captures the hierarchy,the heterogeneous behaviors,the dynamic structures and the real-timeness of embedded systems.We implement the methodology based on semantics mapping.Then we demonstrate its feasibility for application,by applying it on two realistic embedded systems.3.Aimed at the usability of the model,focusing on the automatic construction of models of embedded software,this dissertation develops an automatic termination prover Ceagle-Term for C programs based on normalization conditional rewrite systems.The tool provides the possibility to prove the total correctness of systems.