This paper proposes an approach to verify SysML models consistency and to validate the transformation of SysML models to VHDL-AMS code. This approach is based on two main solutions: the use of model-to-model transformation to verify SysML models consistency and writing unit tests to validate model transformations. The translation of SysML models into VHDL-AMS simulable code uses MMT (Model to Model Transformation) ATL Atlas Transformation Language and M2T (Model To Text) Acceleo tooling. The test validation of the model transformations is performed using EUNIT framework.

This paper proposes a new family of model-based coverage criteria, based on formalizing boundary-value testing heuristics. The new criteria form a hierarchy of data-oriented coverage criteria, and can be applied to any formal notation that uses variables and values. They can be used either to measure the coverage of an existing test set, or to generate tests from a formal model. We give algorithms that can be used to generate tests that satisfy the criteria. These algorithms and criteria have been incorporated into the BZ-TESTING-TOOLS (BZ-TT) tool-set for automated test case generation from B, Z and UML/OCL specifications, and have been used and validated on several industrial applications in the domain of critical software, particularly smart cards and transport systems.

Abstract This paper presents the results of a case study on generating test cases for a fragment of the smart card GSM 11‐11 standard. The generation method is based on an original approach using the B notation and techniques of constraint logic programming with sets. The GSM 11‐11 technical specifications were formalized with the B notation. From this B specification, a system of constraints was derived, equivalent to this formal model. Using a set constraint solver, boundary states were computed and test cases were obtained by traversing the constrained reachability graph of the specifications. The purpose of this project was to evaluate the contribution of this testing environment, called B‐TESTING‐TOOLS, in an industrial process on a real life‐size application, by comparing the generated test sequences with the already used and high‐quality manually‐designed tests. This comparison enabled us to validate our approach and showed its effectiveness in the validation process of critical applications: the case study gives a wide coverage (about 85%) of the generated tests compared to the pre‐existing tests and a saving of 30% in test design time. Copyright © 2004 John Wiley & Sons, Ltd.

Abstract BZ‐Testing‐Tools (BZ‐TT) is a tool‐set for automated model‐based test case generation from B abstract machines and Z specifications. BZ‐TT uses boundary testing as well as cause–effect testing on the basis of the formal model. It has been used and validated on several industrial case studies in the domain of critical software: in particular for smart card applications and automotive embedded systems. The main idea of BZ‐TT is to compute a boundary goal for each effect of the operations of the model and then to compute a preamble sequence of operations to place the system under test in such a state that satisfies the goal. In this paper, the preamble computation search strategies used in BZ‐TT are presented. More precisely, two algorithms based respectively on forward chaining and backward chaining are compared. These algorithms both use a customized set constraint solver, which is able to animate the formal model. These algorithms differ, however, in their capacity to reach the boundary goals efficiently. The results of applying the tools to an industrial windscreen wiper controller application are presented. Copyright © 2004 John Wiley & Sons, Ltd.

Abstract BZ‐TESTING‐TOOLS (BZ‐TT) is a tool set for automated test case generation from B and Z specifications. BZ‐TT uses boundary and cause–effect testing on the basis of the formal model. It has been used and validated on several industrial applications in the domain of critical software, particularly smart card and transport systems. This paper presents the test coverage criteria supported by BZ‐TT. On the one hand, these correspond to various classical structural coverage criteria, but specialized to the case of B abstract machines. The paper gives algorithms for these in Prolog. On the other hand, BZ‐TT introduces new coverage criteria for complex data structures, based on boundary analysis: this paper defines weak and strong state‐boundary coverage, input‐boundary coverage and output‐boundary coverage. Finally, the paper describes how BZ‐TT presents a unified view of these criteria to the validation engineer, and allows him or her to control the test case explosion on a coarse basis (choosing from a range of coverage criteria) as well as a fine basis (selecting options for each state or input variable). Copyright © 2004 John Wiley & Sons, Ltd.

The paper presents an original method to generate test sequences. From formal specifications of the system to be tested, an equivalent system of constraints is derived, and then the domain of each state variable of this system is partitioned into subdomains. Using this partition, limit states are computed with a specific solver that uses constraint logic programming with sets. This specific solver is then used to build test sequences by traversing the constrained reachability graph of the specifications. Finally, the formal specifications are used as an oracle by using them to determine the expected output for a given input. The results of an industrial case-study of the Smart Card GSM 11-11 standard are presented and discussed.