# ForTesSE Group

## Research Area: Logical Representations and Proof-based Techniques

Techniques for the automated generation of test-cases — be it from specifications in form of pre- and postconditions, from transition systems or from annotated programs — suffer from state-space explosion similarly to model-checking techniques. One possible anwer to the challenge is to use symbolic representations of models, their normal forms, symbolic states, the resulting test-cases (partitions of test-data) and constraint-solving techniques for test-data selection.

## Aims and Scope :

The proof-based testing paradigm is described by the goal to transform specifications as long as possible abstractly and normalizing them in an automated deduction process specific to the problem domain. Proof-based testing depends on the following prerequisites:

1. Logical representations are required for the various specification languages, presenting the semantics in a formal, unambiguous way, in order to allow for verified transformation rules and normalization processes.
2. Proof-environments have to be adapted in order to represent test-case generation processes as symbolic evaluation and problem-specific normalization.
3. Constraint-solvers and random-exploration methods have to be integrated into the process, in particular for the test-data selection.
4. New technologies such as fine-grained parallelization have to be integrated in the underlying symbolic computing processes in order to leverage test-case generation for large models.
5. New forms of test-driver generations have to be developed in order to improve the applicability of the approach to more application domains.

## Main achievements

• Ad 1.) we developed various semantic theories (so called "shallow embeddings") for programming and specification languages in Isabelle/HOL. Examples are UML/OCL, Z, CSP, Circus, core-languages of C like Boogie, or UPF (a special purpose language to describe security policies) in Isabelle/HOL. Rule-sets derived from these theories can be used for specification normalization, which are a pre-requisite for (efficient) test-case generation techniques.
• Ad 2), we developed the environment HOL-TestGen, (built as a kind of "plugin" in Isabelle/HOL), which provides an infrastructure for test-case generation by decomposing specifications or annotated programs into classes of data (characterized by constraint-systems or path-conditions), for constraint-solving based test-data selection and for the generation of efficient test-drivers.
• Ad 3) we integrated SMT solvers like Z3, in particular the counter-example generation facility into HOL-TestGen; a future integration of uniform random-distribution techniques such as Rukia is another line of future research.
• Ad 4), we aim to integrate parallelism into the kernel of Isabelle and similar systems in order to profit from new hardware-trends and the fact, that normal-from computations in test-case generation procedures are highly suited for parallelization.
• Ad 5), we developed for example specific test-drivers for web-service tests, future developments can also include the generation of runtime-testers for temporal properties.

## People

• Burkhart Wolff
• Marie-Claude Gaudel
• Delphine Longuet
• Matthias Krieger (- 2012)
• Abdou Feliachi
• Yakoub Nemouchi

## References

• Thierry Jéron, Margus Veanes and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021). Dagstuhl Reports 3(1):1–29, 2013.
[ BibTeX ]

@article{jron_et_al:DR:2013:4006,
author = "Thierry J{\'e}ron and Margus Veanes and Burkhart Wolff",
title = "{Symbolic Methods in Testing (Dagstuhl Seminar 13021)}",
pages = "1--29",
journal = "Dagstuhl Reports",
issn = "2192-5283",
year = 2013,
volume = 3,
number = 1,
editor = "Thierry J{\'e}ron and Margus Veanes and Burkhart Wolff",
publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
url = "http://drops.dagstuhl.de/opus/volltexte/2013/4006",
urn = "urn:nbn:de:0030-drops-40060",
doi = "10.4230/DagRep.3.1.1",
area = "logical_representations",
annote = "Keywords: Automated Deduction, White-box testing, Black-box Testing, Fuzz-Testing, Unit-Testing, Theorem prover-based Testing"
}

• Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel and Burkhart Wolff. Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. In MKM/Calculemus/DML 7961. 2013, 359-363.
[ BibTeX | pdf ]

