This article addresses the challenges of memory safety in life-critical medical devices. Since the last decade, healthcare manufacturers have embraced the Internet of Things, pushing technological innovations to increase market share. Medical devices, including the most critical ones, tend to be increasingly connected to the Internet. Unfortunately, as critical devices often rely on unsafe programming languages such as C, they are no exception to memory safety issues. Given a memory vulnerability, a skillful attacker can take over a system and perform remote code execution. Combined with the fact that medical devices directly impact the safety of their users, a security vulnerability can lead to disastrous scenarios. To address this issue, this article presents TrustFlow-X, a novel hardware/software co-designed framework that provides efficient fine-grained control-flow integrity protection against memory-based attacks. The TrustFlow-X framework is composed of an LLVM-based compiler toolchain that generates a secure code. This secure code is then executed on an extended RISC-V processor that keeps track of sensitive data using a trusted memory. The obtained results show that the contribution is practical, providing a high level of trust in life-critical embedded systems.

Fault tolerance is a key research area for many of applications such as those based on sensor network technologies. In a large scale wireless sensor network (WSN), it becomes important to find new methods for fault-tolerance that can meet new application requirements like Internet of things, urbane intelligence and observation systems. The challenge is beyond the limit of a single wireless sensor network and concerns multiple widely interconnected sub networks. The domain of fault grows considerably because of this new configuration. In this context, the paper proposes a fault fuzzy-ontology (FFO) for large scale WSNs to be used within a Web service architecture for diagnosis and testing.

This paper proposes a functional testing approach for safety properties formalized as hybrid automata. We first propose a formalism inspired from the concept of operational profile to specify test requirements for hybrid automata. We propose an associated parametric adequacy criterion that measures to what extent a given test suite satisfies these requirements. We also develop a set of hypothesis under which the proposed criterion can be evaluated when testing from a black box system when time is discretized and some signals of the automaton are not observable on the concrete system under test. We finally present the HyATT tool prototype that was developed to implement the proposed approach, and report practical feedback of applying it on a case study.

In recent years, radio frequency identification (RFID) systems have been increasingly used in critical domains such as medical field or real-time processing domains. Although important efforts have been made to make this technology more reliable and fault-tolerant, more research is needed to meet the increasing dependability requirements. In this article, we propose a dependability approach consisting in two steps. The first one is an analysis of RFID systems in order to identify potential failures of RFID middleware components and their effects on the whole system. The second one is the modelling of the communication behaviour of RFID systems (that is represented by Low Level Reader Protocol) as a finite state machine. This protocol FSM will be extended to take into consideration the failures identified in the first step and serves as a diagnosis and test tool for the RFID system.

In this case study we test a landing gear control system of a military aircraft with the new version of Lutess, a tool for testing automatically synchronous software. Lutess requires the tester to specify the environment of the software under test by means of invariant properties in order to guide the test data generation. This specification can be enriched by operational profile specification in order to obtain more realistic scenarios. Moreover, test generation guided by safety properties makes possible to test more thoroughly the key features of the software, possibly under hypotheses on the software behavior. In this case, the generator chooses input data which are able to violate the properties. The new version of Lutess is based on constraint logic programming and provides some additional features (numeric inputs and outputs, hypotheses for safety guided testing, more powerful operational profiles). In this paper, we present the necessary steps for building the test model for Lutess on a real case study from the avionics. This makes possible to better understand the applicability of the approach and to assess the difficulty and the effectiveness of such a process in real-world applications.

Abstract LUSTREis a data‐flow synchronous language, on which is based the SCADEtool‐suite, widely used for specifying and programming critical reactive applications in the areas of avionics, energy or transport. Therefore, testing LUSTREprograms, that is, generating test data and assessing the achieved test coverage, is a major issue. Usual control‐flow‐based test coverage criteria (statement coverage, branch coverage, etc.) are not relevant for LUSTREprograms. In this paper, a new hierarchy of adequacy criteria tailored to the LUSTRElanguage is presented. These criteria are defined on operator networks, which are usual models for LUSTREprograms. The criteria satisfaction measure is automated in LUSTRUCTU, a non‐intrusive tool (no instrumentation of the code), based on the symbolic computation of path activation conditions. The applicability and the relevance of the criteria are assessed on a case study. Copyright © 2008 John Wiley & Sons, Ltd.

