Publications

Integrating formal methods into UML opens up a way to complement UML-based software development with precise semantics, development methodologies, as well as rigorous verification and refinement techniques. In this paper, we present an approach to integrate a formal method to practical component-based model driven development through defining a UML profile that maps the concepts of the formal method as UML stereotypes, and implementing the profile into a CASE tool. Unlike most of the previous works in this vein, which concentrate on verifying the correctness of the models built in the development process, we focus on how the full development process can be driven by applying the refinement rules of the formal method in an incremental and interactive manner. The formal method we adopt in this work is the refinement for Component and Object Systems (rCOS). We demonstrate the development activities in the CASE tool using an example.

Model-driven architecture (MDA) has become a main stream technology for software-intensive system design. The main engineering principle behind it is that the inherent complexity of software development can only be mastered by building, analyzing and manipulating system models. MDA also deals with system complexity by providing component-based design techniques, allowing independent component design, implementation and deployment, and then system integration and reconfiguration based on component interfaces. The model of a system in any stage is an integration of models of different viewpoints. Therefore, for a model-driven method to be applied effectively, it must provide a body of techniques and an integrated suite of tools for model construction, validation, and transformation. This requires a number of modeling notations for the specification of different concerns and viewpoints of the system. These notations should have formally defined syntaxes and a unified theory of semantics. The underlying theory of the method is needed to underpin the development of tools and correct use of tools in software development, as well as to formally verify and reason about properties of systems in mission-critical applications. The modeling notations, techniques, and tools must be designed so that they can be used seamlessly in supporting development activities and documentation of artifacts in software design processes. This article presents such a method, called the rCOS, focusing on the models of a system at different stages in a software development process, their semantic integration, and how they are constructed, analyzed, transformed, validated, and verified.

 Deadlocks are a common error in programs with lock-based concurrency and are hard to avoid or even to detect. One way for deadlock prevention is to statically analyze the program code to spot sources of potential deadlocks. Often static approaches try to confirm that the lock-taking adheres to a given order, or, better, to infer that such an order exists. Such an order precludes situations of cyclic waiting for each other’s resources, which constitute a deadlock.

In contrast, we do not enforce or infer an explicit order on locks. Instead we use a behavioral type and effect system that, in a first stage, checks the behavior of each thread or process against the declared behavior, which captures potential interaction of the thread with the locks. In a second step on a global level, the state space of the behavior is explored to detect potential deadlocks. We define a notion of deadlock-sensitive simulation to prove the soundness of the abstraction inherent in the behavioral description. Soundness of the effect system is proven by subject reduction, formulated such that it captures deadlock-sensitive simulation.

Delta-oriented programming allows software developers to define software product lines as variations of a common code base, where variations are expressed as so-called program deltas. Monitor-oriented programming (MOP) provides a mechanism to execute functionality based on the program's execution history; this is useful, e.g., for the purpose of runtime verification and for enforcing security policies.

Consider a requirements model with a set of interfaces representing use cases, and a set of system sequence diagrams specifying the scenarios of the interfaces, this paper discusses how to automatically transform such a model into an inial design model by generating a protocol state machine for each interface from its sequence diagrams, and deriving a controller class as an implementation of the interface. The generated model can be severed as the starting point for the detailed object-oriented design. The contracts of the controller class ensure that the behaviour defined by the sequence diagrams is fully complied with through pre/post-conditions. The transformation takes into account the concurrency and critical area of the respective diagrams. We present the design and implementation of the transformation, which is specified using the graphical notation of QVT Relations and integrated into a CASE tool.

Consider an object-oriented model with a class diagram, and a set of object sequence diagrams, each representing the design of object interactions for a use case. This article discusses how such an OO design model can be automatically transformed into a component-based model for the purpose of reusability, maintenance, and more importantly, distributed and independent deployment. We present the design and implementation of a tool that transforms an object-oriented model to a component-based model, which are both formally defined in the rCOS method of model driven design of component-based software, in an interactive, stepwise manner. The transformation is designed using QVT Relations and implemented as part of the rCOS CASE tool.

Health information systems (HIS) are becoming increasingly integrated through network communication technologies. Integration aims at supporting collaborative healthcare workflows (CHWF) for improvement in sharing healthcare information and resources, efficiency of services and patients safety. CHWF are inherently complex, involving interactions among human actors, and (legacy) digital and physical systems. They are mission safety critical, privacy sensitive, and open to changes of requirements and environments. The complexity makes the definition, understanding, analysis, management, and monitoring of CHWF a software engineering challenge. We propose an approach to formal modelling and analysis of CHWF. The main problems that the approach addresses are abstraction and separation of concerns through algebraic manipulation. We use the CSP process algebra for modeling and verifying the dynamic interaction behavior of processes, and discuss the relation between the dynamic model and the static model of healthcare cases and resources. We also follow the idea of UML of some visualized models, but definitions of the syntax and semantics of these graphical models and their relation to the CSP models are left for future work.

This compendium consists of the papers presented at the TTSS’10 workshop for the convenience of the workshop participants.

This compendium consists of the papers presented at the TTSS’10 workshop for the convenience of the workshop participants.

Component-based development allows one to build software from existing components and promises to improve software reuse and reduce costs. For critical applications, the user of a component must ensure that it fits the requirements of the application. To achieve this, testing is a well-suited means when the source code of the components is not available. Robustness testing is a testing methodology to detect the vulnerabilities of a component under unexpected inputs or in a stressful environment. As components may fail differently in different states, we use a state machine based approach to robustness testing. First, a set of paths is generated to cover transitions of the state machine, and it is used by the test cases to bring the component into a specific control state. Second, method calls with invalid inputs are fed to the component in different states to test the robustness. By traversing the paths, the test cases cover more states and transitions compared to stateless API testing. We apply our approach to several components, including open source software, and compare our results with existing approaches.

We extend our previous approach to run-time verification of a single finite path against a formula in next-free Linear-Time Logic (LTL) with free variables and quantification. We discuss the design space of quantification and introduce a binary operator that binds values based on the current state. The binding semantics of propositions containing quantified variables is a pure top-down evaluation. The alternating binding automaton corresponding to a formula is evaluated in a breadth-first manner, allowing us to detect refuted formulae during execution.