MTV2 2023

Journée MTV2 du 16 Mars 2023

Laboratoire LMF, Université Paris Saclay

ENS Paris-Saclay - bâtiment Sud-Ouest (Etage 1), 4 avenue des Sciences, 91190 Gif-sur-Yvette, France 

Local organizers : Burkhart Wolff, Frédéric Voisin et Fatiha Zaidi

Sponsors : GDR GPL, Laboratoire LMF, Gradute School - Computer Science, Université Paris-Saclay

Programme de la journée

La durée d’un exposé régulier / regular talk duration: 20min+5min questions.

La durée d’un exposé invité / invited talk duration : 50min+10min questions.

9h45-10h10 Accueil, Café / Arrival, Coffee

10h10-11h55 Session 1

10h10-10h15 Ouverture de la journée / Opening of the day

10h15-10h40 An Efficient Black-Box Support of Advanced Coverage Criteria for Klee - Delphine Longuet - Thales

10h40-11h05 TreeFrog for Exhaustive Branch Coverage - Nicky Williams - CEA List

11h05-11h30 Opportunistic Monitoring of Multithreaded Programs - Chukri Soueidi - INRIA Grenoble Alpes

11h30-11h55 ehW - an inference approach for fully testing SUTs with data-dependent behaviour, without the need for resets - Germán Vega - UGA // This talk is moved to the afternoon - it will be the 1st in Session 3

11h55-13h45 Pause déjeuner / Lunch Break

13h45-14h45 Session 2 

13h45-14h45 Complete Model-based Module Testing - Jan Peleska - University of Bremen & Verified Systems

14h45-15h15 Pause café / Coffee Break

15h15-16h45 Session 3 

15h15-15h40 Computing the maximally-permissiveness of timed automata - Emily Clement - ISIR

15h40-16h05 Automated unit test generation integrated into an IDE - David Mentré - MERCE

16h05-16h30 - An Approach to Model-based Testing of Driving Strategies in Autonomous Cars - Burkhart Wolff - Université Paris Saclay

16h30-16h45 Annonces, discussions, fin de journée / Announcements, discussions, end of the day 

Résumés - Abstracts 

Invited talk. Complete Model-based Module Testing.  Jan Peleska, University of Bremen and Verified Systems.

(With contributions by Felix Brüning, Mario Gleirscher, Wen-ling Huang, Niklas Krafczyk, and Robert Sachtleben)

Model-based testing (MBT) intends to automate the verification process by automatically creating test cases and test suites from models. Preferably, the suites are then automatically executed in suitable test harnesses or more general test execution environments, and the responses of the system under test are automatically checked against the model, so that a manual creation of test oracles becomes superfluous as well.  Specific model-based test strategies are called complete: under certain hypotheses, they guarantee to accept every implementation conforming to the model and to uncover every violation of the conformance relation. Typical conformance relations are language equivalence or language inclusion at the system interface.

In this presentation, we report on complete MBT for module tests of C/C++ software code for embedded control systems. As a case study, the software of a novel automated train protection and train operation (ATP/ATO) system is tested. We show, how reference models can be easily created in the formalism of symbolic finite state machines (SFSM; these are finite state machine with input variables, output variables, guard conditions and output expressions). A crucial insight consists in the fact that the hypotheses required for guaranteeing test suite completeness can be checked by means of static analysis on the module source code. Consequently, the test suite achieves a formal verification of conformance between module code and reference model. Therefore, this test approach represents a practical alternative to proving code correctness by means of model checking or with the help of proof assistants. It turns out that the complete test of all safety-critical modules of the train control system can be achieved with surprisingly low effort. This is possible, because a specific equivalence partitioning strategy allows for a significant reduction of the otherwise very large number of input test data to be exercised on the module under test. The applicability of this strategy is verified by means of static analysis if the module code.

The underlying theory of complete test suites can be used both for verifying conformance relations and for property-oriented testing. The letter aims at showing that the software module correctly implements a set of LTL properties representing requirements that are properly reflected by the model. We have implemented the theory in  the libsfsmtest, an open source library for generating test suites from SFSM models. A web interface to the cloud server farm of our department allows for automated test generation from SFSM models, creation of test harnesses, and automated test execution in the cloud.

Regular talks.

• An Efficient Black-Box Support of Advanced Coverage Criteria for Klee (Delphine Longuet - Thales TRT)
  
  

Dynamic symbolic execution (DSE) is a powerful test generation approach based on an exploration of the path space of the program under test. Well-adapted for path coverage, this approach is however less efficient for conditions, decisions, advanced coverage criteria (such as multiple conditions, weak mutations, boundary testing) or user-provided test objectives. While theoretical solutions to adapt DSE to a large set of criteria have been proposed, they have never been integrated into publicly available testing tools. This talk presents a first integration of an optimized test generation strategy for advanced coverage criteria into a popular open-source testing tool based on DSE, namely, Klee. The integration is performed in a fully black-box manner, and can therefore inspire an easy integration into other similar tools. The resulting version of the tool, named Klee4labels, is publicly available. We present the design of the proposed technique and evaluate it on several benchmarks. Our results confirm the benefits of the proposed tool for advanced coverage criteria. This is a joint work with Nicolas Berthier, Steven De Oliveira, Nikolai Kosmatov and Romain Soulat. 

