Tracker Item History

Not logging

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

Version	Date	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.

Log In

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