Publications

 Ensuring a correct test result from execution of test cases requires more than just writing of a test suite. Testing and Test Control Notation version 3 (TTCN-3) is a standardized test specification and test implementation language. Its architecture has various entities which interact by providing and/or requiring services from each other. We analyze the operations of a TTCN-3 test system and characterize the properties of these operations. We describe the interactions at a system level using sequence diagrams followed by a precise and structural specification of the operations of the TTCN-3 test systems.

 We present a design of a triple modular fault-tolerant system that is a real case we received from our collaborators in the aerospace field. The system is used to compute the action that a subsystem should take and output the result to another subsystem. We model the system as timed automata, where a fault is modelled as an unobservable transition from a "good state" to an "error state". Based on the faults that we were given by the application engineers, we design a system to tolerate the faults and use UPPAAL to check relevant properties. Keywords: Fault-tolerance, real-time embedded systems, abstraction techniques, model checking

 Software development tools need to support more and more phases of the entire development process, because applications must be developed more correctly and efficiently. The tools therefore need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensure high quality of such add-ins is to base them on sound formal foundations. In order to know where such add-ins will fit, we investigate the use of an existing successful commercial tool and identify suitable places for adding formally supported checking, transformation and generation modules. The paper concludes with a discussion of feasibility of developing the proposed add-ins and how to give conditions such that they will actually be used.

 Modern software development has to deal with many different aspects and different views of applications. Thus it needs different modelling notations and tools to support more and more phases of the entire development process. To ensure the correctness of the models produced, the tools need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensuring high quality of such add-ins is to base them on sound formal foundations. This paper summarizes our research on the Refinement of Component and Object Systems (rCOS) and illustrates it with experiences from the work on the Common Component Modelling Example (CoCoME). This gives evidence that the formal techniques developed in rCOS can be integrated into a model-driven development process and shows where it may be integrated in computer-aided software engineering (CASE) tools for adding formally supported checking, transformation and generation facilities. Keywords: Formal methods, multi-view modelling, rCOS, software design process, tool design, UML

Modern software development is complex as it has to deal with many different and yet related aspects of applications. In practical software engineering this is now handled by a UML-like modelling approach in which different aspects are modelled by different notations. Component-based and object-oriented design techniques are found effective in the support of separation of correctness concerns of different aspects. These techniques are practised in a model-driven development process in which models are constructed in each phase of the development. To ensure the correctness of the software system developed, all models constructed in each phase are verifiable. This requires that the modelling notations are formally defined and related in order to have tool support developed for the integration of sophisticated checkers, generators and transformations. This paper summarises our research on the method of Refinement of Component and Object Systems (rCOS) and illustrates it with experiences from the work on the Common Component Modelling Example (CoCoME). This gives evidence that the formal techniques developed in rCOS can be integrated into a model-driven development process and shows where it may be integrated in computer-aided software engineering (CASE) tools for adding formally supported checking, transformation and generation facilities.