Chargement...
 

Historique de fiche de formulaire

Visualiser la fiche de formulaire

Version Date Utilisateur ID du Champ Champ Difference
3 15 mai 2012 16:40 burkhart.wolff 185 Extra information
 Publications: Publications:
-[BW11] Achim D. Brucker, Burkhart 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.[FGW12]Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Isabelle/Circus: A process specification and verification environment. In VSTTE, volume 7152 of Lecture Notes in Computer Science, pages 243-260, 2012. +[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.[FGW12]A 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.
2 15 mai 2012 16:37 burkhart.wolff 180 Abstract
 In this thesis, the Isabelle/HOL-TestGen system should be extended by a component that 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. A potential approachis the Isabelle/CIRCUS language, which provides process-algebraic modeling approach to concurrency. +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 forsequence 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.
      181 Context
 wishes to extend its expertise in model-based testing techniques. wishes to extend its expertise in model-based testing techniques.
 An integral part of this Phd is therefore to apply the test-generation 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), +tools developed above to Testing critical components of the Biotroniks Pace-maker Home-Monitoring System. As an example, the Home-Monitoring System containsan efficient communication multiplexer (which is basically a prioritized multi-level Queue),
 which must satisfy critical security properties (a FIFO-Principle of ingoing/outgoing which must satisfy critical security properties (a FIFO-Principle of ingoing/outgoing
-information packages must +information packages must be preserved) as well as dead-lock and lifeness properties.
1 15 mai 2012 15:01 burkhart.wolff 225 Domain - extra
-Model-Based testing of JAVA Programs +Model-Based testing of Concurrent JAVA Programs

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