Study On Integration Method Of Modular Modeling And Model Checking For Concurrent Systems

Modern software and hardware systems become more complex, intelligent, and concurrent. With the popularity of concurrent systems, especially in safety-critical areas, the reliability is highly concerned about.The traditional methods are mainly based on testing technology, which is difficult to guarantee the test cases covering all possible execution paths. Model checking has been attracting significant interest due to the completeness and automation. Because the modeling process is usually done by hand, a language to modeling the behavior and functions of concurrent systems is needed. For designing and applying the modeling language, the mainly problems are as follows:(1) How to describe the control flow and data flow of concurrent systems;(2) How to reduce the cost and improve the efficiency of modeling;(3) How to ensure the consistency between the system, model and verification;(4) How to resolve the conflict between the white-box verification and the confidentiality.To solve the above problems, this paper made the following research:? A modeling language MCD is proposed. MCD uses the module as the basic component, defines hierarchical event automaton and function block process to describe the control flow and data flow of systems respectively. The syntax, semantics and formal definition of MCD are given. Based on the syntax and semantics, the system model can be verified and analyzed.? We propose the PROMELA code generation algorithms and optimization strategies. The hierarchical event automata are translated into threads, and the function block processes are translated into inline functions. Blocking and random mechanism is used to realize the synchronization, asynchronization and uncertainty.? We design and develop a modular modeling and model checking tool M3 C. It uses graphical module for modeling, generates the intermediate codes automatically and executes model checking.? We use our methods and M3 C for actual systems of train communication network,and some errors which could lead to dysfunction are found and fixed. It demonstrates the e ff ectiveness of our methods and tools.