Modeling And Verifying Multithreaded Discrete Event Simulation Lanaguage In PVS

Multithreaded Discrete Event Simulation Language(MDESL in abbreviation) is a Verilog-like language based on UTP. It is proposed by Huibiao Zhu in 2005. MDESL has two interesting features:one is event-driven computation, the other shared-variable concurrency. It not only can program like normal programming language, but also can describe the structure and behavior of hardware accurately. In addition, real-time and parallel composition are two main features of MDESL. Unifying Theories of Program-ming(UTP in abbreviation) is a typical formal method. It mainly discusses denotation semantics, algebraic semantics and operational semantics of programs and verifies the consistency of triple of them. Then a Linking Theory is introduced to describe the rela-tionship between models. UTP also provides a collection of relational models which can be used to describe and compare several programming paradigms.PVS(abbreviation of Prototype Verification System) is a verification system:an ef-ficiently interactive environment for writing formal specifications and a theorem prover. The prominent feature of PVS is its congenerous integration of an expressive specification language and powerful theorem-proving capabilities. The specification language is based on higher-order logic with various of sophisticated types which made it expressive. The theorem prover is highly interactively and automatic. The system can provide mechanical verifying for applying formal methods in computer science.Hand based verifying were used a lot in proving algebraic laws based on denotation semantics. Bi-simulation was usually used for proving operational semantics. Neverthe-less, we analyzed and modeled for MDESL using PVS and proved some of the theorems after acquainted with PVS and UTP. We introduced the syntax and the semantics of the MDESL in detail in chapter 2. Moreover, how to model and prove in PVS are illustrated by an example in four steps——specification, parsing, TCC and proving.We first construct the base environment modeling in chapter 3, then the predicate modeling and last the triple modeling based on higher-order logic in chapter 4. There are five THEORY in our model(Env, Skippre, Command, Tripro, Skip). Fig 3.1 shows the structure of our model pattern and Fig 3.2 shows the relationship between the five theories. We prove most of the theorems in these THEORY using PVS. In chapter 5 some typical ones are explained. Both the model and the denotation semantics are validated. These are not over because we will add the event-driven model, parallel construct and even the linking theory between operational semantics and denotational semantics to our model in the near future. A lot more modeling and validation will be constructed on MDESL using PVS.