Process Calculus With Data Structure And Its Model Checking Algorithm

Formal methods include two parts: one is formal specification, and the other is design verification, it is to describe a software system and its properties which based on mathematics. It can ensure the correctness and reliability, now has become the necessary tools for software and hardware development. As an important automatically formal verification technology, model checking has achieved remarkable success and changed from research to industry production, such as computer hardware, security, authentication protocol, communication protocols, control systems and other field of analysis and verification.The major work done in this paper is as follows:(1) First studied the new process calculation system CCS-Z which combined data structure, and syntax and semantic of it. There are five parts in its syntax, including input action, output action, internal action, CCS part and Z part. Input, output and internal actions mainly depict system behavior, CCS part is used to depict state conversion, and Z part is used to depict the change processes for variables in system. Semantic part mainly gives the operation semantic for five operators in this system. The new system includes Z language and processes calculus system CCS, it can describe the concurrent system and also date structure. Then gave the simulation definition and theorems, which include strong mutual simulation and weak mutual simulation.(2) Then gave the logic which is used to describe system properties, including logic formula and satisfy relations. Logic formula is mainly used to depict system properties, in this paper mainly use calculation tree logic CTL, which ten basic operators, since the other seven operators can described with EX, EU, EG operators, so not use them again. Satisfy relations mainly used to describe whether the system meets its properties, including atomic proposition, negation, conjunction, EX, EU, EG and existential quantification.(3) The last part is about model checking, including the model checking algorithm, class diagram and flow diagram. Class diagram mainly gives the relationship between classes, and flow diagram gives the executive process of algorithm. Then give two examples, one is switch control system and the other is train control system. Switch control system includes switch and switch controller. Train control system includes two trains and traffic control system, which is also given the system information and model checking result.