High testability is a strongly desired feature of software, since it tends to make the validation phase more efficient in exposing faults during testing, and consequently it increases the quality of the end-product. Furthermore, testability is a criterion of crucial importance to software developers, since the sooner it can be estimated, the better the software architecture will be organized to improve subsequent maintenance. This paper is concerned with the testability of data flow software designs, its definition, and the axiomatization of its expected behavior. This behavior is expressed in relation to basic operations that are applicable on designs, and to the dedicated test strategies which are selected. Measurements are proposed which are consistent with the stated axioms. The whole approach is demonstrated using design specifications of embedded software developed in the avionics industry.

Several studies have shown that automated testing is a promising approach to save significant amounts of time and money in the industry of reactive software.But automated testing requires a formal framework and adequate means to generate test data.In the context of synchronous reactive software, we have built such a framework and its associated tool -Lutess-to integrate various well-founded testing techniques.This tool automatically constructs test harnesses for fully automated test data generation and verdict return.The generation conforms to different formal descriptions: software environment constraints, functional and safety-oriented properties to be satisfied by the software, software operational profiles and software behavior patterns.These descriptions are expressed in an extended executable temporal logic.They correspond to more and more complex test objectives raised by the first pre-industrial applications of Lutess.This paper concentrates on the latest development of the tool and its use in the validation of standard feature specifications in telephone systems.The four testing techniques which are coordinated in Lutess uniform framework are shown to be well-suited to efficient software testing.The lessons learnt from the use of Lutess in the context of industrial partnerships are discussed.

Lutess is a tool that we developed for testing reactive synchronous software and which is being used in different industrial contexts. It offers several formal testing methods with automatic generation of test data from the environment specification. Lutess provides also an approach to assign a probability to the next event issued by the environment. However, a Lutess' user faces the problem of expressing operational profiles with sophisticated and varying probability assignments to software inputs, in a format directly usable by Lutess. The paper concentrates on how to express operational profiles for specifications which are implemented as binary decision diagrams.

This paper is concerned with diagnosability, its definition and the axiomatization of its expected behaviour. The intuitive expected behaviour of diagnosability is defined relative to basic operations that are applicable on software designs. A diagnosability measurement is proposed which is consistent with the stated axioms. The diagnosability metric is based on an analysis of the design structure: fault location effort and precision are measured for a given testing context. Compromises between global test difficulty and diagnostic precision are illustrated on part of a data-flow software design. Throughout the paper, we develop a case study.

Synchronous programming makes the implementation of reactive software easier and safer. Automatic formal verification methods based on model-checking have been developed within the synchronous approach to prove the satisfaction by the software of safety properties. But these methods often require huge memory or time amounts. As a solution to that problem we propose a set of formally defined testing techniques allowing for automatic test data generation. These techniques can be used independently or as a complement to formal verification, since they need the same set of specifications.

We describe a uniform approach to specify operational profiles for synchronous reactive software and to automatically generate random software inputs according to these profiles. The approach is general enough to allow realistic description of the operating environment: as the environment behavior is often characterized by properties expressing causal temporal dependencies, the operational profile specification technique gives a means to assign to the next event issued by the environment with a probability depending on any sequence of previous events. Two examples of reactive software controlling respectively a temperature control system and an elevator are used to illustrate the technique.

Three approaches to the problem of testing synchronous critical software are presented, based on the data-flow language LUSTRE. The first approach automatically transforms a set of LUSTRE invariant properties characterizing the environment into a constrained random generator of test data sequences. The second approach consists in analyzing the required safety properties (written in LUSTRE) of the software. This analysis may result, in specific cases, in automatic generators of relevant test data. The third approach considers that LUSTRE is used for the implementation of the software. The usual structure-based testing criteria are adapted to the operator net associated with the LUSTRE nodes. Moreover, an automatic test data generation process is described for this last approach using LESAR, a tool designed to automatically prove the satisfaction of safety properties on LUSTRE programs.>