MBAT 2014 Abstracts

Full Papers
Full Papers
Paper Nr: 2
Title:

The ETSI Test Description Language TDL and its Application
Authors:

Andreas Ulrich, Sylvia Jell, Anjelika Votintseva and Andres Kull
Abstract: The wide-scale introduction of model-based testing techniques in an industrial context faces many obstacles. One of the obstacles is the existing methodology gap between informally described test purposes and formally defined test descriptions used as the starting point for test automation. The provision of an explicit test description becomes increasingly essential when integrating complex, distributed systems and providing support for conformance and interoperability tests of such systems. The upcoming ETSI standard on the Test Definition Language (TDL) covers this gap. It allows describing scenarios on a higher abstraction level than programming or scripting languages. Furthermore, TDL can be used as an intermediate representation of tests generated from other sources, e.g. simulators, test case generators, or logs from previous test runs. TDL is based on a meta-modelling approach that expresses its abstract syntax. Deploying this design approach, individual concrete syntaxes of TDL can be designed for different application domains. The paper provides an overview of TDL and discusses its application on a use case from the rail domain.
Download
Paper Nr: 3
Title:

Towards a Method for Combined Model-based Testing and Analysis
Authors:

Brian Nielsen
Abstract: Efficient and effective verification and validation of complex embedded systems is challenging, and requires the use of various tools and techniques, such as model-based testing and analysis. The aim of this paper is to devise an overall \method{} for how analysis and testing may be used in combination to increase the quality of embedded systems, and reduce development cost. The method is centered on a common verification planning and iteratively exploiting the established results to strengthen the verification activities. We conclude that the proposed method is general enough to capture most interesting combinations and workflows, but also that formulation of more specific combination patterns will be useful to encourage future tool collaborations.
Download
Paper Nr: 4
Title:

Integrating Model-based Formal Timing Analysis in the Industrial Development Process of Satellite On-Board Software
Authors:

Rafik Henia, Laurent Rioux, Nicolas Sordon, Gerald-Emmanuel Garcia and Marco Panunzio
Abstract: As a consequence of the increasing complexity of modern real-time applications, the need for an efficient, reliable and automated performance estimation method throughout the whole development cycle becomes essential. Model-based formal timing analysis appears at first sight to be the adequate candidate for this purpose. However, its use in the industry is conditioned by a smooth and seamless integration in the development process. This is not an easy task due to the semantic mismatches between the design and timing analysis models but also due to the missing links to the testing phase after code implementation. In this paper, we present a model-based timing analysis framework we developed in the industrial context of satellite on-board software. The framework enables overcoming the above mentioned problems, thus allowing a fully integration and automation of model-based timing verification activities in the development process, as a mean to shorten the design time and reduce risks of timing failures.
Download
Paper Nr: 5
Title:

Formal Test-Driven Development with Verified Test Cases
Authors:

Bernhard K. Aichernig, Florian Lorber and Stefan Tiran
Abstract: In this paper we propose the combination of several techniques into an agile formal development process: model-based testing, formal models, refinement of models, model checking, and test-driven development. The motivation is a smooth integration of formal techniques into an existing development cycle. Formal models are used to generate abstract test cases. These abstract tests are verified against requirement properties by means of model checking. The motivation for verifying the tests and not the model is two-fold: (1) in a typical safety-certification process the test cases are essential, not the models, (2) many common modelling tools do not provide a model checker. We refine the models, check refinement, and generate additional test cases capturing the newly added details. The final refinement step from a model to code is done with classical test-driven development. Hence, a developer implements one generated and formally verified test case after another, until all tests pass. The process is scalable to actual needs. Emphasis can be shifted between formal refinement of models and test-driven development. A car alarm system serves as a demonstrating case-study. We use Back’s Action Systems as modelling language and mutation analysis for test case generation. We define refinement as input-output conformance (ioco). Model checking is done with the CADP toolbox.
Download
Paper Nr: 6
Title:

Combining Test and Proof in MBAT - An Aerospace Case Study
Authors:

Michael Dierkes
Abstract: In the aerospace industry, it has become possible to use formal analysis results as certification evidence thanks to the new version of the standard DO-178C and its formal methods supplement DO-333. Furthermore, formal proof has a high potential of cost reduction. On the other hand, it is not possible to replace testing completely by formal analysis, because the latter only considers more or less abstract models of the system under analysis, and can fail due to a too high complexity. But since certain verification tasks can be carried out by formal analysis with an advantage compared to testing, the question arises how both techniques, i.e. proof and test, can be combined in the best way. The European project MBAT gives answers to this question, and in this article we show how the combined approach has been applied to a relevant use case from Rockwell Collins.
Download
Paper Nr: 7
Title:

Creating a Reference Technology Platform - Performing Model-based Safety Analysis in a Heterogeneous Development Environment
Authors:

Omar Kacimi, Christian Ellen, Markus Oertel and Daniel Sojka
Abstract: The interoperability of tools and methods is a topic being currently discussed across all engineering domains of embedded systems. The increasing amount of requirements on interoperability demands a common understanding of design artifacts which needs to be accessible beyond tool boundaries. Furthermore, to support safety related development, a framework to integrate verification and validation activities has to be established. This eases early design decisions and provides support for certification processes. Different European projects tackled the subject and current ones like MBAT (Model-Based Analysis and testing) are addressing it under the form of a so called Reference Technology Platform (RTP). Nevertheless, besides theoretical discussions on interoperability standards and basic transfer technologies, few implementations of such a platform exist. Within MBAT, we integrated an automated safety analysis into our existing RTP prototype. This setup was developed for the purposes of an industrial case study calling upon a typical set of heterogeneous tools and formats like MATLAB Simulink/Stateflow, IBM Rational DOORS and EAST-ADL. In this paper, we present our RTP implementation and evaluate its effectiveness with respect to the safety aspects and the interoperability challenges raised by the use case.
Download