@inproceedings{DBLP:conf/mkm/BarrasGHRTWW13,
author = "Bruno Barras and Lourdes Del Carmen Gonz{\'a}lez-Huesca and Hugo Herbelin and Yann R{\'e}gis-Gianas and Enrico Tassi and Makarius Wenzel and Burkhart Wolff",
title = "Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems",
booktitle = "MKM/Calculemus/DML",
year = 2013,
pages = "359-363",
doi = "10.1007/978-3-642-39320-4_29",
pdf = "http://www.lri.fr/~wolff/papers/conf/CICM13-PervasiveParallsm.pdf",
area = "logical_representations",
bibsource = "DBLP, http://dblp.uni-trier.de",
classification = "conference",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = 7961,
abstract = "Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semi-automated verifications of complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multicore hardware. The architecture of contemporary interactive provers such as Coq, Isabelle or the HOL family goes back to the influential LCF system from 1979, which has pioneered key principles like correctness by construction for primitive inferences and definitions, free programmability in userspace via ML, and toplevel command interaction. Both Coq and Isabelle have elaborated the prover architecture over the years, driven by the demands of sophisticated proof procedures, derived specification principles, large libraries of formalized mathematics etc. Despite this success, the operational model of interactive proof checking was limited by sequential ML evaluation and the sequential read-eval-print loop, as inherited from LCF."
}

