Chargement...
 

Historique de fiche de formulaire


Version Date Utilisateur ID du Champ Champ Difference
12 181 Context
 * Simulation methods for the heterogenous modeling of embedded systems (represented by the Supelec/THeSys Team) * Simulation methods for the heterogenous modeling of embedded systems (represented by the Supelec/THeSys Team)
 * Formal verification techniques based on theorem proving and denotational  * 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). semantics for timed transition systems as in timed process algebras. (represented by the LRI / VALS Team).
      183 Objectives
 * Development of a timed, modular semantics framework in Isabelle/HOL for behavioral semantics * Development of a timed, modular semantics framework in Isabelle/HOL for behavioral semantics
 * Instantiating the framework for TESL and its variants (""""semantic deviation points"""") * Instantiating the framework for TESL and its variants (""""semantic deviation points"""")
 * Deriving operational semantics (""""modeles de calcul"""") for exemplary language pair combinations * Deriving operational semantics (""""modeles de calcul"""") for exemplary language pair combinations
 * Deriving test-case generation rules for an UML MARTE like language fragment. * Deriving test-case generation rules for an UML MARTE like language fragment.
11 183 Objectives
-xdfg +* 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.
10 181 Context
 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 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 approaches for timed specification formalisms in UTP and circus (9 +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).
9 181 Context
 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 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 approaches for timed specification formalisms in UTP and circus [[ +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 approaches for timed specification formalisms in UTP and circus (9
8 180 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. +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.
      181 Context
 The thesis project stands at the intersection of two major research areas: 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) +* Simulation methods for the heterogenous modeling of embedded systems (represented by the Supelec/THeSys Team)
 * Formal verification techniques based on theorem proving and denotational  * Formal verification techniques based on theorem proving and denotational
 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 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 approaches for timed specification formalisms in UTP and circus [ +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 approaches for timed specification formalisms in UTP and circus [[
6 181 Context
 The thesis project stands at the intersection of two major research areas: 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) +* 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). +* 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 approaches for timed specification formalisms in UTP and circus [
      182 Work program
-sdgf +Follows directly the objectives list.
5 180 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. +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.
4 180 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. +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.
3 180 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, in particular if it comes to the treatment of timed events (such as CCSL (Clock Constraints Specification Language) """"[1]"""" and TESL (Tagged Events Specification Language) """"[2]"""" ). 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. +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.
      181 Context
-dfgh +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).
2 180 Abstract
-Industrial development processes were usually done by heterogeneous specification formalism, usually done by 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, in particular if it comes to the treatment of timed events (such as CCSL (Clock Constraints Specification Language) [1] and TESL (Tagged Events Specification Language) [2] ). 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. +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, in particular if it comes to the treatment of timed events (such as CCSL (Clock Constraints Specification Language) """"[1]"""" and TESL (Tagged Events Specification Language) """"[2]"""" ). 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.
1 180 Abstract
-dfg +Industrial development processes were usually done by heterogeneous specification formalism, usually done by 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, in particular if it comes to the treatment of timed events (such as CCSL (Clock Constraints Specification Language) [1] and TESL (Tagged Events Specification Language) [2] ). 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.

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