Research Activities

Research Activities (or: Special Interest Groups) were used to give "research areas" a more refined structure. They were supported by one or more ForTesSE members and provide an iterest in a research theme beyond the organizational boundaries of a financed research project or Phd project.

An (incomplete) List of Activities:

The rest of this page contains outlines of activities of the group ForTesSE. So far, we have in particular:

 

 

Modeling Sequence and Unit-Testing in HOL

Description: The purpose of this line of research is to investigate universal, i.e. not specification language oriented techniques for the representation of test-specifications and their decomposition. This covers monadic representations of test-sequences and (still rudimentary) theories of automata in HOL which can be found in the libraries of HOL-TestGen.

People: Burkhart Wolff, Matthias Krieger, Abdou Felliachi, Delphine Longuet

Collaborations: Achim Brucker(SAP Research, Karlsruhe), Lukas Brügger(ETH Zürich).

Publications:

Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff. An Approach to Modular and Testable Security Models of real-world health-care Applications. Proceedings of the ACM Symposium on Access control models and technologies, pages 133-142. ACM, 2011. SACMAT 2011. [ bib ]
Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff. HOL-TestGen 1.5.0 user guide. Technical Report 670, ETH Zurich, April 2010. [ bib | http | .pdf ]
Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff. Verified Firewall Policy Transformations for Test Case Generation. Software Testing, Verification, and Validation, 2010 International Conference on, 0:345-354, 2010. [ bib | DOI | .pdf ]
Achim D. Brucker and Burkhart Wolff. HOL-TestGen: An Interactive Test-case Generation Framework. In Marsha Chechik and Martin Wirsing, editors, Fundamental Approaches to Software Engineering (FASE09), number 5503 in Lecture Notes in Computer Science, pages 417-420. Springer-Verlag, Heidelberg, 2009. [ bib | DOI | http | .ps.gz | .pdf ]
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Model-based Firewall Conformance Testing. In Kenji Suzuki and Teruo Higashino, editors, Testcom/FATES 2008, LNCS 5047, pages 103-118. Springer-Verlag, Tokyo, Japan, 2008. [ bib | DOI | http | .pdf ]
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Verifying test-hypotheses - an experiment in test and proof. In Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko, editors, Model-based Testing (MBT) 2008, volume 202 of Electronic Notes in Theoretical Computer Science, pages 15-28, Budapest, Hungary, 2008. Elsevier Science Publishers. [ bib | DOI | .pdf ]
Achim D. Brucker and Burkhart Wolff. Test-sequence Generation with HOL-Testgen - with an application to firewall testing. In Bertrand Meyer and Yuri Gurevich, editors, TAP 2007: Tests And Proofs, number 4454 in Lecture Notes in Computer Science, pages 149-168. Springer-Verlag, Zurich, 2007. [ bib | DOI | http | .ps.gz | .pdf ]
Achim D. Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 user guide. Technical Report 482, Computer Security Group, ETH Zürich, apr 2005. [ bib ]
Achim D. Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Wolfgang Grieskamp and Carsten Weise, editors, Formal Approaches to Testing of Software (FATES 05), LNCS 3997, pages 87-102. Springer-Verlag, Edinburgh, 2005. [ bib | DOI ]
Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Jens Grabowski and Brian Nielsen, editors, Formal Approaches to Testing of Software (FATES 04), LNCS 3395, pages 16-32. Springer-Verlag, Linz 04, 2005. [ bib | DOI | http ]
 

Modeling Systems in UML/OCL for Unit Testing

Description: The Unified Modeling Language (UML) is a de-facto standard for specifications in an industrial context. While mostly used for model-driven architecture (MDA) developments, it has in parts a formal semantics and is thus amenable to formal analysis (consistency checks) and verification techniques, let them be oriented towards test or proof. The challenge is to complete the formal semantics documents and assure their consistency as well as the development of specific techniques to deal with the inherent object-oriented bias of this modeling technique.

People: Burkhart Wolff, Matthias Krieger, Delphine Longuet alt

Collaborations: Achim Brucker

Publications

