Tool Development Roadmap: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas |
imported>Nicolas |
||
| Line 6: | Line 6: | ||
{| border="1" | {| border="1" | ||
!Task Id | !Task Id | ||
!Deliverable | |||
!Title | !Title | ||
!Status | !Status | ||
|- | |- | ||
|3.2.1 | |3.2.1 | ||
|D3.2, D3.3, D3.4 | |||
|Answer questions from ADVANCE partners | |Answer questions from ADVANCE partners | ||
| | | | ||
|- | |- | ||
|3.2.2 | |3.2.2 | ||
|D3.2, D3.3, D3.4 | |||
|Process feature requests and platform issues | |Process feature requests and platform issues | ||
| | | | ||
|- | |- | ||
|3.2.3 | |3.2.3 | ||
|D3.2, D3.3, D3.4 | |||
|Maintain and evolve model editors | |Maintain and evolve model editors | ||
| | | | ||
|- | |- | ||
|3.2.4 | |3.2.4 | ||
|D3.2, D3.3, D3.4 | |||
|Ensure Event-B handbook consistency | |Ensure Event-B handbook consistency | ||
| | | | ||
|- | |- | ||
|3.3.1.a | |3.3.1.a | ||
|D3.2, D3.3 | |||
|Enrich SMT support for Event-B mathematical language | |Enrich SMT support for Event-B mathematical language | ||
| | | | ||
|- | |- | ||
|3.3.1.b | |3.3.1.b | ||
|D3.2, D3.3 | |||
|Assess SMT solvers effectiveness | |Assess SMT solvers effectiveness | ||
| | | | ||
|- | |- | ||
|3.3.2.a | |3.3.2.a | ||
|D3.2 | |||
|Develop specialised prover tactics for case studies | |Develop specialised prover tactics for case studies | ||
| | | | ||
|- | |- | ||
|3.3.2.b | |3.3.2.b | ||
|D3.2 | |||
|Add FAQ in handbook with tips on prover tactics | |Add FAQ in handbook with tips on prover tactics | ||
| | | | ||
|- | |- | ||
|3.3.3.a | |3.3.3.a | ||
|D3.2, D3.3 | |||
|Develop methods for combining SAT/SMT with ProB | |Develop methods for combining SAT/SMT with ProB | ||
| | | | ||
|- | |- | ||
|3.3.3.b | |3.3.3.b | ||
|D3.3 | |||
|Develop methods for state space compression and state hashing | |Develop methods for state space compression and state hashing | ||
| | | | ||
|- | |- | ||
|3.3.4.a | |3.3.4.a | ||
|D3.3 | |||
|Develop links between theory plug-in and SMT | |Develop links between theory plug-in and SMT | ||
| | | | ||
|- | |- | ||
|3.3.4.b | |3.3.4.b | ||
| | |D3.3 | ||
|Develop links between theory plug-in and ProB | |||
| | | | ||
|- | |- | ||
|3.3.4.c | |3.3.4.c | ||
|D3.3 | |||
|Develop links between theory plug-in and user tactics | |Develop links between theory plug-in and user tactics | ||
| | | | ||
|- | |- | ||
|3.4.1.a | |3.4.1.a | ||
|D3.3 | |||
|Develop a theory of real arithmetic | |Develop a theory of real arithmetic | ||
| | | | ||
|- | |- | ||
|3.4.1.b | |3.4.1.b | ||
|D3.4 | |||
|Develop other domain-specific theories for case studies | |Develop other domain-specific theories for case studies | ||
| | | | ||
|- | |- | ||
|3.4.2.a | |3.4.2.a | ||
|D3.3 | |||
|Develop enabledness-preservation proof obligations | |Develop enabledness-preservation proof obligations | ||
| | | | ||
|- | |- | ||
|3.4.2.b | |3.4.2.b | ||
|D3.3 | |||
|Link modelling of discrete behaviour with continuous behaviour | |Link modelling of discrete behaviour with continuous behaviour | ||
| | | | ||
|- | |- | ||
|3.4.2.c | |3.4.2.c | ||
|D3.3 | |||
|Develop Event-B extensions to specify temporal properties | |Develop Event-B extensions to specify temporal properties | ||
| | | | ||
|- | |- | ||
|3.4.2.d | |3.4.2.d | ||
|D3.3 | |||
|Extend UML-B plug-in to support additional UML and SysML features | |Extend UML-B plug-in to support additional UML and SysML features | ||
| | | | ||
|- | |- | ||
|3.4.3.a | |3.4.3.a | ||
|D3.3 | |||
|Develop mechanism for generic modelling and refinement patterns | |Develop mechanism for generic modelling and refinement patterns | ||
| | | | ||
|- | |- | ||
|3.4.3.b | |3.4.3.b | ||
|D3.3 | |||
|Develop patterns for modelling timing properties | |Develop patterns for modelling timing properties | ||
| | | | ||
|- | |- | ||
|3.4.3.c | |3.4.3.c | ||
|D3.3, D3.4 | |||
|Develop other modelling and refinement patterns for case studies | |Develop other modelling and refinement patterns for case studies | ||
| | | | ||
|- | |- | ||
|3.5.1.a | |3.5.1.a | ||
| | |||
|Support for composition and decomposition | |Support for composition and decomposition | ||
| | |D3.2 | ||
|- | |- | ||
|3.5.1.b | |3.5.1.b | ||
|D3.3 | |||
|Additional tool support for composition and decomposition | |Additional tool support for composition and decomposition | ||
| | | | ||
|- | |- | ||
|3.5.1.c | |3.5.1.c | ||
|D3.3 | |||
|Propagating changes in abstract models down through decomposition | |Propagating changes in abstract models down through decomposition | ||
| | | | ||
|- | |- | ||
|3.5.1.d | |3.5.1.d | ||
|D3.3 | |||
|Ensure decomposition is supported by multi-simulation framework | |Ensure decomposition is supported by multi-simulation framework | ||
| | | | ||
|- | |- | ||
|3.5.2.a | |3.5.2.a | ||
|D3.3 | |||
|Add team working support for merging proofs, | |Add team working support for merging proofs, | ||
model checking, composition and decomposition | model checking, composition and decomposition | ||
| | | | ||
|} | |} | ||
Revision as of 16:25, 5 September 2013
Task Plan
Task Status
| Task Id | Deliverable | Title | Status |
|---|---|---|---|
| 3.2.1 | D3.2, D3.3, D3.4 | Answer questions from ADVANCE partners | |
| 3.2.2 | D3.2, D3.3, D3.4 | Process feature requests and platform issues | |
| 3.2.3 | D3.2, D3.3, D3.4 | Maintain and evolve model editors | |
| 3.2.4 | D3.2, D3.3, D3.4 | Ensure Event-B handbook consistency | |
| 3.3.1.a | D3.2, D3.3 | Enrich SMT support for Event-B mathematical language | |
| 3.3.1.b | D3.2, D3.3 | Assess SMT solvers effectiveness | |
| 3.3.2.a | D3.2 | Develop specialised prover tactics for case studies | |
| 3.3.2.b | D3.2 | Add FAQ in handbook with tips on prover tactics | |
| 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 | |
| 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 | |
| 3.5.1.a | Support for composition and decomposition | D3.2 | |
| 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 merging proofs,
model checking, composition and decomposition |
