Search

A recent trend in the study of UML formal semantics is to integrate semantics of various UML diagrams into a single framework. The aim is to get a unified basis for main research topics like validation, verification and syntax checking. In this paper, we propose an approach based on the Situation Calculus (SC) which is a sophisticated action theory and is capable of modeling general systems. UML models are treated as a tailored SC system, containing eternals, fluents and actions that formalize the frequently used concepts in the UML metamodel. Class diagrams and object diagrams are modeled by eternals for consistency checking. State machine diagrams and sequence diagrams are modeled by fluents and actions, with corresponding precondition axioms and successor state axioms in SC. We use Golog, an executable high-level programming language based on the SC, to analyze and test UML diagrams. Based on the methods proposed in this paper, UML diagrams can be formally analyzed and simulated in the Golog interpreter, which can be useful in discovering system deficits at the design level.

UML Sequence Diagrams are widely used in software development. When putting to applications such as code generation, model simulation and other automated analysis, the formalization of UML Sequence Diagrams, especially correctness of it becomes increasingly important. This article presents the formal specification including denotational semantics and operational semantics of UML Sequence Diagrams. The Coq proof assistant is used to mechanize the semantics and prove the correctness of operational semantics compared to denoational semantics.

An arising interest in the study of UML formal semantics is to integrate UML Diagrams into a uniform semantic model. In this paper, we propose a unified operational semantics for UML based on the Situation Calculus (SC) which is a sophisticated action theory and capable of modeling general dynamic systems. Specifically, UML models are treated as tailored dynamic systems in SC, with vocabularies borrowed from the UML metamodel. Structural diagrams, Class Diagrams and Object Diagrams, are modeled by Eternals for consistency checking. Behavioral diagram, the State Machine Diagram is modeled by Fluents and corresponding Axioms in SC. To analyze and test these dynamic diagrams, we appeal to Golog, an executable high-level programming language based on the SC. By executing Golog programs, UML diagrams can be analyzed and tested under a single semantic model.

Medical Diagnosis System is widely used in health care domain. Nowadays, advent of the era of Medical Diagnosis System means healthcare services at any time and at any places, which leads to advance studying and exploring of Medical Diagnosis Systems based on context-awareness framework. As a typical complex and widely used context aware system, reliable and complete designment of Medical Diagnosis System is espacially important. In this paper, we would analyze the modelling of a Medical Diagnosis System based on context-awareness theory in detail, proposes a new method of modelling, simulation and verification of such system, we would also present a typical illustration of context aware Medical Diagnosis System in this paper.

As a standard modeling language of software architecture design, UML lacks formal semantics on account of its informal graphical notation. To further provide refined description of UML, OCL is primarily and widely employed. Generally, OCL constraints are written manually, which may cause incorrectness and extra overhead. Therefore, generating OCL constraints template for UML models is a superior solution. The OCL constraints template automatically generated can be used as a reference for software designers. First of all, the significance of automatic generation of OCL constraints was emphasized, and then the application domain of OCL was shown, followed by a lexical analysis of how to extract the target objects in UML models where OCL constraints were needed to build and an algorithm of extraction. Eventually, this extraction algorithm was implemented by Perl. In our way, the overall quality and efficiency of software design is enhanced and thus contributions are made for the automation of Software Engineering.

Context aware system (CAS) is a large scale system which senses information and changes of surrounding environment, and adapts its response correspondingly. Recently, CAS is widely investigated and developed both in academy and industry. CAS is notoriously heterogeneous and complex. For this reason, it is especially important to achieve a complete and safe context aware system. Requirements analysis and preliminary design play key role in CAS software development. In this paper, we propose a new method of designing, simulating and verifying of CAS by applying a toolkit named UPPAAL. we will also use an example to expound and prove the feasibility and convenience of the tool UPPAAL for CAS.

The modeling, simulation and verification of real-time systems can be unified and the efficiency of system development can be improved if the UML timing diagram model can be translated into the timed automata model. The conversion rules and the algorithm are given in this paper. A coffee machine control system is given as an example in which we give the UML timing diagram model and translate it to timed automata model in UPPAAL, then we verify the accessibility, the security and the activity of the system by UPPAAL.

In order to solve the problem of trust management in E-marketplace where asymmetric information exists between buyers and sellers, we propose a trade selection algorithm based on game processing in C2C environment in this paper. With the idea of rational expectation of economics, the selection of rational contracting parties is imitated, and a credit-scoring model is presented according to history information about the traders, in which some speculators are removed by trade selection method. In order to make the method more effective, Swarm simulation is carried out, which tracks the trading processes and shows that how it maintain a better rate of elimination at last. The results are distinct in different scale of market, and have the benefit for the optimization of mechanism. The Swarm-based trust model in a large market is also feasible, and the reputation effect in game theory is validated here at the same time.

This article is mainly about how to allocate scarce resources efficiently in network service, to enable network resources meeting the demand as far as possible, and improving the social welfare of user groups. Considering the user's credit and waiting time for allocating resources, we propose a user welfare function and establish a common network resource allocation mechanism which integrates combinatorial auctions algorithm and welfare function. With the experimental data analyzed, the user welfare function based combinatorial auctions mechanism can achieve a high social welfare and acts effectively and stably.

