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
Laboratory LRI VALS
Collaborations Supelec / THeSys 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).
  • 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:
Prerequisite Knowledge in Embedded Systems, Formal Methods, Formal Logic, Functional Programming desirable.
Expected funding Institutional funding
Status of funding Expected
user burkhart.wolff
Created Wednesday 28 of May, 2014 16:20:13 CEST
LastModif Wednesday 28 of May, 2014 17:17:56 CEST
Attachments (0)


No attachments for this item

The original document is available at