Loading...
 
[Show/Hide Left Column]

Sujets Help

Print History View Items
No Tabs
ViewCommentsAttachments (0)

View Item

Domain Programming-Testing-Proving
Domain - extra Formal Semantics, Heterogenous Languages
Year 2014
Starting 1.10.2014
Status Open
Subject IsaTESL - Semantic Faithful Combination of Industrially used Heterogenuous Timed Specification Languages in Isabelle/HOL
Thesis advisor WOLFF Burkhart
Co-advisors Frederic Boulanger
NN
Laboratory LRI VALS
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.
Details
Expected funding Institutional funding
Status of funding Expected
Candidates
user burkhart.wolff
Created Wednesday 28 of May, 2014 16:20:13 CEST
LastModif Wednesday 28 of May, 2014 17:17:56 CEST


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 at lri.fr