The widely used programming language JAVA supports concurrency by allowing thread creation and
synchronization on objects. Concurrent programs are notoriously difficult to verify, be it by
proof or testing techniques.
Some approaches, however, have been explored based on symbolic test-case generation techniques, mostly based on symbolic evaluation (JavaPathFinderSE (sequential algorithms), Pexx (sequential algorithms), Chalice (Proofs)).
In this thesis, the Isabelle/HOL-TestGen system should be extended by a component that
allows to model JAVA-like concurrent programs and to generate tests for them.
One potential approach is to extend the existing Monad-library in HOL-TestGen (used for
sequence testing) by suitable combinators for interleaving and synchronization.Another potential approach is to use the Isabelle/CIRCUS language, which provides process-algebraic modeling approach to concurrency, and to extend it by support for similar
mechanisms.
Context
This thesis is in the context of a collaboration with the Biotronik Gmbh that is
a major producer of medical systems. Biotronik underlies particularly high
high standards of software quality and certification; the company therefore
wishes to extend its expertise in model-based testing techniques.
An integral part of this Phd is therefore to apply the test-generation
tools developed above to Testing critical components of the Biotroniks Pace-maker
Home-Monitoring System. As an example, the Home-Monitoring System contains
an efficient communication multiplexer (which is basically a prioritized multi-level Queue),
which must satisfy critical security properties (a FIFO-Principle of ingoing/outgoing
information packages must be preserved) as well as dead-lock and lifeness properties.
Objectives
- Develop a new method to symbolic test-case generation of concurrent program
of non-trivial size (2000 loc)
- Apply the approach for a realistic case-study provided by Biotronik Gmbh
- The goal is not to support full Java - rather a small subset containing the essentials
defined for the case studies.
Work program
- Selecting a means to represent and abstract concurrent JAVA programs
- Building theories
Extra information
Publications: BW11 A D. 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. FGW12A Feliachi, M-C Gaudel, and B Wolff. Isabelle/Circus: A process specification and verification environment. In VSTTE, volume 7152 of Lecture Notes in Computer Science, pages 243-260, 2012. LSB 09 ]D Leijen, W Schulte, and S Burckhardt: The design of a task parallel library.
In Oopsla09.
Prerequisite
- Interest in functional programming and formal modeling
- Interest in proof techniques (in Isabelle)
- Interest in working at least part-time (a few months over
the duration of the project) at the site of the project partner
- knowledge in english.
Détails
Expected funding
Research contract
Status of funding
Expected
Candidates
Utilisateur
burkhart.wolff
Créé
Mardi 15 mai 2012 14:45:20 CEST
dernière modif.
Mardi 15 mai 2012 16:40:38 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