Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led i...Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led it to be introduced into the development of approaches and tools to check the correctness of electronic commerce protocols. This paper focuses on the research of a method that connects an extension of AUML to model checker SPIN/Promela for the specification and verification of agent interaction protocols (AIP) in electronic commerce. The method presented here allows us to combine the benefits of visual specification with the power of some static analysis and model checking. Some algorithms and rules are developed to permit all visual modeling constructs translated mechanically into some Promela models of AIP, as supported by the model checker SPIN. Moreover, a process is illustrated to guide the specification and verification of AIP. The method is demonstrated thoroughly using the e commerce protocol NetBill as an example.展开更多
XCD is a design-by-contract based architecture description language that supports modular specifications in terms of components and connectors (i.e., interaction protocols). XCD is supported by a translator that produ...XCD is a design-by-contract based architecture description language that supports modular specifications in terms of components and connectors (i.e., interaction protocols). XCD is supported by a translator that produces formal models in SPIN’s ProMeLa formal verification language, which can then be formally analysed using SPIN’s model checker. XCD is extended with a visual notation set called VXCD. VXCD extends UML’s component diagram and adapts it to XCD’s structure, contractual behaviour, and interaction protocol specifications. Visual VXCD specifications can be translated into textual XCD specifications for formal analysis. To illustrate VXCD, the well-known gas station system is used. The gas system is specified contractually using VXCD’s visual notation set and then formally analysed using SPIN’s model checker for a number of properties including deadlock and race-condition.展开更多
The problem of the description of interaction between agents in a multi-agent system (MAS) in the form of dialogues of negotiations is considered. For formalization of the description of interaction at a level of step...The problem of the description of interaction between agents in a multi-agent system (MAS) in the form of dialogues of negotiations is considered. For formalization of the description of interaction at a level of steps of the dialogue which is carried out in common by two spatially divided agents, the concept of synchronization of processes is analyzed. The approach to formalization of the description of conditions of synchronization when both the independent behaviour, and the communications of agents can be presented at a level of logic is offered. It is shown, that the collective behavior of agents can be described by the synthetic temporal logic that unite linear and branching time temporal logics.展开更多
基金Supported by the Research Grants Council of Hong Kong(DAG99/0 0 .EG0 5 ) the Sino-French Advanced ResearchProgram 2 0 0 0 (PR
文摘Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led it to be introduced into the development of approaches and tools to check the correctness of electronic commerce protocols. This paper focuses on the research of a method that connects an extension of AUML to model checker SPIN/Promela for the specification and verification of agent interaction protocols (AIP) in electronic commerce. The method presented here allows us to combine the benefits of visual specification with the power of some static analysis and model checking. Some algorithms and rules are developed to permit all visual modeling constructs translated mechanically into some Promela models of AIP, as supported by the model checker SPIN. Moreover, a process is illustrated to guide the specification and verification of AIP. The method is demonstrated thoroughly using the e commerce protocol NetBill as an example.
文摘XCD is a design-by-contract based architecture description language that supports modular specifications in terms of components and connectors (i.e., interaction protocols). XCD is supported by a translator that produces formal models in SPIN’s ProMeLa formal verification language, which can then be formally analysed using SPIN’s model checker. XCD is extended with a visual notation set called VXCD. VXCD extends UML’s component diagram and adapts it to XCD’s structure, contractual behaviour, and interaction protocol specifications. Visual VXCD specifications can be translated into textual XCD specifications for formal analysis. To illustrate VXCD, the well-known gas station system is used. The gas system is specified contractually using VXCD’s visual notation set and then formally analysed using SPIN’s model checker for a number of properties including deadlock and race-condition.
文摘The problem of the description of interaction between agents in a multi-agent system (MAS) in the form of dialogues of negotiations is considered. For formalization of the description of interaction at a level of steps of the dialogue which is carried out in common by two spatially divided agents, the concept of synchronization of processes is analyzed. The approach to formalization of the description of conditions of synchronization when both the independent behaviour, and the communications of agents can be presented at a level of logic is offered. It is shown, that the collective behavior of agents can be described by the synthetic temporal logic that unite linear and branching time temporal logics.