• Achim D Brucker, Abderrahmane Feliachi, Yakoub Nemouchi and Burkhart Wolff. Test Program Generation for a Microprocessor – A Case-Study. In Proceedings of the 6th Intl. Conf. on Test and Proof (TAP '13) LNCS 7942. 2013, 76–95.
[ BibTeX | pdf ]

@inproceedings{Brucker:2013:TAP,
author = "Brucker, Achim D. and Feliachi, Abderrahmane and Nemouchi, Yakoub and Wolff, Burkhart",
title = "Test Program Generation for a Microprocessor -- A Case-Study",
booktitle = "Proceedings of the 6th Intl. Conf. on Test and Proof (TAP '13)",
series = "Lecture Notes in Computer Science",
volume = "LNCS 7942",
year = 2013,
location = "Budapest, Hungaria",
pages = "76--95",
numpages = 20,
classification = "conference",
pdf = "http://www.lri.fr/~wolff/papers/conf/2013-TapPresentation.pdf",
publisher = "Springer LNCS",
doi = "10.1007/978-3-642-38916-0_5",
area = "logical_representations",
domain = "os_test",
abstract = "Certifications of critical security or safety system properties are becoming increasingly important for a wide range of products. Certifying large systems like operating systems up to Common Criteria EAL 4 is common practice today, and higher certification levels are at the brink of becoming reality. To reach EAL 7 one has to formally verify properties on the specification as well as test the implementation thoroughly. This includes tests of the used hardware platform underlying a proof architecture to be certified. In this paper, we address the latter problem: we present a case study that uses a formal model of a microprocessor and generate test programs from it. These test programs validate that a microprocessor implements the specified instruction set correctly. We built our case study on an existing model that was, together with an operating system, developed in Isabelle/HOL. We use HOL-TestGen, a model-based testing environment which is an extension of Isabelle/HOL. We develop several conformance test scenarios, where processor models were used to synthesize test programs that were run against real hard- ware in the loop. Our test case generation approach directly benefits from the existing models and formal proofs in Isabelle/HOL.",
keywords = "test program generation, symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing"
}

• Achim D Brucker and Burkhart Wolff. Featherweight OCL: a study for the consistent semantics of OCL 2.3 in HOL. In Proceedings of the 12th Workshop on OCL and Textual Modelling. 2012, 19–24.
[ BibTeX | pdf ]

@inproceedings{Brucker:2012:FOS:2428516.2428520,
author = "Brucker, Achim D. and Wolff, Burkhart",
title = "Featherweight OCL: a study for the consistent semantics of OCL 2.3 in HOL",
booktitle = "Proceedings of the 12th Workshop on OCL and Textual Modelling",
series = "OCL '12",
year = 2012,
isbn = "978-1-4503-1799-3",
location = "Innsbruck, Austria",
pages = "19--24",
numpages = 6,
url = "10.1145/2428516.2428520",
doi = "10.1145/2428516.2428520",
acmid = 2428520,
pdf = "http://www.lri.fr/~wolff/papers/workshop/featherweight-ocl.pdf",
publisher = "ACM",
address = "New York, NY, USA",
area = "logical_representations",
domain = "os_test",
classification = "conference",
keywords = "HOL-OCL, OCL, formal semantics"
}

• Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel. Isabelle/Circus. Archive of Formal Proofs, 2012. \urlhttp://afp.sourceforge.net/entries/Circus.shtml, Formal proof development.
[ BibTeX ]

@article{Feliachi-Wolff-Gaudel-AFP12,
author = "Abderrahmane Feliachi and Burkhart Wolff and Marie-Claude Gaudel",
title = "Isabelle/Circus",
journal = "Archive of Formal Proofs",
month = "",
year = 2012,
note = "\url{http://afp.sourceforge.net/entries/Circus.shtml}, Formal proof development",
area = "logical_representations",
abstract = "The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's Unifying Theories of Programming (UTP). Isabelle/Circus is a formalization of the UTP and the Circus language in Isabelle/HOL. It contains proof rules and tactic support that allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). The Isabelle/Circus environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus. This article contains an extended version of corresponding VSTTE Paper together with the complete formal development of its underlying commented theories.",
issn = "2150-914x"
}

• Achim D Brucker, Lukas Brügger, Matthias P Krieger and Burkhart Wolff. HOL-TestGen 1.7.0 User Guide. Number 1551, Laboratoire en Recherche en Infromatique (LRI), Université Paris-Sud 11, France, 2012.
[ BibTeX | pdf ]

@techreport{ brucker.ea:hol-testgen:2012,
author = {Achim D. Brucker and Lukas Br{\"u}gger and Matthias P. Krieger and Burkhart Wolff},
institution = "Laboratoire en Recherche en Infromatique (LRI), Universit\'e Paris-Sud 11, France",
language = "USenglish",
month = "",
title = "{HOL-TestGen} 1.7.0 User Guide",
categories = "testing,holtestgen",
classification = "unrefereed",
areas = "formal methods, software",
keywords = "symbolic test case generations, black box testing, theorem proving, Isabelle/HOL",
year = 2012,
number = 1551,
area = "logical_representations",
num_pages = 120,
public = "yes",
url = "http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2012"
}

• Abderrahmane Feliachi, Marie-Claude Gaudel and Burkhart Wolff. Isabelle/Circus: A Process Specification and Verification Environment. In VSTTE LNCS 7152. 2012, 243-260.
[ BibTeX | pdf ]

@inproceedings{feliachigw12,
author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff",
title = "Isabelle/{C}ircus: A Process Specification and Verification Environment",
booktitle = "VSTTE",
year = 2012,
pages = "243-260",
series = "Lecture Notes in Computer Science",
volume = "LNCS 7152",
isbn = "978-3-642-27704-7",
ee = "http://dx.doi.org/10.1007/978-3-642-27705-4_20",
doi = "10.1007/978-3-642-27705-4_20",
abstract = {The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's unifying theories of programming (UTP). We develop a machine-checked, formal semantics based on a "shallow embedding" of Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and imple- ment tactic support that finally allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). This proof environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus.},
pdf = "http://www.lri.fr/~wolff/papers/conf/VSTTE-IsabelleCircus11.pdf",
classification = "conference",
area = "logical_representations",
bibsource = "DBLP, http://dblp.uni-trier.de",
crossref = "DBLP:conf/vstte/2012",
x-equipes = "fortesse",
x-type = "article",
x-support = "actes"
}

• 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. Series Proceedings of the ACM Symposium on Access control models and technologies, ACM, 2011, pages 133-142. SACMAT 2011.
[ BibTeX | pdf ]

@incollection{2011-sacmat-mbtsec-npfit,
author = {Achim D. Brucker and Lukas Br\"ugger and Paul Kearney and Burkhart Wolff},
title = "An Approach to Modular and Testable Security Models of Real-world Health-Care Applications",
pages = "133-142",
publisher = "ACM",
year = 2011,
series = "Proceedings of the ACM Symposium on Access control models and technologies",
abstract = "We present a generic modular policy modelling framework and instantiate it with a substantial case study for model- based testing of some key security mechanisms of applications and services of the NPfIT. NPfIT, the National Programme for IT, is a very large-scale development project aiming to modernise the IT infrastructure of the National Health Service (NHS) in England. Consisting of heteroge- neous and distributed applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features. We model the four information governance principles, comprising a role-based access control model, as well as policy rules governing the concepts of patient consent, sealed en- velopes and legitimate relationships. The model is given in Higher-order Logic (HOL) and processed together with suitable test specifications in the HOL-TestGen system, that generates test sequences according to them. Particular em- phasis is put on the modular description of security poli- cies and their generic combination and its consequences for model-based testing.",
note = "SACMAT 2011",
doi = "10.1145/1998441.1998461",
area = "logical_representations",
}

• Abderrahmane Feliachi, Marie-Claude Gaudel and Burkhart Wolff. Unifying Theories in Isabelle/HOL. In Unifying Theories of Programming (UTP2010). Series Lecture Notes in Computer Science, volume to appear, number 6445, Springer-Verlag, November 2010, pages 188-206. 20 pages.
[ BibTeX | pdf ]

@incollection{feliachi:uznifying-theories:2010,
title = "{U}nifying {T}heories in {I}sabelle/{HOL}",
abstract = "In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and xsCircus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation. \keywords{UTP, Theorem Proving, Isabelle/HOL, CSP, Circus}",
keywords = "UTP, Theorem Proving, Symbolic test case generations, Isabelle/HOL",
author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff",
booktitle = "Unifying Theories of Programming {(UTP2010)}",
language = "USenglish",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
number = 6445,
classification = "conference",
ee = "http://dx.doi.org/10.1007/978-3-642-16690-7_9",
year = 2010,
doi = "10.1007/978-3-642-16690-7_9",
pdf = "http://www.lri.fr/~wolff/papers/conf/2010-utp-unifying-theories.pdf",
area = "logical_representations",
public = "yes",
volume = "to appear",
month = "November",
note = "20 pages",
x-equipes = "fortesse",
x-type = "article",
x-support = "actes",
x-cle-support = "B",
type_digiteo = "conf_isbn",
pages = "188-206"
}

• 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) 6627. 2010. LNCS 6627.
[ BibTeX | pdf ]

@inproceedings{Brucker.ea:SpecificationBased:2010,
author = "Achim D. Brucker and Matthias P. Krieger and Delphine Longuet and Burkhart Wolff",
title = "{A} {S}pecification-based {T}est {C}ase {G}eneration {M}ethod for {UML}/{OCL}",
abstract = "Automated test data generation is an important method for the verification and validation of UML/OCL specifications. In this paper, we present an extension of DNF-based test case generation methods to class models and recursive query operations on them. A key feature of our approach is an implicit representation of object graphs avoiding a repre- sentation based on object-id's; thus, our approach avoids the generation of isomorphic object graphs by using a concise and still human-readable symbolic representation.",
pdf = "http://www.lri.fr/~wolff/papers/workshop/ocl-testing.pdf",
booktitle = "Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010)",
classification = "conference",
year = 2010,
doi = "10.1007/978-3-642-21210-9_33",
area = "logical_representations",
note = "LNCS 6627",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = 6627
}

• 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.
[ BibTeX | pdf ]

@article{brucker.ea:2010,
author = {Achim D. Brucker and Lukas Br\"ugger and Paul Kearney and Burkhart Wolff},
journal = "Software Testing, Verification, and Validation, 2010 International Conference on",
volume = 0,
title = "{V}erified {F}irewall {P}olicy {T}ransformations for {T}est {C}ase {G}eneration",
year = 2010,
isbn = "978-0-7695-3990-4",
pages = "345-354",
publisher = "IEEE Computer Society",
booktitle = "International Conference on Software Testing {(ICST10)}",
location = "Paris, France",
editor = "Ana Cavalli and Sudipto Ghosh",
classification = "conference",
doi = "10.1109/ICST.2010.50",
address = "Los Alamitos, CA, USA",
area = "logical_representations",
abstract = "We present an optimization technique for model-based generation of test cases for firewalls. Based on a formal model for firewall policies in higher-order logic, we derive a collection of semantics-preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage. The correctness of the rules and the algorithm is established by formal proofs in Isabelle/\acs{hol}. Finally, we use the normalized policies to generate test cases with the domain-specific firewall testing tool \testgenFW. The resulting procedure is characterized by a gain in efficiency of two orders of magnitude and can handle configurations with hundreds of rules as occur in practice. Our approach can be seen as an instance of a methodology to tame inherent state-space explosions in test case generation for security policies."
}

• Achim D Brucker and Burkhart Wolff. On Theorem Prover-based Testing. Formal Asp. Comput. (FAOC) 25(5):683–721, 2013.
[ BibTeX | pdf ]

@article{brucker.ea:2012,
author = "Achim D. Brucker and Burkhart Wolff",
title = "On {T}heorem {P}rover-based {T}esting",
journal = "Formal Asp. Comput. (FAOC)",
year = 2013,
month = "",
volume = 25,
number = 5,
pages = "683--721",
abstract = "\emph{HOL-TestGen} is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.",
pdf = "http://www.lri.fr/~wolff/papers/journals/brucker.ea-hol-testgen-2008.rev-1.pdf",
keywords = "Isabelle/HOL, Theorem proving, Model-based Testing, Program-based Testing, Testcase Generation",
doi = "10.1007/s00165-012-0222-y",
area = "logical_representations",
classification = "journal"
}

• Achim D Brucker and Burkhart Wolff. Semantics, Calculi, and Analysis for Object-Oriented Specifications. Acta Informatica 46(4):255–284, 2009.
[ BibTeX | pdf ]

@article{brucker.ea:2009,
author = "Achim D. Brucker and Burkhart Wolff",
title = "{S}emantics, {C}alculi, and {A}nalysis for {O}bject-{O}riented {S}pecifications",
journal = "Acta Informatica",
volume = 46,
number = 4,
pages = "255--284",
year = 2009,
abstract = "We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/HOL and the language is oriented towards OCL formulae in the context of UML class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.",
pdf = "http://www.lri.fr/~wolff/papers/journals/acta-holocl.pdf",
keywords = "UML , OCL , object-oriented specification , refinement , formal methods",
doi = "10.1007/s00236-009-0093-8",
area = "logical_representations",
classification = "journal"
}

• 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)..
[ BibTeX | pdf ]

@article{daum.ea:fairness:2009,
author = {Matthias Daum and Jan D\"{o}rrenb\"{a}cher and Burkhart Wolff},
title = "{P}roving {F}airness and {I}mplementation {C}orrectness of a {M}icrokernel {S}cheduler",
journal = "Journal of Automated Reasoning (JAR)",
volume = 42,
number = "2--4",
year = 2009,
pdf = "http://www.lri.fr/~wolff/papers/journals/pre-fairness.pdf",
pages = "349--388",
publisher = "Springer Verlag",
abstract = "We report on the formal proof of a microkernel's key property, namely the fairness property of its multi-priority process scheduler. The proof architecture links a layer of behavioral reasoning over system-trace sets with a concrete, fairly realistic implementation written in C. Our microkernel provides an infra-structure for memory virtualization, for communication with hardware devices, for processes (represented as a sequence of assembler instructions, which are executed concurrently over an underlying, formally defined processor), and for inter-process communication (IPC) via synchronous message passing. The kernel establishes process switches according to IPCs and timer-events; however, the scheduling of process switches follows a hierarchy of priorities, favoring, e. g., system processes over application processes over maintenance processes. Besides the quite substantial models developed in Isabelle/HOL and the formal clarification of their relationship, we provide a detailed analysis what formal requirements a microkernel imposes on the key ingredients (hardware, timers, machine-dependent code) in order to establish the correct operation of the overall system. On the methodological side, we show how early modeling with hindsight to the later verification has substantially helped our project.",
doi = "10.1007/s10817-009-9119-8",
note = "G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008).",
keywords = "Microkernel, Formal verification, Interactive theorem proving, Isabelle/HOL",
area = "logical_representations",
classification = "journal"
}


## Activities in this research area in more detail:

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

You are here