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