Automata are the usual formalism decribing the BEHAVIOUR of systems-components. If behavioural descriptions do include the exchange of complex data, the traditional approach to represent automata by data-enumerations fails due to state-space explosion. An answer are SYMBOLIC AUTOMATA, whose states consists of a formula representing classes of data; symbolic states may represent infinitely many elementary states. The HOL-TestGen system (based on the theorem-prover Isabelle, but geared towards the automatic symbolic computation) is used to generate test-data from specifications in Higher-order Logic (HOL).
The goal of this Phd is to study foundational concepts of Tests (IO-conformance, IO-automata- refinement,...) in the context of HOL-TestGen, develop efficient deductive methods to handle them, inside HOL-TestGen, and to apply ecently emmerging parallelized symbolic evaluations, as a consequence of a pervasively parallel prover architecture available in the underlying Isabelle system.
Context
Symbolic Automata Processing for Test-Case Generation is a trendy research subject. The main challenges are to combine automata theory with deductive techniques, which is so far treated by very different and separated research communites. Finding effective, parallelized deductive ways to handle specific symbolic automata as arising in concrete practical problems is both a conceptual and technical challenge, in particular in a concrete system context such as HOL-TestGen.
Objectives
In this Phd, the ultimate goal is:
1) Find Compact Representation of Symbolic Automata (RegExps, LTL, CSP, StateCharts, ...) amenable to symbolic computation in HOL-TestGen;
2) Improve existing methods in HOL-TestGen to Paralellized Sequence Testing and
3) Find ways to incorporate classical sequence tests like IO-conformance, IO-automata-refinement, etc.
Work program
Extra information
A Brucker, B Wolff: On Theorem Prover-based Testing. Accepted the 07-08- 2011. In Formal Aspects of Computing (FAOC). DOI: 10.1007/s00165-012-0222-y. Springer, 2011.
D Matthews and M Wenzel. Efficient Parallel Programming in Poly/ML and Isabelle/ML. 2010.
Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. In Sacerdoti C Coen and D Aspinall (eds.). User Interfaces for Theorem Provers (UITP 2010).
Prerequisite
- Knowledge in Formal Methods and Functional Programming
- english
Détails
Expected funding
Institutional funding
Status of funding
Expected
Candidates
Utilisateur
burkhart.wolff
Créé
Mardi 22 mai 2012 15:24:28 CEST
dernière modif.
Mardi 22 mai 2012 15:24:28 CEST
Fichiers joints
filename
créé
hits
filesize
Aucun fichier joint à cette fiche
Connexion
Ecole Doctorale Informatique Paris-Sud
Directrice
Nicole Bidoit Assistante
Stéphanie Druetta Conseiller aux thèses
Dominique Gouyou-Beauchamps
ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr