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.