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 UnitTesting in HOL.
 Modeling Systems in UML/OCL for Unit Testing
 Testing based on Process Algebra Specifications
 Modeling Security Policies
 Operating Systems and Embedded Systems
 Extending the Isabelle Platform (PlugIn Mechanisms, Pervasive Parallelism)
 Randombased Exploration and Testing of CPrograms
 RASTA (RAndom System Testing and Analysis)
Modeling Sequence and UnitTesting 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 testspecifications and their decomposition. This covers monadic representations of testsequences and (still rudimentary) theories of automata in HOL which can be found in the libraries of HOLTestGen.
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 realworld healthcare Applications. Proceedings of the ACM Symposium on Access control models and technologies, pages 133142. ACM, 2011. SACMAT 2011. [ bib ] 
Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff. HOLTestGen 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:345354, 2010. [ bib  DOI  .pdf ] 
Achim D. Brucker and Burkhart Wolff. HOLTestGen: An Interactive Testcase Generation Framework. In Marsha Chechik and Martin Wirsing, editors, Fundamental Approaches to Software Engineering (FASE09), number 5503 in Lecture Notes in Computer Science, pages 417420. SpringerVerlag, Heidelberg, 2009. [ bib  DOI  http  .ps.gz  .pdf ] 
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Modelbased Firewall Conformance Testing. In Kenji Suzuki and Teruo Higashino, editors, Testcom/FATES 2008, LNCS 5047, pages 103118. SpringerVerlag, Tokyo, Japan, 2008. [ bib  DOI  http  .pdf ] 
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Verifying testhypotheses  an experiment in test and proof. In Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko, editors, Modelbased Testing (MBT) 2008, volume 202 of Electronic Notes in Theoretical Computer Science, pages 1528, Budapest, Hungary, 2008. Elsevier Science Publishers. [ bib  DOI  .pdf ] 
Achim D. Brucker and Burkhart Wolff. Testsequence Generation with HOLTestgen  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 149168. SpringerVerlag, Zurich, 2007. [ bib  DOI  http  .ps.gz  .pdf ] 
Achim D. Brucker and Burkhart Wolff. HOLTestGen 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 HOLTestGen. In Wolfgang Grieskamp and Carsten Weise, editors, Formal Approaches to Testing of Software (FATES 05), LNCS 3997, pages 87102. SpringerVerlag, 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 1632. SpringerVerlag, Linz 04, 2005. [ bib  DOI  http ] 
Modeling Systems in UML/OCL for Unit Testing
Description: The Unified Modeling Language (UML) is a defacto standard for specifications in an industrial context. While mostly used for modeldriven 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 objectoriented bias of this modeling technique.
People: Burkhart Wolff, Matthias Krieger, Delphine Longuet
Collaborations: Achim Brucker
Publications:
Achim D. Brucker, Matthias P. Krieger, Delphine Longuet, and Burkhart Wolff. A Specificationbased 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 ObjectOriented Specifications. Acta Informatica, 46(4):255284, 2009. [ bib  DOI  .pdf ] 
Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff. Extending OCL with nullreferences. In S. Ghosh, editor, MODELS 2009 Workshops, LNCS 6002, pages 261275. Springer Verlag, Heidelberg, 2009. BestPaper Award at the OCL 2009 Workshop. [ bib  http  .ps.gz  .pdf ] 
Achim D. Brucker and Burkhart Wolff. Extensible universes for objectoriented data models. In Jan Vitek, editor, Proceedings of the European Conference of ObjectOriented Programming (ECOOP 2008), LNCS 5142, pages 438462. SpringerVerlag, Paphos, Cyprus, July 2008. [ bib  DOI  http  .pdf ] 
Achim D. Brucker and Burkhart Wolff. An Extensible Encoding of Objectoriented Data Models in HOL with an Application to IMP++. Journal of Automated Reasoning (JAR), Selected Papers of the AVOCSVERIFY Workshop 2006(34):219249, 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 97101. 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 HOLOCL 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 306320. SpringerVerlag, 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 99114. SpringerVerlag, 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 subprocesses. 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 Circuslike 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, MarieClaude Gaudel.
Collaborations: Ana Cavalcanti(Uni York), Jim Woodcock (Uni York)
Abderrahmane Feliachi, MarieClaude Gaudel, and Burkhart Wolff. Unifying Theories in Isabelle/HOL. In Unifying Theories of Programming (UTP2010), number 6445 in Lecture Notes in Computer Science. SpringerVerlag, Heidelberg, 2010. [ bib  .pdf ] 
Ana Cavalcanti and MarieClaude Gaudel. Testing for refinement in Circus. Acta Informatica, 48(2):97147, . [ bib  pdf ] 
Ana Cavalcanti and MarieClaude 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 151170. Springer Verlag, 2007. [ bib  pdf ] 
H. Tej and B. Wolff. A corrected FailureDivergence 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 318337. 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 BelnapLogics for securitymodeling, but a more constructivist flavor. The main incentive of the approach is to view UPFmodels as modelbased specifications and to derive testcases for them. The UPF framework as well as concrete policies are specified in Higherorder logic integrated in HOLTestGen. This approach has been applied in two major casestudies:
 automatic generation of testcases for firewall policies  for both stateless and stateful firewalls, and

