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