Tool Development Roadmap: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas |
imported>Tommy mNo edit summary |
||
| (2 intermediate revisions by one other user not shown) | |||
| Line 11: | Line 11: | ||
!Status | !Status | ||
|- | |- | ||
|rowspan="4"|Platform maintenance | |rowspan="4"|'''Platform maintenance'''<br/>[Systerel / Düsseldorf] | ||
|3.2.1 | |3.2.1 | ||
|D3.2, D3.3, D3.4 | |D3.2, D3.3, D3.4 | ||
| Line 32: | Line 32: | ||
| | | | ||
|- | |- | ||
|rowspan="9"|Automated Proof and Model-checking | |rowspan="9"|'''Automated Proof and Model-checking'''<br/>[Systerel / Düsseldorf / Southampton] | ||
|3.3.1.a | |3.3.1.a | ||
|D3.2, D3.3 | |D3.2, D3.3 | ||
| Line 78: | Line 78: | ||
| | | | ||
|- | |- | ||
|rowspan="9"|Language extension | |rowspan="9"|'''Language extension'''<br/>[Southampton / Systerel / Düsseldorf / All Partners] | ||
|3.4.1.a | |3.4.1.a | ||
|D3.3 | |D3.3 | ||
| Line 124: | Line 124: | ||
| | | | ||
|- | |- | ||
|rowspan="5"|Composition and decomposition | |rowspan="5"|'''Composition and decomposition'''<br/>[Southampton / Düsseldorf / Systerel] | ||
|3.5.1.a | |3.5.1.a | ||
|D3.2 | |D3.2 | ||
| Line 151: | Line 151: | ||
| | | | ||
|- | |- | ||
|rowspan="6"|Multi-simulation framework development | |rowspan="6"|'''Multi-simulation framework development'''<br/>[Southampton / Düsseldorf] | ||
|4.2.1.a | |4.2.1.a | ||
|D4.2 | |D4.2 | ||
| Line 182: | Line 182: | ||
| | | | ||
|- | |- | ||
|rowspan="5"|Model simulation with ProB | |rowspan="5"|'''Model simulation with ProB'''<br/>[Düsseldorf] | ||
|4.3.1.a | |4.3.1.a | ||
|D4.2 | |D4.2 | ||
| Line 208: | Line 208: | ||
| | | | ||
|- | |- | ||
|rowspan="4"|Model-based testing | |rowspan="4"|'''Model-based testing'''<br/>[Düsseldorf / Southampton] | ||
|4.4.1.a | |4.4.1.a | ||
|D4.3 | |D4.3 | ||
| Line 229: | Line 229: | ||
| | | | ||
|- | |- | ||
|rowspan="4"|Code generation | |rowspan="4"|'''Code generation'''<br/>[Southampton / Düsseldorf] | ||
|4.5.1.a | |4.5.1.a | ||
|D4.2 | |D4.2 | ||
Latest revision as of 09:50, 12 September 2013
Task Plan
Task Status
| Task | Task Id | Deliverable | Title | Status |
|---|---|---|---|---|
| Platform maintenance [Systerel / Düsseldorf] |
3.2.1 | D3.2, D3.3, D3.4 | Answer questions from ADVANCE partners | Done, covered in D3.3. |
| 3.2.2 | D3.2, D3.3, D3.4 | Process feature requests and platform issues | Done, covered in D3.3. | |
| 3.2.3 | D3.2, D3.3, D3.4 | Maintain and evolve model editors | Done, covered in D3.3. | |
| 3.2.4 | D3.2, D3.3, D3.4 | Ensure Event-B handbook consistency | ||
| Automated Proof and Model-checking [Systerel / Düsseldorf / Southampton] |
3.3.1.a | D3.2, D3.3 | Enrich SMT support for Event-B mathematical language | Done, covered in D3.3. |
| 3.3.1.b | D3.2, D3.3 | Assess SMT solvers effectiveness | Done, covered in D3.3. | |
| 3.3.2.a | D3.2 | Develop specialised prover tactics for case studies | Not done yet, expecting feedback from case studies | |
| 3.3.2.b | D3.2 | Add FAQ in handbook with tips on prover tactics | Partially done, paragraph exists: [1], to be enriched | |
| 3.3.3.a | D3.2, D3.3 | Develop methods for combining SAT/SMT with ProB | ||
| 3.3.3.b | D3.3 | Develop methods for state space compression and state hashing | ||
| 3.3.4.a | D3.3 | Develop links between theory plug-in and SMT | ||
| 3.3.4.b | D3.3 | Develop links between theory plug-in and ProB | ||
| 3.3.4.c | D3.3 | Develop links between theory plug-in and user tactics | ||
| Language extension [Southampton / Systerel / Düsseldorf / All Partners] |
3.4.1.a | D3.3 | Develop a theory of real arithmetic | |
| 3.4.1.b | D3.4 | Develop other domain-specific theories for case studies | ||
| 3.4.2.a | D3.3 | Develop enabledness-preservation proof obligations | ||
| 3.4.2.b | D3.3 | Link modelling of discrete behaviour with continuous behaviour | ||
| 3.4.2.c | D3.3 | Develop Event-B extensions to specify temporal properties | ||
| 3.4.2.d | D3.3 | Extend UML-B plug-in to support additional UML and SysML features | ||
| 3.4.3.a | D3.3 | Develop mechanism for generic modelling and refinement patterns | ||
| 3.4.3.b | D3.3 | Develop patterns for modelling timing properties | ||
| 3.4.3.c | D3.3, D3.4 | Develop other modelling and refinement patterns for case studies | ||
| Composition and decomposition [Southampton / Düsseldorf / Systerel] |
3.5.1.a | D3.2 | Support for composition and decomposition | |
| 3.5.1.b | D3.3 | Additional tool support for composition and decomposition | ||
| 3.5.1.c | D3.3 | Propagating changes in abstract models down through decomposition | ||
| 3.5.1.d | D3.3 | Ensure decomposition is supported by multi-simulation framework | ||
| 3.5.2.a | D3.3 | Add team working support for comparing and merging proofs,
model checking, composition and decomposition |
||
| Multi-simulation framework development [Southampton / Düsseldorf] |
4.2.1.a | D4.2 | Experimental prototypes | |
| 4.2.1.b | D4.2 | Support co-simulation of composite system model | ||
| 4.2.1.c | D4.2 | Explore technologies for simulation of continuous models | ||
| 4.2.1.d | D4.2 | Elaborate the specification of the multi-simulation framework | ||
| 4.2.2.a | D4.3 | Develop robust, flexible multi-simulation framework | ||
| 4.2.2.b | D4.4 | Develop guidelines on effective usage of the multi-simulation framework | ||
| Model simulation with ProB [Düsseldorf] |
4.3.1.a | D4.2 | Improve scalability of ProB with large hardware: analysis & development | |
| 4.3.1.b | D4.3 | Improve scalability of ProB with large hardware: performance tuning | ||
| 4.3.2.a | D4.3 | Improve the constraint-solving kernel of ProB | ||
| 4.3.3.a | D4.3 | BMotion Studio support for case studies | ||
| 4.3.3.b | D4.4 | Prototypes for visualisation of large state-spaces and event-trace sets | ||
| Model-based testing [Düsseldorf / Southampton] |
4.4.1.a | D4.3 | Extend Model-based testing framework to accommodate random testing | |
| 4.4.2.a | D4.3, D4.4 | Scenario-based testing | ||
| 4.4.3.a | D4.3 | Coverage detection: specific coverage criteria | ||
| 4.4.3.b | D4.4 | Coverage detection: user annotations | ||
| Code generation [Southampton / Düsseldorf] |
4.5.1.a | D4.2 | Enrich the translation rule set from case studies | |
| 4.5.1.b | D4.3 | Continue to extend translation rule set | ||
| 4.5.2.a | D4.3 | Link code generation to multi-simulation framework | ||
| 4.5.3.a | D4.3 | Generation of stand-alone prototypes |
