Research On Formalization Of CORBA Distribted Systems Security Based On Object Oriented Petri Nets

Distributed computing has formed various specifications or standards withits rapid progress in recent years, and can be applied to develop distributedsoftware systems. However, these industry specifications or standards obviouslylack solid theory foundation, which causes great inconvenience to distributedsoftware system specification, correctness verification and performanceevaluation. It is still a hard and complicated job for the developers to develop alarge-scale distributed system.CORBA(Common Object Request Broker Architecture, CORBA) is a set ofopen standards proposed by the OMG in order to promote interoperabilitybetween distributed systems, and it is not implementation but only specification.The aim of the formal method is to support the formal simulation and verificationof large-scale application systems. Formal methods convert informalspecifications into formal description for the purpose that the dynamic behaviorsof the modeled systems can be formally described with unambiguous precisedefinitions, and efective mathematic tools for the specification, design andverification of parallel and distributed system can also be provided. Therefore, theformal method plays an important role as a bridge between the model simulation,verification of application systems. The formal simulation and analysis of theapplication system can point out the defects in the system designing and help tomodify and enhance the system to make it more sound, effective and reasonable.Formal methods have contributed a lot to the distributed system simulationand analysis. Formal methods over the distributed computing theory model are toformalize al the concepts concerning with the distribution and concurrentbehaviors so as to define these accurately and avoid the ambiguity. Because of theinherent distributed nature, transmission delay of the network information,heterogeneous of network platforms, it is obvious that developing a distributedsystem requires a more accurate mathematics model than the traditionalconcentrated one. It is necessary to use formal methods to analyze and verify thedistributed system so as to provide reliable mathematics tools for the explanation,design and verification of the distributed system, such as the correctness andsecurity of the distributed system.At present, formal methods that can be used to describe and verify in thedistributed system model are mainly categorized into four types: methods basedon models, methods based on logic, methods based on processing calculus,methods based on network.The Petri Net is very suit for descriping the system behavior that has thequalities such as erupting parallely,processing parallely and distribution, it is amodel with not only direct graphic representation but also strict mathematicsdefinition and abundant theory basis, therefore, it is a excellent dynamic statebehavior modeling tool. They can depict the system structure with the help of thealgebra analysis technique, creat the status reachability linear system relationship;They can display the run-time mechanism and analysis the dynamic statusbehavior of the system with the help of the drawing analysis technique of thePetri Net;They can minize the reachable status space of the system and reducethe complications of the system analysis with the help of the induction andanalysis technique of the Petri Net;They can represent and analysis the systemdynamic feature formally with the help of the Petri Net description. With thedevelopment and perfection of the Petri Net, the basic Petri Net model can derivemany expand model system, such as predicate/action Petri Net, Timed PetriNet(TPN), Petri Net with the tape tense logic, Coloured Petri Net(CPN), ObjectOriented Petri Net(OPN), Stochastic Petri Net(SPN), Numerical Petri Net(NPN)and etc. to meet different specification and verification requirement, which hasincreased the simulate and analysis ability of the Petri Net.The complicated system safty problem of the distributed system that arebrought about by the object distribution feature,the information transmission inthe network,the difference structure platform and etc. and such as are importantbut universe. Using the formal method to verify the safety of the distributedsystem is very necessary to realize the safety distributed system. For the safety ofthe distributed system, the existing shortage that based on the general Petri Netmethod mainly is that the system safety feature can't be expressed explicitly,though the high level Petri Net such as coloured Petri Net, can distinguish thedistributed object indivial information with color, with the expression and matchcolor information type on the arc, but to the system safety, as though the colorcan distinguish different distributed object or individual, the track can't beexpressed nicely and the attribute of the resposnsibility, certificate of the masterthat safeness in cludes can't be distinguished and analysed. Therefore, this textleads to go into the concept of the object oriented Petri Net, distinguish andanalysis the inner part operating and interactive operating of the object, trackdown the run time process of the business object clearly, appoint the messageplace of the input/output, put the interactive information into the input/outputplace, and give indenying witness for solving the after disputation.Using the Petri Net as a formal tool, the paper studies the safness of thedistributed system that bases on the CORBA, and comes to the followingconclusions:(1) Giving the systemic, formal Object Oriented Petri Net description rule ofthe Petri Net, describing the relationship of the objective world with abstract andsimple method.(2) Getting the OOPN model and OCN model of each object of system withObject Oriented Petri Net method to carry on modeling to CORBA system, andverifying the reachability, liveness, conservativeness, boundeness and safeness ofthe model with the method of the matrix equation invariant analysis method.(3) Using the Object-Oriented Petri-Nets to describe and analyze clearly thesubjective responsibility and evidence contained in CORBA security service andprovides the non-repudiation model based on CORBA security.