Formal Technique Of Concurrent Systems

With computer system applying to advanced domain, for improving security and reliability of the system formalization method has progressed quiet great. Many kinds of excellent formalizing tools have boomed, such as B, VDM and Z, together with Petri net, CSP, CCS, TSL, etc. However, all of these tools are based on a single form, only suitable for describing one aspect of a system. Aiming at this situation, people begin to study the characteristics of each tool and then integrate some of them. Thus, integrated formalization has become a important tendency.This paper tries the method of integrating B language and CCS to construct a BCCS hybrid model. That is, with the help of B language, we can not only expand the capability of CCS in data and operating definition, but at the same time keep the capability of CCS in describing concurrent system. Hence, the integrated formalization model can describe and analyze different aspects of a system (structure, control, data and function) as well as different types of system (sequence, concurrent and distribution). In this model, we'll provide a light weight language which can both offer a colorful expression and general syntax for describing the value of CCS and lay a theoretical foundation for describing the behavior-based and model-based requirements in one model. The BCCS model makes up the weakness of traditional single method. In BCCS model, two important facets of the information system get unified. BCCS adopts the thought of hybridizing CCS and B language, using B language to expand the capability of CCS in data and operating definition and using CCS to expand the capability of B in denoting operating semantics and describing subsequent system, and because of introducing module technology of B method the BCCS can specify a large-scale complex system.In conclusion, we can find a more expressive formalization method, which can describe a large-scale complex system from more facets and offer new attempts for the exploitation of formalization.