Research On Formal Modeling Of Distributed Systems

Distributed computing has formed various specifications or standards with its rapid progress in recent years, and can be applied to develop distributed software systems. However, these industry specifications or standards obviously lack solid theory foundation, which causes great inconvenience to distributed software system specification, correctness verification and performance evaluation. It is still a hard and complicated job for the developers to develop a large-scale distributed systemCORBA(Common Object Request Broker Architecture,CORE A) is a set of open standards proposed by the OMG in order to promote interoperability between distributed systems, and it is not implementation but only specification. The aim of the formal method is to support the formal simulation and verification of large-scale application systems. Formal methods convert informal specifications into formal description for the purpose that the dynamic behaviors of the modeled systems can be formally described with unambiguous precise definitions, and effective mathematic tools for the specification, design and verification of parallel and distributed system can also be provided. Therefore, the formal method plays an important role as a bridge between the model simulation, verification of application systems. The formal simulation and analysis of the application system can point out the defects in the system designing and help to modify and enhance the system to make it more sound, effective and reasonable.Formal methods have contributed a lot to the distributed system simulation and analysis. Formal methods over the distributed computing theory model are to formalize all the concepts concerning with the distribution and concurrent behaviors so as to define these accurately and avoid the ambiguity. Because of the inherent distributed nature, transmission delay of the network information, heterogeneous of network platforms, it is obvious that developing a distributed system requires a more accurate mathematics model than the traditional concentrated one. It is necessary to use formal methods to analyze and verify the distributed system so as to provide reliable mathematics tools for the explanation, design and verification of the distributed system, such as the correctness and security of the distributed system.At present, formal methods that can be used to describe and verify in the distributed system model are mainly categorized into four types: methods based on models, methods based on logic, methods based on processing calculus, methods based on networks. This paper illustrates the above methods characteristics and defects, and focus on formal modeling of the CORBA distributed system based onThis research is supported by the National Natural Science Foundation of P.R.China and The Research Grants Council of Hong Kong (No. 79910161989)Petri nets. The main contributions of this paper are as follows:(1) This paper introduces an extended Colored Petri net to express the behaviors of individual objects, the concurrency between different objects as well as the intra-object concurrency in the context of CORBA, and gives formal specifications of the CORBA Event Service.(2) For the security of the distributed system, the paper applies the Labeled Colored Petri nets to describe and analyze clearly the subjective responsibility and evidence contained in CORBA security service and provides the non-repudiation model based on CORBA security.(3) The paper simulates and analyzes the ACID transaction of distributed system by using the temporal Petri nets, provides an analysis method for building the transaction processing system based on CORBA. In addition, the paper describes and analyzes some issues concerning the workflow with Timed Petri nets and the notions of work flow nets.