• TreeFrog for Exhaustive Branch Coverage (Nicky Williams - CEA List)
  
  

Concolic methods efficiently generate test inputs for exhaustive path coverage. However, exhaustive path coverage is not often required or even realistic whereas exhaustive branch coverage is at the heart of many verification tasks. We explain how, in TreeFrog, we have tried to find an efficient solution to this very different problem. We have kept the efficient aspects of depth-first concolic generation but combined it with multi-threading for breadth-first search, conflict learning lifted to branches and finally, some controlled path enumeration. First results show dramatic improvements over concolic methods.

• Computing the Maximally-permissiveness of Timed Automata (Emily Clement - ISIR)

Timed automata are a powerful mathematical model to verify real-time systems.  They are used to represent the temporal aspect of real-time systems. A crucial property is whether some state is reachable from an initial state. Nevertheless, a state can be declared reachable in this abstract model and still be impossible to reach in the physical system it models.  In our model, we add temporal perturbations that we quantify with a symbolic function called permissiveness and compute the maximally-permissiveness of timed automata using a two-players game model.

• Opportunistic Monitoring of Multithreaded Programs (Chukri Soueidi - INRIA Grenoble Alpes)
  
  

We introduce a generic approach for monitoring multithreaded programs online, leveraging existing runtime verification (RV) techniques. In our setting, monitors are deployed to monitor specific threads and only exchange information upon reaching synchronization regions defined by the program itself. They use the opportunity of a lock in the program to evaluate information across threads. As such, we refer to this approach as opportunistic monitoring. By using the existing synchronization, our approach reduces additional overhead and interference to synchronize at the cost of adding a delay to determine the verdict. We utilize a textbook example of readers-writers to show how opportunistic monitoring can express specifications on concurrent regions. We also present a preliminary assessment of the overhead of our approach and compare it to classical monitoring, showing that it scales particularly well with the concurrency present in the program.

• Automated unit test generation integrated into an IDE (David Mentré - MERCE)

Over the years, Mitsubishi Electric R&D Centre Europe (MERCE) has developed automated test generation tool for C language, based on AI and formal methods. Initially developed as a command line tool, we integrated it inside the well-known Microsoft VS Code IDE (Integrated Development Environment). Our aim is to test the software as early as possible, i.e. as soon as the source code has been written, in order to achieve the so-called shift-to-left in the V development cycle. During this presentation we will present our technology, its integration inside the IDE et the expected benefits on the development process.

• ehW - an inference approach for fully testing SUTs with data-dependent behaviour, without the need for resets (Germán Vega - UGA)

Model inference is particularly interesting from a software testing perspective, because there is a strong relationship between the ‘representativeness’ of the set of examples (i.e. execution traces) from which a model is inferred, and its test adequacy. A variety of active-learning algorithms have been developed to support such approaches. The classes of systems that can (at least reliably) be tested by such approaches are however bound by two significant constraints. Firstly, the need for the algorithm to attempt its own test sequences requires frequent resets of the system. Secondly, since most algorithms are based on FSMs, there can be no behaviour that depends on data values, either supplied as parameters or stored in memory.  

Over the course of the past decade, several techniques have been proposed to work around these limitations. Inference approaches have been proposed to minimise resets and there have been several approaches to accommodate parameters and internal registers in model inference. Although such approaches can be effective for their respective purposes, combining them into a unified approach is not straightforward. The query strategy that is required to identify control-states in a non-resettable machine is entirely different from that which is required to identify data-states in a system that may have unknown data registers. In this work we present an approach that achieves this feat. Our ehW -inference approach is capable of fully testing SUTs with data-dependent behaviour, without the need for resets.

• An Approach to Model-based Testing of Driving Strategies in Autonomous Cars (Burkhart Wolff - Université Paris Saclay)

Modelling and Analysing Cyber-Physical Systems (CPS) is a challenge for Formal Methods  and therefore a field of active research. It is characteristic of CPS that models comprise  aspects of Newtonian Physics appearing in system environments, the difficulties of their discretisation, the problems of communication and interaction between actors in this environment.  

We present a novel framework to address these problems developed with industrial partners involved  in the Autonomous Car domain. Based on HOL-CSP,  we model time, physical evolution, ”scenes”  (global states) and ”scenarios” (traces) as well as the interaction of ”actors” (vehicles, pedestrians, traffic lights)  inside this framework.   

Based on a proof on abstract safety properties for a particular well-known driving strategy called RSS, we derive functional test scenarios that can be used for system integration tests  of cars implementing this strategy.