the security policies for a largescale patient datamanagement 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:
 Rolebased Access Control
 Legitimate Relationships
 Patient's Consent
 Sealed Envelopes
The combination of these different concepts serves as a challenging scenario for modelbased 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 Website: Here
Publications:
Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. An Approach to Modular and Testable Security Models of Realworld HealthCare 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). SpringerVerlag, 2010. [PDF] [Presentation] 
Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Modelbased Firewall Conformance Testing. In Testcom/FATES 2008. Lecture Notes in Computer Science SpringerVerlag, 2008. [PDF, © SpringerVerlag] 
Achim D. Brucker and Burkhart Wolff. TestSequence Generation with HOLTestGen  With an Application to Firewall Testing. In TAP 2007: Tests And Proofs. Lecture Notes in Computer Science 4454, SpringerVerlag, 2007. [PDF,© SpringerVerlag] 
Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Verifying TestHypotheses  An Experiment in Test and Proof. In Modelbased Testing (MBT 2008). Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2008.[PDF] 
Modeling Operating and Embedded Systems
Description: The goal of this research area is to develop modeling and testing techniques for lowlevel, machine oriented computer components. This includes memory models. processor models and their embedding in a "real hardware"environment. The models are typically oriented on bitvectorrepresentations; 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. HOLBoogie  An Interactive ProverBackend for the Verified C Compiler. Journal of Automated Resoning (JAR), 44(12):111144, 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(24):349388, 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 systemlevel concurrent programs. In Verified Software: Theories, Tools, Experiments, LNCS 5295, pages 161176. Springer Berlin / Heidelberg, September 2008. [ bib  DOI  .pdf ] 
Sascha Böhme, Rustan Leino, and Burkhart Wolff. HOLBoogie  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 HigherOrder Logics (TPHOLs 2008), LNCS 5170. SpringerVerlag, 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):233247, 2005. [ bib  DOI  .pdf ] 
Nicole Rauch, Burkhart Wolff: Formalizing Java's Two'sComplement Integral Type in Isabelle/HOL. Electr. Notes Theor. Comput. Sci. 80: 4158 (2003) 
Extending the Isabelle Platform (PlugIn 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 plugin mechanisms for Isabelle ("Isabelle as an Eclipse for FM Tools"), its computational basis ("Parallel Kernel supporting asynchronous Proof Development") and new industrystrength 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 20111, 2012 and 2013.
People: Burkhart Wolff, Makarius Wenzel
Makarius Wenzel: Isabelle/jEdit – A Prover IDE within the PIDE Framework. CICM/MKM 2012, LNCS 7362, pp. 468471. 
Makarius Wenzel and Burkhart Wolff: Isabelle/PIDE as Platform for Educational Tools Thedu '11, pp 143153. 
David C. J. Matthews, Makarius Wenzel: Efficient parallel programming in Poly/ML and Isabelle/ML. DAMP 2010, pp 5362. 
Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow: The Isabelle Framework. TPHOLs 2008, LNCS pp. 3338. 
Makarius Wenzel. Isabelle as Documentoriented Proof Assistant.Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011). LNCS 6824, pp. 244259. 
Makarius Wenzel. Parallel ProofChecking 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 351366. SpringerVerlag, 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 405422. Springer Verlag, 2000. [ bib  .pdf ] 
Randombased Exploration and Testing of CPrograms
Description: In order to push ideas from randombased exploration and in order to experiment with resulting testing methods in practice, a redesign of a new release of the Auguste prototype is untertaken. Auguste was initially developed by SandrineDominique 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 reimplementation Auguste++ will appear as a plugin for the FramaC platform (http://framac.com), connected to external tools: on the one hand some tool for the uniform drawing of paths (formerly Auguste used the “MupadCombinat” ￼ 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 FramaC and will offer a test generation capability. In the following diagram, the existing machinery (including GUI) of the FramaC 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 lowlevel 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 constraintsolver 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 (“allinstructions”, “all branches”, all kloops, 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 coveragebiased” testing of August share part of the techniques (symbolic evaluation, constraintsolving, 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, MarieClaude Gaudel, Burkhart Wolff, Romain Aissat (doctorant), Alain Denise
Related Projects: Bourse Ministerielle pour la thèse de Romain Aissat
Selected Publications:
[1] Alain Denise, MarieClaude Gaudel, SandrineDominique Gouraud, Richard Lassaigne, Johan Oudinet, and Sylvain Peyronnet. Coveragebiased random exploration of large models and application to testing. STTT, International Journal on Software Tools for Technology Transfer, 14(1):7393, 2012.
[2] SandrineDominique Gouraud: Utilisation des structures combinatoires pour le test statistique,
Thèse de doctorat en Informatique, Université ParisSud, 2004.
[3] R. Majundar and K. Shen : Hybrid Concolic Testing, ICSE '07 Proceedings of the 29th international conference on Software Engineering, pages 416426 , 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 3542, 2010.[6] Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. HOLBoogie  An Interactive ProverBackend for the Verified C Compiler. Journal of Automated Resoning (JAR), 44(12):111144, 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 modelchecking.
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 nonambiguous 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 s_{0}, s_{1}, ..., s_{n}such that s_{i }is a state that is chosen uniformly at random among the successors of the state s_{i1}, 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 10^{34 }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 divideandconquer 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 statecoverage and transitioncoverage. The idea could also be applied starting from some other graph description of a system to be tested, for instance a UMLlike state machine model.
With such "coveragebiased" 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 constraintsolving (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 constraintsolvers 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 SandrineDominique Gouraud for a small subset of a "Clike" language, for the structural statistical testing of C programs.
Uniformly randomised LTL modelchecking :
In addition to the various current works mentioned above, we have generalised uniform drawing of paths to uniform drawing of socalled ``lassos'' that are interesting for MonteCarlo modelchecking 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 wellstructured programs and controlcommand systems. An immediate perspective is to embed this method in an existing modelchecker such as SPIN or CADP, with the aim of developing efficient randomised methods for LTL modelchecking with as result a guaranted probability of satisfaction of the checked formula.
Collaboration:
Equipe de Logique Mathématique de Paris 7 (Richard LASSAIGNE)
People:
Papers:
 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 2534, 2004.
 A.Denise, M.C. Gaudel, S.D. Gouraud, R.Lassaigne, and S.Peyronnet : Uniform random sampling of traces in very large models, in 1^{st}International ACM Workshop on Random Testing, pages 1019, July 2006.
 A. Denise, M.C. Gaudel, S.D. Gouraud, R. Lassaigne, J. Oudinet, and S. Peyronnet : Coveragebiased random exploration of large models and application to testing, in STTT, International Journal on Software Tools for Technology Transfer, vol. 14, pp. 7393, 2012.
 M.C. Gaudel, A. Denise, S.D. Gouraud, R. Lassaigne, J. Oudinet and S. Peyronnet : Coveragebiased random exploration of large models, in 4^{th} ETAPS Workshop on Model Based Testing, volume 220, Issue1, 10 of Electronic Notes in Theoretical Computer Science, pages 314, 2008 (invited lecture).
 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 512, 2001.
 J. Oudinet : Uniform random walks in very large models, in RT '07: Proceedings of the 2nd international workshop on Random testing}, pages 2629, Atlanta, GA, USA, November 2007. ACM Press.
 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.
 J. Oudinet, A. Denise, M.C. Gaudel, R. Lassaigne, S. Peyronnet : Uniform MonteCarlo model checking, in FASE. LNCS vol. 6603, pp. 127140, Springer, 2011.
 Johan Oudinet, Alain Denise, and MarieClaude Gaudel. A new dichotomic algorithm for the uniform random generation of words in regular languages. TCS, Theoretical Computer Science, accepted, 2012. available online