The VALS team is interested in the application of formal methods for the test of soft- and hardware systems. Particular emphasis is put on combinations of Test and Proof techniques.

• model-based testing using logical representations and proof techniques,
• random-based exploration methods, and
• automata and model-checking for behavioural models.

The fundamental research of the group relies on theoretical activities around the formalisms used for specification and modelisation (higher-order logics, transition systems, process algebras) and their associated verification methods (theorem proving, symbolic evaluation), exploration methods (random-based exploration of large models or programs), or symbolic runtime-checking (of time in hybrid systems).

The application domains of this work cover security infrastructures, critical embedded systems (operating systems, medical devices) as well as distributed and communicating systems (communication protocols, Web services). A further domain consists in the development of test-generation methods for programming languages.

Formalisation of specification languages: Circus

Process algebras like CSP (Concurrent Sequential Processes), CCS/Lotos or Circus provide a framework to model abstract and concrete system processes, their reactive behavior and their architecture in form of sub-processes. Circus is essentially an integration of CSP and Z, with in addition a notion of refinement. This makes it possible to specify reactive systems with states where complex data structures may be stored and evolve, and to describe their refinement into imperative programs. This research aims at developing testing theories for Circus and to design test-strategies by derived rules from a formal semantics, thus exemplifying testing strategies that take into account both behavior and data type specificities of the specification of the system under test. A prototypical test-environment implemented in Isabelle/HOL generates from Circus specifications jUnit-Testfiles.

Formalisation of specification languages: HOL-OCL

The thesis "Automated Generation of Tests with Isabelle and HOL-TestGen" attempts to apply “proof-based testing techniques” on concrete embedded systems to be concretized by project partners. The Isabelle/HOL is be used to formalize wide-spread specification languages (UML, OCL) as logical embeddings and to extend them by techniques to generate unit-tests from models involving constraints using distributed and massively parallel processors. This work focusses strategies to test for fairly complex pre-conditions and invariants represented inside a non-standard, 4-valued logics.

Testing IPC Communication

The goal of the project is to address secure virtualisation for trustworthy applications in critical domains. The mission of the EURO-MILS project is to develop a solution for virtualisation of heterogeneous resources and provide strong guarantees for isolation of resources by means of Common Criteria certification with usage of formal methods. Our team is involved in particular as part of the activity to use model-based testing techniques to establish conformance of the real concurrent code to the projects system models. Part of the research is oriented to the question, how can tests be organized in a format such that it is useable in an Common Criteria EAL5+ certification process.

Multicore interactive front-ends for proof assistants (till 2015)

The Paral-ITP project intends to overcome the sequential execution model for the interactive theorem proving systems Coq and Isabelle, to make the resources of multi-core hardware available for even larger proof developments. Beyond traditional processing of proof scripts as sequence of proof commands, and batchloading of theory modules, there is a large space of possibilities and challenges for pervasive parallelism. This affects many layers of each prover system: basic computational structures, inference kernel, tactical programming, proof command language, and interactive front-ends. Some of these aspects need to be addressed for Coq and Isabelle in slightly different ways, to accommodate different approaches in either system tradition. These substantial extensions of the operational aspects of interactive theorem proving shall retain the trustability of LCF-style proving at the very core. The parallelization mechanisms are of foundational importance for HOL-TestGen, a modeling and test data generation environment based on Isabelle.

Service Orchestration Modelling and Testing

Abstraction used in the requirement, composition, and adaptation processes, together with the important role played by composition execution engines, make it important to test service compositions. In this direction, we adress conformance testing of service orchestrations with several methods that go from enumerate to symbolic approaches. The main contributions of this work are an end-to-end and fully automated online testing technique and a symbolic approach to avoid state space explosion in formal models due to rich XML-based data used in Web service interfaces. An eclipse plug-in, SWST tool, is avalaible.

Model-checking and testing of distributed and Concurrent Systems

In distributed environment, services can be developed independently and are composed to achieve common requirements through interactions between them. Several kinds of models like service choreographies, message sequence charts or Petri nets are used to define such requirements, specifying the interactions among a set of participants. As for choreographies specifications, we have formalized the problems and developped a framework by which service choreographies can be developed correctly for top-down or bottom-up approaches. We work on composition/decomposition service design, testing of choreography implementation. We focus our research on the handling on data part by means of symbolic techniques and on passive technique for the implementation testing. We work also on Petri net specification to deal with concurrent systems and on the definition of several conformance relations allowing to handle concurrency explicity.

Random Exploration Methods and Application to Testing

