This Phd is part of the EU Integrated Project EURO-MILLS.
Abstract
System-level code (i.e. code referring to hardware such as CPU's,
MMU's, and device-drivers typically written in C) are notoriously difficult
to verify. Nevertheless they represent a rewarding target for formal
verification, since components are fairly well-described, highly critical,
and highly re-used.
Based on prior experience of model-based generating test data
with HOL-TestGen system, this Phd work attempts to adapt and extend
model-based testing techniques to operating-system level functional tests.
In particular, it has to be explored how reasonable abstractions can be found
and how restricted forms of concurrency can be effectively tested.
Context
This Phd is part of the EU Integrated Project EURO-MILLS (consisting of
14 partners in Germany, Austria, Belgium, France, the Netherlands)
whose primary goal is to provide a small virtualization platform
(based on the operating system PikeOS) intended to allow the secure
decomposition of complex embedded systems into independent components.
The secondary goal is to achieve EAL7 certification for this virtualization
platform by applying formal verification; for this purpose, a combination
of proof and test techniques is envisaged, where the Partner U-PSud plays
a major role.
Objectives
- Develop suitable, testable abstractions of the (in Isabelle developed)
Pike-OS Model to be developed in the project
- Develop specific testing techniques and infrastructure
for test-generation in the context of OS systems,
possibly by exploiting explicit parallelism in the
HOL-TestGen Test-Generation Procedure
- integrate test-data generation into the industry-oriented,
concretely used workflow in the project.
Work program
Extra information
Publications: 1 A Brucker, B Wolff: On Theorem Prover-based Testing. Accepted the 07-08- 2011.
In Formal Aspects of Computing (FAOC). DOI: DOI: 10.1007/s00165-012-0222-y. Springer, 2011. 2 A Feliachi, MC Gaudel, and B Wolff: Isabelle/Circus:
A process specification and verification environment. In VSTTE, LNCS 7152, pages 243-260, 2012. 3 M Daum, J Dörrenbächer and B Wolff: Proving Fairness and Implementation Correctness of a Microkernel Scheduler. JAR, 42(2-4), pp 349-388,2009
Prerequisite
- Knowledge in Formal Methods, Logic, Functional Programming
- Interest in Modeling and Programming with Isabelle/HOL
- English
Détails
Expected funding
Institutional funding
Status of funding
Expected
Candidates
Utilisateur
burkhart.wolff
Créé
Mardi 22 mai 2012 15:09:39 CEST
dernière modif.
Mardi 22 mai 2012 15:09:39 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