The article is mainly about how to allocate the limited network resources timely and effectively meanwhile improving the overall satisfaction after the allocation. In this paper, a general resource allocation model is established which integrates the typical characteristic of the actual access / supply restricted network resources, considering user credit, waiting time and other factors. The user satisfaction function was designed in the article, and according to this function, the unit satisfaction based allocation mechanism and combinatorial auction based allocation mechanism are also designed. The experiment here is designed to simulate the effects of resources allocation when using different allocation mechanisms. Treating the overall satisfaction from unit-based allocation mechanism as a base of comparison, and considering the satisfaction proportion to analyze the performance of different allocation mechanisms, it is concluded that combinatorial auction based allocation mechanism could get a more effective and stable network resource allocation and achieve a higher overall satisfaction.

System states space based on Kripke structure can be exhausted by model checking, thus system key property described by temporal logic can be automatically verified. Presently model checking has been widely used in hardware validation and network protocol analysis. Sliding window protocol is a classical receive-send protocol, which is used in TCP/IP protocol group. In this paper, we propose the respective formal model of sliding window protocol under three conditions, as well as Kripke structure semantics of the protocol. The key properties of system such as data integrity, liveliness and information consistency are automatically validated. Finally experiment, table and analysis are given out. The method we proposed to analysis specific bit sliding window protocol can be extended to analysis arbitrary bit sliding window protocol.

UML provides a graphical method to model object-oriented system. However, UML is a meta-model which has only static semantics and without dynamic semantics. From the perspective of assembly mechanism, we proposed six kinds of UML state diagram's assembly mechanisms, and gave the mapping rules between assembly mechanism and picalculus. Finally we proved that it is practical to validate model refinement with above theory in two different ways — experiment and theory deduction. The theory deduction coincides with the experiment results. Furthermore, the mobile assembly and interrupt assembly we proposed supplement for the insufficient description ability of UML.

The gap between informal models used in a UML environment and formal verifications and proofs in academic research prevents UML from valid and efficient application. In this paper, we propose an approach to bridge the gap between UML class diagram and situation calculus via our formal verification tool, UCVSC (UML Class diagram online Verification based on Situation Calculus). UML class diagram describes a software system informally while situation calculus is employed as the underlying formalism to precisely specify the system. With respect to most components in UML class diagram, the strength of reasoning about actions and describing the state of the world in situation calculus can be applied to represent them appropriately. Using UML tools and predefined mapping mechanism, we transform UML class diagram to XMI, an intermediate format, and finally to situation calculus in Prolog syntax. This approach attempts to provide precise semantics of UML class diagram which can be logically verified. In addition, we automate the verification process in an online prototype system. Furthermore, a case study on an academic system is presented to illustrate and evaluate our approach.

Pattern-based composition is rather complex and need formal treatments. This paper demonstrates an approach based on logic programming language Golog, whose logical foundations roots in the Situation Calculus. The first step is formalizing design patterns by a set of fluents, actions and corresponding axioms in the Situation Calculus. Based on the formal specification of the underlying patterns, we program their composition in Golog. The program constructs available in Golog provide us with flexible and expressive means for pattern composition. Since the composed specifications in Golog can be regress into the Situation Calculus formulas by Golog interpreter, the properties of underlying patterns can be preserved in their composition. As a case study, we formalize and compose the Mediator pattern and Observer pattern.

VDM-SL is one of the most popular formal language used in software development, its mathematical approach allows unambiguous specification and development of high integrity software. JML is a behavioral interface specification language tailored to Java(TM). And the existing JML-based tools of debugging, verifying and testing are mature. This paper discusses the two kinds of specification language and provides a novel design mapping VDM-SL to JML of constant values, variables and constraints. The strategies of the design are illustrated with an example.

Ad-hoc agent networks are self-organizing societies of agents. Each society of agents is composed of autonomous agents forming an ad-hoc network having no infrastructure. A network community has an interface agent that serves as the certified access point for that network. Communication between two agents within a society requires the cooperation of other agents in the society who will act as intermediaries. This paper proposes an incentive-based mechanism to promote trusted collaboration among agents within a society. Based on this mechanism and through the certified interface agents an agent in one society can securely interact with one or more agents in another society.

As we known, the virtual reality simulation technology of true ocean environment was one of the most important research fields in visual simulation technology. Firstly, the ocean geographic environment information from 2-dimension electronic chart was extracted directly; the information was the data basement of virtual ocean environment visual simulation. Second, on the basis of studied the environment modeling technology and constitution of three dimension ocean environment model systematically, using the 3-D digital map modeling Delaunay algorithm for environment modeling, then the 3-D landform DEM data was translated into the DED file which could serve for the data of 3-D landform modeling. At last, this paper shows the realization of 3-D virtual ocean environment base on true ocean information, which achieved living simulation result, and improve the whole level of view simulation.

Approaches to enforcing communication integrity in the implementation, exemplified by ArchJava, consider only architectural constraints, without taking into account the late integration of prebuilt components into the architecture. This may hinder the practice of architecture in the common component building. In this paper, we present an approach to supporting the integration of prebuilt components in the context of the architectural constraints. This approach is described in terms of a novel design pattern, an architectural description language (ADL) JCMPL and a toolset JCMP. The language and toolset are designed based on the pattern to dynamically link the architectural constraints with the component building. To achieve this goal, an important step is to automatically translate the connector specification defined in the architecture into the connector implementation, which can serve as glue codes to connect two prebuilt components together by transferring the methods invocation between two components.