Tools

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 and Marie-Claude Gaudel. A new dichotomic algorithm for the uniform random generation of words in regular languages. TCS, Theoretical Computer Science 502:165-176, 2013. extended version of \citegascom10.
    [ BibTeX | pdf ]

    @article{TCS:2012,
	author = "Johan Oudinet and Alain Denise and Marie-Claude Gaudel",
	title = "A new dichotomic algorithm for the uniform random generation of words in regular languages",
	journal = "TCS, Theoretical Computer Science",
	year = 2013,
	volume = 502,
	pages = "165-176",
	publisher = "Elsevier",
	note = "extended version of \cite{gascom10}",
	pdf = "http://www.lri.fr/~mcg/PDF/TCSfinal.pdf"
}

  • 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 ]

    @inproceedings{FASE:2011,
	author = "Johan Oudinet and Alain Denise and Marie-Claude Gaudel and Richard Lassaigne and Sylvain Peyronnet",
	title = "Uniform {M}onte-{C}arlo model checking",
	booktitle = "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",
	publisher = "Springer Verlag",
	volume = 6603,
	series = "Lecture Notes in Computer Science",
	year = 2011,
	pages = "127-140",
	pdf = "http://www.lri.fr/~mcg/PDF/FASE.pdf",
	x-equipes = "fortesse",
	x-type = "article",
	x-support = "actes",
	x-cle-support = "A",
	type_digiteo = "conf_isbn"
}

  • Johan Oudinet. Exploration aléatoire de modèles. Journal Européen des Systèmes Automatisés (JESA) 43:905–919, November 2009. Colloque francophone sur la Modélisation des Systèmes Réactifs.
    [ BibTeX | pdf ]

    @article{oudinetJESA09,
	author = "Johan Oudinet",
	title = "Exploration al\'eatoire de mod\`eles",
	journal = "Journal Europ\'een des Syst\`emes Automatis\'es (JESA)",
	year = 2009,
	volume = 43,
	pages = "905--919",
	month = "November",
	note = "Colloque francophone sur la Mod\'elisation des Syst\`emes R\'eactifs",
	annote = "S\'el\'ectionn\'e pour soumission \`a DEDS",
	pdf = "http://rukia.lri.fr/publis/JESA09.pdf"
}
 
 

HOL-TestGen

 

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
You are here Tools