Loïc Correnson

Vincent Mussot, Silvano Dal Zilio, Loic Correnson et al.

We propose a new approach for modelling the functional behaviour of an Earth observation satellite. We leverage this approach in order to develop a safety critical software, a "telecommand verifier", that is in charge of checking onboard whether a sequence of instructions is safe for execution. This new service is needed in order to add more autonomy to satellites. To do so, we propose a new Domain Specific Modelling Language and the toolchain required for integration into an embedded software. This framework is based on the composition of deterministic finite state machines with safety conditions , timeouts, and transitions that accept durations as a parameter. It is able to generate code in the synchronous programming language Lustre from a high-level specification of the satellite. This gives a formal way to derive an event-based algorithm simulating the execution of telecommand sequence and, thereupon, a provably correct onboard verifier.

Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov et al.

Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting efficient test suites, able to detect a maximum number of bugs with manageable effort. To do so, they rely on coverage criteria, which define some precise test objectives to be covered. However, many common criteria specify a significant number of objectives that occur to be infeasible or redundant in practice, like covering dead code or semantically equal mutants. Such objectives are well-known to be harmful to the design of test suites, impacting both the efficiency and precision of testers' effort. This work introduces a sound and scalable formal technique able to prune out a significant part of the infeasible and redundant objectives produced by a large panel of white-box criteria. In a nutshell, we reduce this challenging problem to proving the validity of logical assertions in the code under test. This technique is implemented in a tool that relies on weakest-precondition calculus and SMT solving for proving the assertions. The tool is built on top of the Frama-C verification platform, which we carefully tune for our specific scalability needs. The experiments reveal that the tool can prune out up to 27% of test objectives in a program and scale to applications of 200K lines of code.