This page outlines major tool-developments of the group ForTesSE. They have been used as basis for several case studies:
- Rukia is a C++ library for model exploration by uniform random walk.
- HOL-TestGen is a test case generator, built on top of Isabelle/HOL, for theorem-proving based unit and sequence testing.
- The group also makes major contributions to Isabelle/HOL as a modeling platform as well as implementation framework for Formal Methods Tools.
- Auguste++ is a white-box statistical testing tool for C programs.
Rukia - Random Uniform Walk in Automata
-
Description: Rukia is a C++ library to explore graphical models by generating at random paths in automata. Instead of using an isotropic random walk (i.e., choosing the next state uniformly at random among the successors of the current state), Rukia guides the random walk to guarantee a global uniform distribution among the elements to be covered, whatever the model topology. To do that, Rukia uses combinatorial techniques to count the number of elements to be covered and then guide the model exploration in order to maximize the minimal probability of covering one of those elements. One particularity of Rukia is the use of space-efficient algorithms that leverage the limitation on the size of model and the length of paths that can be generated with this approach (See, for example, the Dichopile algorithm). Thus, it was possible to generate paths of length 4000 in an automaton with more than 12 million states.
Currently, Rukia supports the following coverage criteria:- All paths of length n (there is a trick to also allow all paths of length less or equal to n)
- All lassos (kind of paths that end by a cycle -- useful for Monte Carlo model-checking)
- An extension is under development for handling additional criteria besides "all paths" : "all edges" and "all vertices" and maybe criteria describing other sets of edges or vertices.
- Author: Johan Oudinet
- IPR: Rukia is a free software under Lesser GNU Public license (LGPL). Rukia is also deposited in the Agency for the protection of programs (APP) IDDN.FR.001.350014.000.S.C.2009.000.00000.
- Website: http://rukia.lri.fr/
References
Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Richard Lassaigne and Sylvain Peyronnet. Uniform Monte-Carlo model checking. In Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 6603. 2011, 127-140.
[ BibTeX | pdf ]
-
Description: HOL-TestGen is a is a test case generator for specification based unit testing. HOL-TestGen is built on top of the specfication and theorem proving environment Isabelle/HOL.
-
HOL-TestGen allows one to
- write test specifications in Higher-order logics (HOL)
- (semi-) automatically partition the input space, resulting in abstract test cases
- automatically select concrete test data
- automatically generate test scripts (in SML)
- using a foreign language interface, implementations in arbitrary languages (e.g. C, C#, OCaml, Scala) can be tested.
- Authors: Achim D. Brucker, Lukas Brügger, Matthias Krieger, and Burkhart Wolff
- IPR: HOL-TestGen is free software; you can redistribute it and/or modify it under the terms of a BSD-style licence. HOL-TestGen has been deposited in the Agency for the protection of programs (APP) IDDN.FR.001.220032.000.S.A.2011.000.10000 (Signed Paris, 3.6. 2011)
- Website: Here.
- Download: hol-testgen-1.5.0.tar.gz. Developper snapshots can be received on demand.
-
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.
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) ()
-
Achim D. Brucker and Lukas Brügger and Matthias P. Krieger and Burkhart Wolff. HOL-TestGen 1.5.0 User Guide. ETH Zurich, Technical Report 670, 2010. (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (
)
-
Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. Verified Firewall Policy Transformations for Test-Case Generation. In Third International Conference on Software Testing, Verification, and Validation (ICST), pages 345-354, 2010. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1109/ICST.2010.50) (
)
-
Achim D. Brucker and Matthias P. Krieger and Delphine Longuet and Burkhart Wolff. A Specification-based Test Case Generation Method for UML/OCL. In MODELS 2010 Workshops. Lecture Notes in Computer Science (6627), pages 334-348, Springer-Verlag , 2010. Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (
)
-
Achim D. Brucker and Burkhart Wolff. HOL-TestGen: An Interactive Test-case Generation Framework. In Fundamental Approaches to Software Engineering (FASE09). Lecture Notes in Computer Science (5503), pages 417-420, Springer-Verlag , 2009. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1007/978-3-642-00593-0_28) (
)
-
Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Verifying Test-Hypotheses: An Experiment in Test and Proof. In Electronic Notes in Theoretical Computer Science, 220 (1), pages 15-27, 2008. Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008) (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1016/j.entcs.2008.11.003) (
)
-
Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Model-based Firewall Conformance Testing. In Testcom/FATES 2008. Lecture Notes in Computer Science (5047), pages 103-118, Springer-Verlag , 2008. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1007/978-3-540-68524-1_9) (
)
-
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), pages 149-168, Springer-Verlag , 2007. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1007/978-3-540-73770-4_9) (
)
-
Achim D. Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 User Guide. ETH Zurich, Technical Report 482, 2005. (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (
)
-
Achim D. Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Formal Approaches to Testing of Software. Lecture Notes in Computer Science (3997), Springer-Verlag , 2005. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1007/11759744_7) (
)
-
Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. ETH Zurich, Technical Report 449, 2004. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (
)
-
Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Formal Approaches to Testing of Software. Lecture Notes in Computer Science (3395), pages 16-32, Springer-Verlag , 2004. (abstract) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1007/b106767) (
)
-
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.
-
Auguste++ - Random-based Testing of C-Programs
- Description: Auguste will appear as a plug-in for the Frama-C platform, 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 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.
- People: Sandrine Gouraud (past prototype), Frederic Voisin
- Related Activity: Random-based Exploration and Testing of C-Programs
- Download: NOT AVAILABLE YET