Loading...
 
[Show/Hide Left Column]

Tracker Item History Help

Close
warningNot logging
Tracker changes are not being logged: Go to Action log admin to enable

Version Date User Field ID Field Old New
12 14:43 181 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).
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).
12 14:43 183 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.
  • 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.
11 14:43 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 14:43 181 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 approaches for timed specification formalisms in UTP and circus (9
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).
9 14:43 181 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 approaches for timed specification formalisms in UTP and circus [
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 approaches for timed specification formalisms in UTP and circus (9
8 14:43 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.
8 14:43 181 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 approaches for timed specification formalisms in UTP and circus [
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 approaches for timed specification formalisms in UTP and circus [
6 14:43 181 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 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 approaches for timed specification formalisms in UTP and circus [
6 14:43 182 Work program sdgf
Follows directly the objectives list.
5 14:43 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 14:43 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 14:43 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.
3 14:43 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 14:43 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 14:43 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 at lri.fr