Achim D. Brucker, Matthias P. Krieger, Delphine Longuet, and Burkhart Wolff. A Specification-based Test Case Generation Method for UML/OCL. In Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010), 2010. LNCS 6627. [ bib | .pdf ]
Matthias P. Krieger, Alexander Knapp, and Burkhart Wolff. Automatic and Efficient Simulation of Operation Contracts. In Eelco Visser, Jaakko Jarvi, and Giorgios Economopoulos, editors,Ninth International Conference on Generative Programming and Component Engineering (GPCE'10). IEEE Computer Society, 2010. [ bib | DOI | .pdf ]
Achim D. Brucker and Burkhart Wolff. Semantics, Calculi, and Analysis for Object-Oriented Specifications. Acta Informatica, 46(4):255-284, 2009. [ bib | DOI | .pdf ]
Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff. Extending OCL with null-references. In S. Ghosh, editor, MODELS 2009 Workshops, LNCS 6002, pages 261-275. Springer Verlag, Heidelberg, 2009. Best-Paper Award at the OCL 2009 Workshop. [ bib | http | .ps.gz | .pdf ]
Achim D. Brucker and Burkhart Wolff. Extensible universes for object-oriented data models. In Jan Vitek, editor, Proceedings of the European Conference of Object-Oriented Programming (ECOOP 2008), LNCS 5142, pages 438-462. Springer-Verlag, Paphos, Cyprus, July 2008. [ bib | DOI | http | .pdf ]
Achim D. Brucker and Burkhart Wolff. An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++. Journal of Automated Reasoning (JAR), Selected Papers of the AVOCS-VERIFY Workshop 2006(3-4):219-249, 2008. Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds). [ bib | DOI | .pdf ]
Achim D. Brucker and Burkhart Wolff. A Formal Proof Environment for UML/OCL. In Proceedings of Formal Aspects of Software Engineering (FASE 2008), volume 4961 of Lecture Notes in Computer Science, pages 97-101. Springer Berlin / Heidelberg, 2008. [ bib | DOI | .pdf ]
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. An MDA framework supporting OCL. Electronic Communications of the EASST, 5, 2007. [ bib | http | .pdf ]
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. Semantic issues of OCL: Past, present, and future. Electronic Communications of the EASST, 5, 2007. [ bib | http | .pdf ]
Achim D. Brucker and Burkhart Wolff. The HOL-OCL Book. Technical Report 525, ETH Zürich, 2006. [ bib | .pdf ]
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. An MDA framework supporting OCL. In 6th OCL Workshop at the UML/MoDELS Conference, 2006. [ bib | .pdf ]
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. A model transformation semantics and analysis methodology for SecureUML. In Oscar Nierstrasz, Jon Whittle, David Harel, and Gianna Reggio, editors, MoDELS 2006: Model Driven Engineering Languages and Systems, LNCS 4199, pages 306-320. Springer-Verlag, Genova, 2006. An extended version of this paper is available as ETH Technical Report, no. 524. [ bib | DOI | .pdf ]
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. Semantic issues of OCL: Past, present, and future. In 6th OCL Workshop at the UML/MoDELS Conference, 2006. [ bib | http | .pdf ]
Burkhart Wolff. Correct tools for formal methods in software engineering, 2005. Habilitationsschrift. [ bib | .pdf ]
Achim D. Brucker and Burkhart Wolff. A proposal for a formal OCL semantics in Isabelle/HOL. In César Muñoz, Sophiène Tahar, and Víctor Carreño, editors, Theorem Proving in Higher Order Logics, number 2410 in Lecture Notes in Computer Science, pages 99-114. Springer-Verlag, Hampton, VA, USA, 2002. [ bib | DOI | http | .pdf ]

 


 

 

Testing based on Process Algebra Specifications

Description: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-like languages and to design and experiment testing strategies that take into account both behavior and data type specificities of the specification of the system under test.

People: Burkhart Wolff, Abderrahmane Feliachi, Marie-Claude Gaudel.

Collaborations: Ana Cavalcanti(Uni York), Jim Woodcock (Uni York)