Lutess is a testing environment designed for synchronous software specified with Lustre, a synchronous data-flow language. It makes possible to automatically generate test input sequences in conformance with a specification of the software external behavior and of guiding directives such as operational profiles and behavioral patterns. Lutess deals with software and specifications involving only Boolean inputs and outputs. In this paper we propose an extension of Lutess, using constraint logic programming (CLP), making possible to deal with numeric inputs and outputs. In particular, we define an appropriate execution model for test input generation and show how test data generation according to the main guiding facilities of Lutess can still be performed. Furthermore, operational profile based generation becomes more powerful thanks to the introduction of CLP solvers capabilities which make possible to associate occurrence probabilities to any Boolean expression

We present structural test coverage criteria for LUSTRE programs. LUSTRE is a synchronous data-flow declarative language widely used for safety-critical applications (avionics, energy, transport). Many coverage criteria are defined for sequential languages and are widely used in the software industry (for instance, statement or branch coverage). They are defined on the program control-flow graph and, hence, do not apply to LUSTRE programs, represented by data-flow diagrams. We have defined several criteria to measure the coverage achieved after the execution of a test set, based on symbolic computation of path activation conditions. The coverage assessment is non-intrusive (there is no code instrumentation). These criteria provide the user with meaningful automatically computed measures of the thoroughness of a given test set.

We present Lustructu, a tool measuring the structural coverage of LUSTRE programs. LUSTRE is a synchronous data-flow declarative language widely used for safety-critical applications (avionics, energy, transport...). Many coverage criteria are defined for sequential languages and are widely used in the software industry (for instance, statement or branch coverage). They are defined on the program control-flow graph and, hence, do not apply to LUSTRE programs, represented by data-flow diagrams. We have defined several criteria to measure the coverage achieved after the execution of a test set, based on symbolic computation of path activation conditions. These criteria, implemented in Lustructu, provide the user with meaningful automatically computed measures of the thoroughness of a given test set

In this paper we present a method for automatically testing interactive multimodal systems. The proposed approach was originally dedicated to synchronous programming which is mainly used for real-time systems. Nevertheless, the behaviour of real-time systems, consisting of cycles starting by reading an external input and ending by issuing an output, is to a certain extent similar to the one of interactive systems. So considered, this paper investigates the use of the Lutess testing environment dedicated to synchronous software for automatically testing multimodal interactive (not necessarily real-time) systems. More precisely, we focus on test data generation based on operational profiles. The main benefit of this approach is that it increases the ability to automatically test an interactive system over long input sequences, according to various use profiles.

Adequacy criteria for structural testing techniques are defined in terms of coverage (e.g. of statements or branches). For black-box testing, such criteria, making testers able to decide when to stop testing, are more difficult to define. In this paper, we propose such a definition for the particular case of specification-based testing techniques for synchronous software supplied by the Lutess testing environment. Lutess provides a framework for automatically building generators interacting with the software under test and feeding it with test input sequences. It requires a Lustre specification of both the software environment and the software safety properties. This specification is translated into an input-output automaton. A critical situation occurs when a safety property can be violated unless the software reacts adequately. Such situations correspond to particular states of the specification automaton, called suspect states. Suspect states definition can be used in two complementary ways: First, to design testing techniques able to reach several such states during testing. Second, to assess the thoroughness of a test input sequence in terms of covered suspect states. The above techniques are illustrated on a telephony software specification developed for the first Feature Interaction Detection Contest and involving 12 different telephone features. The thoroughness of the Lutess testing strategies is assessed as their ability to lead the software into suspect states.

The paper presents new techniques for specification based-testing of synchronous software with the Lutess tool. Lutess provides a framework consisting of automatically building generators which interact with the software under test and feed it with test input sequences. In the past few years, it has been established that operational profiles as well as scenarios are powerful tools, allowing for a better fault detection ability. As opposed to this last technique which relies on the ability of the human tester to specify scenarios, we propose an approach based solely on software specification to automatically generate input sequences which may correspond to fault revealing scenarios.

LUSTRE is a synchronous declarative language designed to specify and to implement reactive software. One of its main advantages is that it can be used as a temporal logic to express software invariant properties. The satisfaction of the latter can be proven by model-checking, using LESAR, a verification tool designed for LUSTRE programs. We address two important problems related to this verification process. First, developing the specifications of synchronous software is a difficult and error-prone task. Before attempting to formally prove their satisfaction, one should validate them. We propose random automatic animation as a means to validate such formal specifications. Second, due to the often huge amounts of required memory and time, proof may not be applicable, in which case the specification work is wasted. To cope with this problem, we propose testing techniques which reuse the software specifications to formally test the software.

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.>