Automata are the usual formalism decribing the BEHAVIOUR of systems-components, be it modules, protocols, or entire web-services, for example.
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 lay the foundation
of a practically useable testing framework for (reactive) sequence test in HOL-Tes
Context
Symbolic Automata Processing for Test-Case Generation is a trendy research
subject (see 1,2,3). 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 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-TestGen4.
Objectives
In this Phd, the ultimate goal is:
- Find Compact Representation of Symbolic Automata (RegExps, LTL, CSP, ...)
amenable to symbolic computation in HOL-TestGen
- Improve existing methods in HOL-TestGen to Sequence Testing
and
- Find ways to incorporate classical sequence tests like IO-conformance,
IO-automata-refinement, ...
Work program
- Development of Isabelle-Theories adressing the research goals.
- Implementation of Symbolic Computation procedures in form of
Tactics in HOL-testGen
- Applying techniques to speed-up (abstraction, theory-specialization,
parallel evaluation)
- Evaluation of the achievements in medium-suze case-studies.
Extra information
1Margus Veanes and Nikolaj Bjorner, Alternating Simulation and IOCO, in ICTSS'10, Springer Verlag, November 2010 2 C. Constant, T. Jéron, H. Marchand, V. Rusu, Integrating formal verification and conformance testing for reactive systems, IEEE Transactions on Software Engineering, 33(8):558-574, Août 2007. 3 Achim D. Brucker and Burkhart Wolff. Test-sequence generation with hol-testgen - with an application to firewall testing. LNCS 4454. TAP 2007. 4www.brucker.ch/projects/hol-testge
Prerequisite
Prior knowledge in Logic and functional programming (OCaml, SML, Haskell).
Interest in Formal Theory Development with Isabelle.
Interest in Theorem Proving and Symbolic Computation.
Détails
Expected funding
Institutional funding
Status of funding
Expected
Candidates
Utilisateur
Créé
Vendredi 03 juin 2011 11:10:59 CEST
dernière modif.
Vendredi 03 juin 2011 11:14:23 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