Publications:
Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Unifying Theories in Isabelle/HOL. In Unifying Theories of Programming (UTP2010), number 6445 in Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2010. [ bib | .pdf ]
Ana Cavalcanti and Marie-Claude Gaudel. Testing for refinement in Circus. Acta Informatica, 48(2):97-147, . [ bib | pdf ]
Ana Cavalcanti and Marie-Claude Gaudel. Specification coverage for testing in Circus. In Unifying Theories of Programming 2010, volume to appear of Lecture Notes in Computer Science, Shanghai, China, November 2010. Springer Verlag. 45 pages. [ bib | pdf ]
A. Cavalcanti and M.-C. Gaudel. Testing for refinement in CSP. In Formal Methods and Software Engineering, ICFEM 2007, volume 4789 of Lecture Notes in Computer Science, pages 151-170. Springer Verlag, 2007. [ bib | pdf ]
H. Tej and B. Wolff. A corrected Failure-Divergence Model for CSP in Isabelle/HOL. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Proceedings of the FME 97 - Industrial Applications and Strengthened Foundations of Formal Methods, LNCS 1313, pages 318-337. Springer Verlag, 1997. [ bib | DOI | .ps.gz | .pdf ]

 

Modeling Security Policies

Description: The goal of this research area is to find unified framework to security policies, the "Unified Policy Framework" (UPF) enabling to model, combine, and test security enforcement points in system architectures and to test and prove abstract properties over them. UPF has similar goals to Belnap-Logics for security-modeling, but a more constructivist flavor. The main incentive of the approach is to view UPF-models as model-based specifications and to derive test-cases for them. The UPF framework as well as concrete policies are specified in Higher-order logic integrated in HOL-TestGen. This approach has been applied in two major case-studies:

  1. automatic generation of test-cases for firewall policies - for both stateless and stateful firewalls, and
  2. the security policies for a large-scale patient data-management system: the access framework for the National Program for IT in the NHS England (NPfIT). We focus on the policies governing access to the Summary Care Records held in the SPINE. Access to patient data in this system is governed by several concepts:
    • Role-based Access Control 
    • Legitimate Relationships
    • Patient's Consent
    • Sealed Envelopes

The combination of these different concepts serves as a challenging scenario for model-based policy specification, policy analysis, and policy testing.

People:Burkhart Wolff

Collaborations: Achim Brucker (SAP Research Karlsruhe), Lukas Brügger (ETH Zürich), Paul Kearney (British Telecom)

Project Web-site: Here

Publications:

Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. An Approach to Modular and Testable Security Models of Real-world Health-Care Applications. In ACM symposium on access control models and technologies (SACMAT), ACM Press, 2011.
[PDF][Presentation]
Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. Verified firewall policy transformations for test case generation. In Ana Cavalli and Sudipto Ghosh, editors, International Conference on Software Testing (ICST10). Springer-Verlag, 2010. [PDF] [Presentation]
Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Model-based Firewall Conformance Testing. In Testcom/FATES 2008. Lecture Notes in Computer Science Springer-Verlag, 2008. [PDF, © Springer-Verlag]
Achim D. Brucker and Burkhart Wolff. Test-Sequence Generation with HOL-TestGen - With an Application to Firewall Testing. In TAP 2007: Tests And Proofs. Lecture Notes in Computer Science 4454, Springer-Verlag, 2007. [PDF,© Springer-Verlag]
Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Verifying Test-Hypotheses - An Experiment in Test and Proof. In Model-based Testing (MBT 2008). Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2008.[PDF]

 

Modeling Operating and Embedded Systems

DescriptionThe goal of this research area is to develop modeling and testing techniques for low-level, machine oriented computer components. This includes memory models. processor models and their embedding in a "real hardware"-environment. The models are typically oriented on bitvector-representations; the goal of the modeling is, of course, the generation of tests for soft- and hardware.

People: Burkhart Wolff, Abdou Felliachi, Yakoub Nemouchi

Collaborations: Matthias Daum, Wolfgang Paul

Publications:

Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler. Journal of Automated Resoning (JAR), 44(1-2):111-144, 2009. [ bib | DOI | .pdf ]
Matthias Daum, Jan Dörrenbächer, and Burkhart Wolff. Proving Fairness and Implementation Correctness of a Microkernel Scheduler. Journal of Automated Reasoning (JAR), 42(2-4):349-388, 2009. G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008). [ bib | DOI | .pdf ]
Matthias Daum, Jan Dörrenbächer, Mareike Schmidt, and Burkhart Wolff. A verification approach for system-level concurrent programs. In Verified Software: Theories, Tools, Experiments, LNCS 5295, pages 161-176. Springer Berlin / Heidelberg, September 2008. [ bib | DOI | .pdf ]
Sascha Böhme, Rustan Leino, and Burkhart Wolff. HOL-Boogie - An Interactive Prover for the Boogie Program Verifier. In Sofiene Tahar, Otmane Ait Mohamed, and César Muñoz, editors, 21th International Conference on Theorem proving in Higher-Order Logics (TPHOLs 2008), LNCS 5170. Springer-Verlag, Montreal, Canada, 2008. [ bib | DOI | .pdf ]
Achim D. Brucker and Burkhart Wolff. A verification approach for applied system security. International Journal on Software Tools for Technology Transfer (STTT), 7(3):233-247, 2005. [ bib | DOI | .pdf ]
Nicole Rauch, Burkhart Wolff: Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL. Electr. Notes Theor. Comput. Sci. 80: 41-58 (2003)

 

Extending the Isabelle Platform (Plug-In Mechanisms, Pervasive Parallelism, PIDE)

Description: Isabelle/HOL is the technical platform for several major research developments of ForTesSE. The group therefore engages in improving the plug-in mechanisms for Isabelle ("Isabelle as an Eclipse for FM Tools"), its computational basis ("Parallel Kernel supporting asynchronous Proof Development") and new industry-strength IDE's called PIDE in order to improve the applicability of Isabelle further. The contributions (in particular realized by Makarius Wenzel) have been integrated into the Isabelle Versions 2009,2010,2011  ad 2011-1, 2012 and 2013.

People: Burkhart Wolff, Makarius Wenzel

Related Projects: HOL-TestGen XT (funding for Makarius Wenzel for 2 years),  ANR project Paral-ITP.

Collaborations: within ANR project Paral-ITP: INRIA Rocquencourt (H. Herbelin), INRIA Saclay (B. Barras). PIDE discussion group.

Publications:

Makarius Wenzel: Isabelle/jEdit –- A Prover IDE within the PIDE Framework. CICM/MKM 2012LNCS 7362, pp. 468-471. 
Makarius Wenzel and Burkhart Wolff: Isabelle/PIDE as Platform for Educational Tools Thedu '11, pp 143-153.
David C. J. Matthews, Makarius Wenzel: Efficient parallel programming in Poly/ML and Isabelle/ML. DAMP 2010, pp 53-62.
Makarius Wenzel, Lawrence C. PaulsonTobias Nipkow: The Isabelle Framework. TPHOLs 2008, LNCS pp. 33-38.
Makarius Wenzel. Isabelle as Document-oriented Proof Assistant.Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011). LNCS 6824, pp. 244-259. 
Makarius Wenzel. Parallel Proof-Checking in Isabelle/Isar.In G. Dos Reis and L. Théry, editors. The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMSS). Munich, August 2009, ACM Digital Library.
David Aspinall, Christoph Lüth, and Burkhart Wolff. Assisted Proof Document Authoring. In Fourth International Conference on Mathematical Knowledge Management (MKM 05), LNCS 3863. Springer Verlag, 2005. [ bib | DOI | .pdf ]
Christoph Lüth and Burkhart Wolff. Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming, 9(2):167- 189, 1999. [ bib | DOI | .ps.gz | .pdf ]
Makarius Wenzel and Burkhart Wolff. Building formal method tools in the isabelle/isar framework. In Klaus Schneider and Jens Brandt, editors, TPHOLs 2007, LNCS 4732, pages 351-366. Springer-Verlag, 2007. [ bib | DOI | .pdf ]
Christoph Lüth and Burkhart Wolff. TAS - a generic window inference system. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, number 1869 in Lecture Notes in Computer Science, pages 405-422. Springer Verlag, 2000. [ bib | .pdf ]
 

Random-based Exploration and Testing of C-Programs

