Search

The hardware description language Verilog has been standardized and widely used in industry. Multithreaded Discrete Event Simulation Language (MDESL) is a Verilog-like language and it contains a rich variety of interesting features such as the event-driven computation and shared-variable concurrency as well as the realtime feature. In this paper, we present the denotational semantics for MDESL based on UTP. First a discrete time semantic model is proposed to describe the observation-oriented semantics for MDESL. The observations record the change of variables of atomic actions over time. Then the healthy formulae are defined to denote all different behaviors of programs and the semantics of programs is expressed in terms of healthy formulae. In addition, we demonstrate some interesting properties about the MDESL programs expressing as algebraic laws and their proofs are supported by our formalized denotational semantics. Our theoretical approach is complemented by a practical one, we use the theorem proof assistant Coq to formalize the UTP-based semantics for MDESL. The correctness of the algebraic laws is also verified via the mechanical approach in Coq. Our work provides a novel way to verify the correctness of UTP-based semantics forMDESL both in a theoretical approach and in a practical approach. It is also a new attempt for the application of Coq in the mechanized semantics.

Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. It contains interesting features such as event-driven computation and shared-variable concurrency. This article considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. First, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Second, we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, and we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.

The Unified Modeling Language (UML) is an industry standard for modeling analysis and design. However, the semantics of UML is not precisely defined and the correctness of refinement relations cannot be verified. In this study, we use the theorem proof assistant Coq to formalize and mechanize the semantics of UML-Statecharts and the refinement relations between models. Based on the mechanized semantics, the desired properties of both the semantics and the refinement relations can be described and proven as predicates and lemmas. This approach provides a promising way to obtain certified fault-free modeling and refinement.

Model Driven Engineering (MDE) uses models to represent the core part of the software systems. The Unified Model Language (UML) is a widely accepted standard for modeling software systems. Although UML provides numbers of concepts and diagrams to describe the system, there is still an unsolved problem that the semantics and refinement relations of models are not formally defined. In this paper, we apply the constructive type theory to formalize the class diagrams and object diagrams. A suitable subset of UML static models is identified and formally defined. The theorem assistant Coq is applied to encode the semantics of class diagrams. Moreover the refinement relations are also formalized in Coq. The whole approach is supported by tools that do not constrain the semantic definition's expressiveness and flexibility while making it machine-checkable. Our approach offers a novel way for giving a precise foundation in UML and contributes to the goal of improving the overall trustworthy software systems by combining theoretical and practical techniques.

The formal specification of design patterns is central to pattern research and is the foundation of solving various pattern-related problems. In this paper, we propose a metamodeling approach for pattern specification, in which a pattern is modeled as a meta-level class and its participants are meta-level references. Instead of defining a new metamodel, we reuse the Unified Modeling Language (UML) metamodel and incorporate the concepts of Variable and Set into our approach, which are unavailable in the UML but essential for pattern specification. Our approach provides straightforward solutions for pattern-related problems, such as pattern instantiation, evolution, and implementation. By integrating the solutions into a single framework, we can construct a pattern management system, in which patterns can be instantiated, evolved, and implemented in a correct and manageable way.

Performance and reliability are becoming more important in system design draft. Traditional testing and simulation techniques often reach their limits when utilized for the simple reason that they only provide approximate results. This paper addresses performance and reliability analysis problems from quantitative perspective and considers a sensor cluster as a case study. This paper employs probabilistic model checking technique and presents CTMC model of the cluster. Probabilistic model checker PRISM is utilized in the experiment.

Model-based engineering has emerged as a key set of technologies to engineer software systems. While system source code is expected to match with the designed model, legacy systems and workarounds during deployment would undoubtedly change the source code, making the actual running implementation mismatch with its model. Such mismatch poses a challenge of maintaining the conformance between the model and the corresponding implementation. Prior techniques, such as model checking and model-based testing, simply assumed the sole correctness of the model or the implementation, which is naive since they both could contain correct information (e.g. representing either the software requirements or the actual running environment).In this paper, we aim to address this problem through model-based continuous verification (ConV), an iterative verification process that links the traditional model checking phase with the software testing phase to a feedback loop, ensuring the conformance between the system model and its implementation. It allows to execute the abstract test cases over the implementation through a semi-automatic binding mechanism to guide the update of the code, and augments system properties from the actually running system to guide the update of the model through model checking. Based on these techniques, we implemented Eunomia, a conformance verification system, to support the continuous verification process. Experiments show that Eunomia can effectively detect and locate inconsistencies both in the model and the source code.

The UML is a semiformal modeling language which only has syntax and static semantics precisely defined. The dynamic semantics for the UML is specified neither formally nor algorithmically. When using UML at the design phrase, there does not exist a systematic way that allows the model designer to specify its formal semantics and automatically verify correctness properties of the described model. The UML sequence diagrams are widely used to describe the behaviors of software. Reasoning about properties of sequence diagrams at the analysis and design phrase may reveal software faults before software implementation. We propose to use the theorem proof assistant—Coq to verify syntax and semantics constrains of sequence diagrams. The verification and proof process are useful for improving the correctness of sequence diagrams and hence increases the software quality.

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.

If software architecture is assigned with formal semantics, then automatic verification and validation can be performed during the process of model refinement. In this paper, we emphasized on the formal semantics of UML state diagrams oriented performance analysis. The exact definitions of the basic elements and composition mechanism of UML state diagrams are proposed, UML state diagrams is abstracted as a multi-tuple, CTMC models are abstracted as stochastic Kripke structure, mapping rules between the above two mathematics models are proposed, furthermore the corresponding formal semantics are generated. Finally, an asynchronous parallel composition queuing network is presented to illustrate how the theory is applied to formalize UML state diagrams. The key properties of system are manually deduced and validated. The results are analyzed and compared with the automatic executing results through model checker, which validated the practicability and validity of the theory.

If probabilistic model checking is applied in software architecture, function validation and quantitative analysis for Markov process based real-time model can be automatically performed in model refinement, which will improve software quality. In this paper, the exact definitions and mapping rules between UML state diagrams and probabilistic Kripke structure semantics are proposed, as well as the general translation algorithm of formal semantics. An asynchronous parallel composited DTMC system is illustrated, the key non-function properties of system are described by PCTL, which is automatically validated and analyzed by PRISM model checker. The key system properties are also manually deduced and proved, and compared with the experiment results. The mapping rules we proposed are bi-direction, so it can be used in both forward and reverse software engineering.

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.

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.

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.