Methods based on randomness seem attractive for testing large programs or checking large models. Designing efficient random methods is far from obvious since the underlying probability distributions must be carefully designed to get a good coverage of the program or model and to quantify it probabilistically. On the basis of classical results in the area of random generation of combinatorial structures, we develop algorithms and tools for the randomised exploration of graphs with probabilistic guarantee of coverage. This work is applied to random program testing and model-checking. The main aspects have been published in STTT in 2011. Implementation of these techniques led to the RUKIA library (developed by J. Oudinet, a former PhD student) that handle very large models, for instance allowing to generate paths of length 4000 in an automaton with more than 12 million states. RUKIA is also applied for uniform drawing of "lassos" that occurs in model-checking of LTL formulas. Uniform drawing of paths has been adapted for covering other structural items like vertices (states), egdes (transitions) or some structurally defined subset of all paths. In the area of program testing, we aim at showing that coverage-biased drawing of paths can better handle the problem associated with unfeasible paths and can scale up reasonably well. We plan to implement a prototype within the Frama-C platform (http://frama-c.com) for a subset of C.

• Project FSF: thesis in collaboration with IRT SystemX (formalisation of specification languages).
• Project PST: thesis in collaboration with IRT SystemX (applications of proof and test techniques to safe and secure embedded systems).
• EU IP EURO-MILS (secure virtualisation).
• ANR Paral-ITP (multicore interactive front-ends for proof assistants)
• STIC-AmSud project - DATE (Distributed Diagnosability and Testability of Faulty Systems)

• Rukia Rukia is a C++ library to explore graphical models by generating at random paths in automata.
• Contributions to Isabelle/HOL (till 2015): In the ANR Project Paral-ITP, the VALS team made major contributions (and the integration) to the Isabelle Versions 2011,2012, 2014 and 2015.
• Schora Schora is a tool (with an online version) to deal with Symbolic Choreography analysis.
• SWST SWST is a Symbolic Web Service Composition Testing tool.
• HOL-TestGen: HOL-TestGen is a test case generator for specification based unit testing. HOL-TestGen is built on top of the specfication and theorem proving environment Isabelle/HOL.
• Abderrahmane Feliachi, Burkhart Wolff, Marie-Claude Gaudel.
  Isabelle/Circus.
  Archive of Formal Proofs, May 2015.
• Achim D. Brucker, Frédéric Tuong, Burkhart Wolff.
  Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5.
  Archive of Formal Proofs, January 2014.
• Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff, Julien Schmaltz.
  Formal Specification of a Generic Separation Kernel.
  Archive of Formal Proofs, July 2014.
• Achim D. Brucker, Lukas Brügger, Burkhart Wolff.
  Formal Network Models and Their Application to Firewall Policies (based on UPF).
  Archive of Formal Proofs, November 2017.
• Frédéric Tuong, Burkhart Wolff.
  A Meta-Model for the Isabelle API.
  Archive of Formal Proofs, September 2015.

• Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff: Symbolic Test-generation in HOL-TESTGEN/CirTA A Case Study. Int. J. Software and Informatics 9(2): 177-203 (2015)
• Achim D. Brucker, Lukas Brügger and Burkhart Wolff: Formal Firewall Conformance Testing - An Application of Test and Proof Techniques. In: Software Testing, Verification and Reliability (STVR). DOI: 10.1002/stvr.1544. 40 pages. Wiley InterScience (www.interscience.wiley.com), July 2015. [pdf]
• Romain Aïssat, Frédéric Voisin, Burkhart Wolff: Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of Paths. ITP 2016: 36-51
• Romain Aïssat, Marie-Claude Gaudel, Frédéric Voisin, Burkhart Wolff: A Method for Pruning Infeasible Paths via Graph Transformations and Symbolic Execution. QRS 2016: 144-151
• Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, Burkhart Wolff: A Symbolic Operational Semantics for TESL - With an Application to Heterogeneous System Testing. FORMATS 2017: 318-334
• Achim D. Brucker, Idir Aït-Sadoune, Paolo Crisafulli, Burkhart Wolff: Using the Isabelle Ontology Framework - Linking the Formal with the Informal. CICM 2018: 23-38
• Georges L. A. Ouffoue, Fatiha Zaïdi, Ana R. Cavalli, Mounir Lallali: An Attack-Tolerant Framework for Web Services. SCC 2017: 503-506
• Huu Nghia Nguyen, Fatiha Zaïdi, Ana R. Cavalli: Effectively Testing of Timed Composite Systems using Test Case Prioritization. SEKE 2016: 408-413
• Xiaoping Che, Stephane Maag, Huu Nghia Nguyen, Fatiha Zaïdi: Guiding Testers' Hands in Monitoring Tools: Application of Testing Approaches on SIP. ICTSS 2015: 105-123