Description: In order to push ideas from random-based exploration and in order to experiment with resulting testing methods in practice,  a re-design of a new release of the Auguste prototype is untertaken. Auguste was initially developed by Sandrine-Dominique Gouraud for the statistical structural testing of programs in a subset of the C programming language [2]. The following diagram illustrates the global architecture of the system. The re-implementation Auguste++ will appear as a plug-in for the Frama-C platform (http://frama-c.com),  connected to external tools: on the one hand some tool for the uniform drawing  of paths (formerly Auguste used the “Mupad-Combinat”  package for drawing uniformly in “Combinatorial Structures”, and is now using the Rukia library (http://rukia.lri.fr) for drawing uniformly paths in large graphs); on the other hand we need SMT solvers for checking the satisfiability of the “path predicate” associated with each path or common prefix of paths. Note that since we are interested in concrete test cases we do not want only to check the executability of a path but also to have actual values for that path, at least for complete execution paths (satisfiability is sufficient for p artial paths). August will benefit from the various code analysers available in Frama-C and will offer a test generation capability. In the following diagram, the existing machinery (including GUI) of the Frama-C platform is drawn in a dashed lines, Auguste specific modules are in solid lines.

PICTURE HERE

There exists already various systems for generating tests for C (see [3,4,5] for descriptions of a few of them). Our main target is not in handling arbitrary C programs : we do not focus on handling low-level features (bit level computation, union types, arbitrary casts, representation of numbers, etc.) that can be better handled by concolic testing. The main purpose of Auguste is putting in practice our ideas about random testing in an actual working tool when exhaustive of deterministic methods would not be adequate.

A Comparison with “concolic testing” : concolic (“concrete+symbolic”) testing mixes concrete computations with symbolic evaluation and constraint solving. A first test case is started by executing the program on some initial set of values (provided by the tester or drawn randomly); The execution is monitored to perform the symbolic evaluation of the path corresponding to this execution and to record the “history of branching” along that path. Once the path is complete, one can backtrack to the most recent point of branching and negates the symbolic condition that was satisfied during this execution : one obtains a new path predicate fed into a constraint-solver to get a set of input values that allows to execute a new path (there are two other cases: the predicate cannot be satisfied, meaning that there was indeed no possibility of branching here, or the solver being enable to assert if the predicate is satisfiable or not). In this simplest form and by iterating this procedure, one gets a test set corresponding to the “all (executable) path” criterion. If there is a infinite set of path one has to restrict the criterion somehow. The procedure can be refined to handle other coverage criterion (“all-instructions”, “all branches”, all k-loops, etc). Concolic testing avoids the problem of unfeasible paths by relying on actual values yielding fixed and feasible paths.

Although concolic testing and the “statistical coverage-biased” testing of August share part of the techniques (symbolic evaluation, constraint-solving, possible use of annotations, etc) their approaches are quite different. The former is a “deterministic”, systematic way of deriving a test set, with one set of input value for each path in the set. The set of paths for covering a criterion is computed in a systematic way, once the first path is fixed by an initial concrete set of input values. Auguste approach is probabilistic, with a uniformity drawing method resulting in a set set that covers a given criterion with a known probability (thanks to the uniformity of the drawing), whose choice is part of the test strategy and related to the desired number of test cases, and allowing any number of paths of a desired length to be executed (possibly more than once, with possibly different sets of values). No path is ever discarded a priori from the drawing. 

People: Frederic Voisin, Marie-Claude Gaudel, Burkhart Wolff, Romain Aissat (doctorant), Alain Denise

Related Projects: Bourse Ministerielle pour la thèse de Romain Aissat

Selected Publications:

[1] Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet, and Sylvain Peyronnet. Coverage-biased random exploration of large models and application to testing. STTT, International Journal on Software Tools for Technology Transfer, 14(1):73-93, 2012.

[2] Sandrine-Dominique Gouraud: Utilisation des structures combinatoires pour le test statistique,

Thèse de doctorat en Informatique, Université Paris-Sud, 2004.

[3] R. Majundar and K. Shen : Hybrid Concolic Testing, ICSE '07 Proceedings of the 29th international conference on Software Engineering, pages 416-426 , 2007.

[4] C. Cadar, D. Dumbar, D. Engler : KLEE , Unassisted and Automatic Generation of High- Coverage Test for Complex Systems Programs. Usenix Symposium on Operating Systems Design and Implementation (OSDI), San Diego, 2008.

[5] N. Williams, Abstract path testing with PathCrawler. Proceedings of the 5th Workshop on Automation of Software Test, pages 35-42, 2010. 

[6] Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie - An Interactive Prover-Backend for the Verified C CompilerJournal of Automated Resoning (JAR), 44(1-2):111-144, 2009. [ bib | DOI | .pdf ]

 
 

RASTA

 

This research area is devoted to the randomised exploration of graphs with a probabilistic guarantee of coverage. This work leads to applications to random program testing and model-checking

Aims and Scope :

In recent years, the problem of studying and simulating random processes has particularly benefitted from progresses in the area of random generation of combinatorial structures. The seminal works of Wilf and Nijenhuis in the late 70's have led to efficient algorithms for generating uniformly at random a variety of combinatorial structures. In 1994, Flajolet, Zimmermann and Van Cutsem have widely generalised and systematised the approach. Briefly, their approach is based on a non-ambiguous recursive decomposition of the combinatorial structures to be generated. Their work constitutes the basis of powerful tools for uniform random generation of complex entities, as graphs, trees, words, paths, etc.

The RASTA Working Group activity is centred on the application of these powerful results to software testing, and more generally to verification.

Methods based on randomness seem attractive for testing large programs or checking large models. However, designing efficient random methods, i.e. methods that have a good and assessable fault detection power, is far from being obvious:  the underlying probability distribution must be carefully designed if one wants to ensure a good coverage of the program or model, or of potential fault locations, and to quantify coverage or fault detection.

A classical way to explore large graphs at random is random walk. A random walk in the state space of a model is a sequence of states s0, s1, ..., snsuch that sis a state that is chosen uniformly at random among the successors of the state si-1, for i = 1, ..., n.  It is easy to implement and only requires local knowledge of the model.

However, random walk methods have some drawbacks.  In case of irregular topology of the underlying transition graph, uniform choice of the next state is far from being optimal from a coverage point of view.  Moreover, for the same reason, it is generally not possible to get any estimation of the coverage obtained after one or several random walks: it would require some complex global analysis of the topology of the model.


Main achievements

All the various works below rely on combinatorial algorithms, based on a representation of the models or programs by an automaton or a by a product of several automata, synchronised or not.  These algorithms are implemented and available in the RUKIA library (http://rukia.lri.fr/en/index.html).

Uniform path exploration in very large composed models

A first method developed in RASTA makes it possible to perform uniform random walks (where every trace has the same probability to occur) in extremely large models taking advantage that they are composed of several components: it is possible to combine local uniform drawings of traces, and to obtain some global uniform random sampling, without construction of the global model ([2,3,4,6]). Experiments have been successfully led on models with 1034 states, with performances that show that the approach makes it possible to uniformly explore even larger models.

A dichotomic algorithm for the uniform random generation of words in regular languages:  A second problem studied in RASTA is that current implementations of uniform  random generation algorithms (namely recursive methods) need tables whose size grows with the length of the words that are to be generated. We have studied two different strategies to get rid of these tables. The first one consists in performing a kind of  ``on line'' random generation of traces by inverting the recurrences that are used in the classical recursive method; however, this method exhibits numerical instability when using floating point arithmetic.
The second one called dichopile" [7] based on a divide-and-conquer approach, avoids numerical instability and offers an excellent compromise in terms of space and time requirements.

 

Randomised coverage of states and transitions. Application to structural testing of programs

Although the method is based on the uniform drawing of paths in a graph, we have adapted it to address the coverage of other structural items like vertices (states), egdes (transitions) or or some structurally defined subset of all paths. We have defined a notion of randomised coverage satisfaction that has been applied to the structural unit testing of C programs [1,3,5], starting from the control flow graph of the function to be tested. This notion turns out to be related to the assessment of probabilities of fault detection, under the assumption of some fault model. It has been applied successfully to state-coverage and transition-coverage. The idea could also be applied starting from some other graph description of a system to be tested, for instance a  UML-like state machine model.

With such "coverage-biased" statistical methods, the drawing of test cases is designed for maximizing the probability of rare cases to be covered, although actual input values are still drawn randomly. The idea is to compute automatically the probability distribution to be used for the drawing to guarantee a fair exposition to test of all the parts of the program. With respect to a uniform distribution, the resulting distribution is biased towards the satisfaction of a given coverage criterion by the generated test cases.

Once paths have been generated, we are faced to the (undecidable) problem of knowing if there exist input values for executing exactly these paths. Techniques involved come from compiler construction, program annotation, abstract interpretation, symbolic evaluation and constraint-solving (for deciding if a path corresponds to an actual execution path), etc. Some research issues are: computing the "best" combinatorial structures or monitoring the drawing in order to avoid the selection of infeasible paths, efficient use of constraint-solvers for finding input values for executing a given path, adequate representation of coverage criteria besides the ones stated in terms of paths.

Pushing ideas in practice is done through the design of the next version of the Auguste prototype (Auguste++), initially developed by Sandrine-Dominique Gouraud for a small subset of a "C-like" language, for the structural statistical testing of C programs. 

Uniformly randomised LTL model-checking : 

In addition to the various current works mentioned above, we have generalised uniform drawing of paths to uniform drawing of so-called ``lassos'' that are interesting for Monte-Carlo model-checking of LTL formulas [8]. This implies counting and drawing elementary circuits, which is known as a hard problem. However, efficient solutions exist for specific graphs, such as reducible data flow graphs which correspond to well-structured programs and control-command systems. An immediate perspective is to embed this method in an existing model-checker such as SPIN or CADP, with the aim of developing efficient randomised methods for LTL model-checking with as result a guaranted probability of satisfaction of the checked formula.

Collaboration:

Equipe de Logique Mathématique de Paris 7 (Richard LASSAIGNE)

 

People:

  • Marie-Claude Gaudel
  • Romain Aissat, Ph. D. student, LRI/ForTesSE (since Sept. 2012)
  • Alain Denise, LRI/BioInfo
  • Sandrine-Dominique Gouraud, LRI/ForTesSE (until Sept. 30, 2008)
  • Johan Oudinet, Ph. D. student, LRI/ForTesSE (Sept. 2007-Dec. 2010)
  • Sylvain Peyronnet, LRI/Algo (until Sept. 2012), now at the Université de Caen
  • Frédéric Voisin, LRI/ForTesSE

 

Papers:

  1. A.Denise, M.-C. Gaudel, and S.-D. Gouraud : A generic method for statistical testing, in  IEEE Int. Symp. on Software Reliability Engineering (ISSRE),  pages 25--34, 2004.
  2. A.Denise, M.-C. Gaudel, S.-D. Gouraud, R.Lassaigne, and S.Peyronnet : Uniform random sampling of traces in very large models, in 1stInternational ACM Workshop on Random Testing, pages 10--19, July 2006.
  3. A. Denise, M.-C. Gaudel, S.-D. Gouraud, R.  Lassaigne, J. Oudinet, and S. Peyronnet : Coverage-biased random exploration of large models and application to testing, in STTT, International Journal on Software Tools for Technology Transfer, vol. 14, pp. 73-93, 2012.
  4. M.-C. Gaudel, A. Denise, S.-D. Gouraud, R.  Lassaigne, J. Oudinet and S. Peyronnet : Coverage-biased random exploration of large models, in 4th ETAPS Workshop on Model Based Testing, volume 220, Issue1, 10 of Electronic Notes in Theoretical Computer Science, pages 3--14,  2008 (invited lecture).
  5. S.-D. Gouraud, A.Denise, M.-C. Gaudel, and B. Marre :  A new way of automating statistical testing methods in IEEE International Conference on Automated Software  Engineering (ASE), pages 5--12, 2001.
  6. J. Oudinet :  Uniform random walks in very large models, in RT '07: Proceedings of the 2nd international workshop on Random testing}, pages 26--29, Atlanta, GA, USA, November 2007. ACM Press.
  7. J. Oudinet, A. Denise, and M.-C. Gaudel : A new dichotomic algorithm for the uniform random generation of words in regular languages, in Conference on random and exhaustive generation of combinatorial objects ({GASCom}), Montreal, Canada, September 2010. Extended version accepted in TCS, in press, 2012.
  8. J. Oudinet, A. Denise, M.-C. Gaudel, R. Lassaigne, S. Peyronnet : Uniform Monte-Carlo model checking, in FASE. LNCS vol. 6603, pp. 127--140, Springer, 2011.
  9. Johan Oudinet, Alain Denise, and Marie-Claude Gaudel. A new dichotomic algorithm for the uniform random generation of words in regular languages. TCS, Theoretical Computer Science, accepted, 2012. available online 

 

You are here Activities