Research Of UML Dynamic Semantics Based On ASM And π-calculus

With the development of the integrated circuit industry, computer hardware perfor-mance has improved dramatically in the past20years. As a consequence of continuous improvement in hardware and computer applications, users nowadays demand a higher quality software technology. How to improve software quality and enhance development efficiency has become an important research area in the software industry.Since its debut in1990s, Object-Oriented concept has been well-received due to its many advantages, such as visualization, reusable and close to demands. At the same time, software modeling technology was also becoming an important bridge between user needs and the ultimate realization. UML unifies and extends many modeling language, provides rich graphical modeling elements. The advantage of readability makes UML widely used in the early stages of software development. However, the lack of precise semantics results in that is difficult to establish complete, unambiguous models during the analysis, design and implementation stage. And the lack of necessary tools results in that is difficult to refine and verify too.Formal method is based on rigorous mathematical and logical techniques, and suita-ble for the specification, design and verification of software system. The significance of formal method is that it can find the inconsistent, ambiguity and incomplete in the early stage of software development to improve the safety and reliability. The precise seman-tics is helpful to form a consistent understanding of the needs between developers and users, it eliminates the ambiguity and inconsistent in the development process. The auto-matic verification can greatly improve the reliability and efficiency. However, due to the requirements of mathematics and logic knowledge, formal method has limitations in ap-plication, and is difficult to popularity.The ideal software development should be a combination of visual modeling tech-niques and formal methods. In this dissertation, we investigate the dynamic semantics of UML. Under the premise of readability, we add necessary semantic elements to ensure unambiguous and verifiable. The main contributions are as follows:Providing the ASM semantics specification of UML activity diagrams. First we define the static semantics of the activity diagram, including the specification of action nodes (atom nodes), branch nodes, concurrent nodes and active nodes, and generate the ASM activity di-agram specification recursively. Then the dynamic behavior rules are proposed, including the join and fork rule, trigger and capture events rule and so on. In the workflow loop discrimi-nator model, this method more clearly standardizes semantics.Providing the ASM semantics specification of UML state diagram. As an important part of UML dynamic diagrams, the state diagram covers all states during the object’s life cycle. This dissertation gives static semantics of state diagrams to specify the semantics of transi-tions and states. Then extends UML state diagram to the ASM state diagram, and proposes the behavior semantics based on this extended model.Providing the ASM semantics specification of UML sequence diagram. First defines the specification of messages and objects in the sequence diagram. And subsequently, pro-poses rules of message transmission to eliminate the uncertainty of pre-conditions and the unclear timing sequence. Specifying and verifying UML dynamic model of the elevator according to the previous se-mantic specification of the state diagram and the sequence diagram. This method eliminates the deadlock and inconsistencies caused by recursive calls.Providing the incremental refinement of UML dynamic diagram by π-calculus. First gives the π-calculus semantics specification of UML dynamic diagrams, map various ele-ments in the dynamic diagrams to processes and channels of π-calculus. Next, gives the specifications of various dynamic elements, such as the state transition and the message transferring. Finally, by the weak bisimulation relations, defines the equivalence criterion of the sequence and state diagrams. Providing maximum weak bisimulation set and the re-placement rule, and giving a way to verify the incremental consistency of the refinement model, greatly improving the efficiency of verification.