Chargement...
 

Programming-Testing-Proving

Domaine
Programming-Testing-Proving
Domain - extra
Formal Semantics, Heterogenous Languages
Année
2014
Starting
1.10.2014
État
Open
Sujet
IsaTESL - Semantic Faithful Combination of Industrially used Heterogenuous Timed Specification Languages in Isabelle/HOL
Thesis advisor
WOLFF Burkhart
Co-advisors
Frederic Boulanger
NN
Laboratory
Collaborations
Supelec / THeSys Team
LRI / VALS Team
Abstract
Industrial development processes of embedded systems were usually done by heterogeneous specification formalisms, usually based on UML/SysML like descriptions. In order to allow simulation AND verification on this form of description, own simulation environments like ModHel’X [[3]] have been developed, that execute in principle an operational semantics for heterogeneous parts of a system description. This approach comes to its limits in particular if timed, event-based specifications (such as CCSL (Clock Constraints Specification Language) [[1]] and TESL (Tagged Events Specification Language) [[2]] ) were handled. However, in order to get a deeper integration of these semantics, a denotational approach (such as used in process-agebraic approaches as timed CSP, Circus, etc.) is desirable, that allows for the consistent derivation of optimized simulation rules as well as test-generation techniques.
Context
The thesis project stands at the intersection of two major research areas:

  • Simulation methods for the heterogenous modeling of embedded systems (represented by the Supelec/THeSys Team)
  • Formal verification techniques based on theorem proving and denotational
semantics for timed transition systems as in timed process algebras. (represented by the LRI / VALS Team).

The former developed the ModHel’X platform [[3]] for the simulation of heterogenous systems, which we will consider only for the case of TIMED event systems for the language TESL and its variants, captured in UML/MARTE diagrams.

The latter acquired experience in the development of formal denotational semantics for UML/OCL (a particular model is discussed as new "Appendix A" of OMG Standard; this work is pursued in a collaboration with System X with the goal of test-generation as well). Another line of experience is the use of MODULAR semantics for timed specification formalisms in UTP and circus (9,10).
Objectives
  • Development of a timed, modular semantics framework in Isabelle/HOL for behavioral semantics
  • Instantiating the framework for TESL and its variants ("semantic deviation points")
  • Deriving operational semantics ("modeles de calcul") for exemplary language pair combinations
  • Deriving test-case generation rules for an UML MARTE like language fragment.
Work program
Follows directly the objectives list.
Extra information
Detailed description and Bibliography:
https://www.lri.fr/~wolff/tmp/AllocDoc2014.doc
Prerequisite
Knowledge in Embedded Systems, Formal Methods, Formal Logic, Functional Programming desirable.
Détails
Expected funding
Institutional funding
Status of funding
Expected
Candidates
Utilisateur
burkhart.wolff
Créé
Mercredi 28 mai 2014 16:20:13 CEST
dernière modif.
Mercredi 28 mai 2014 17:17:56 CEST

Fichiers joints

 filenamecrééhitsfilesize 
Aucun fichier joint à cette fiche


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