Difference between revisions of "Tool Development Roadmap"
From Event-B
Jump to navigationJump to searchimported>Nicolas m (→Task Status) |
imported>Nicolas m (→Task Status) |
||
| Line 26: | Line 26: | ||
|- | |- | ||
|3.3.1.a | |3.3.1.a | ||
| − | | | + | |Enrich SMT support for Event-B mathematical language |
| | | | ||
|- | |- | ||
|3.3.1.b | |3.3.1.b | ||
| − | | | + | |Assess SMT solvers effectiveness |
| | | | ||
|- | |- | ||
| Line 62: | Line 62: | ||
|- | |- | ||
|3.4.1.a | |3.4.1.a | ||
| − | | | + | |Develop a theory of real arithmetic |
| | | | ||
|- | |- | ||
| − | |3.4.1. | + | |3.4.1.b |
| − | | | + | |Develop other domain-specific theories for case studies |
| | | | ||
|- | |- | ||
| − | |3.4. | + | |3.4.2.a |
| − | | | + | |Develop enabledness-preservation proof obligations |
| | | | ||
|- | |- | ||
| − | |3.4. | + | |3.4.2.b |
| − | | | + | |Link modelling of discrete behaviour with continuous behaviour |
| | | | ||
|- | |- | ||
| − | |3.4. | + | |3.4.2.c |
| − | | | + | |Develop Event-B extensions to specify temporal properties |
| | | | ||
|- | |- | ||
| − | |3.4. | + | |3.4.2.d |
| − | | | + | |Extend UML-B plug-in to support additional UML and SysML features |
| | | | ||
|- | |- | ||
| − | |3.4. | + | |3.4.3.a |
| − | | | + | |Develop mechanism for generic modelling and refinement patterns |
| | | | ||
|- | |- | ||
| − | |3.4. | + | |3.4.3.b |
| − | | | + | |Develop patterns for modelling timing properties |
| | | | ||
|- | |- | ||
| − | |3.4. | + | |3.4.3.c |
| − | | | + | |Develop other modelling and refinement patterns for case studies |
| | | | ||
|} | |} | ||
Revision as of 15:07, 5 September 2013
Task Plan
Task Status
| Task Id | Title | Status |
|---|---|---|
| 3.2.1 | Answer questions from ADVANCE partners | |
| 3.2.2 | Process feature requests and platform issues | |
| 3.2.3 | Maintain and evolve model editors | |
| 3.2.4 | Ensure Event-B handbook consistency | |
| 3.3.1.a | Enrich SMT support for Event-B mathematical language | |
| 3.3.1.b | Assess SMT solvers effectiveness | |
| 3.3.2.a | Develop specialised prover tactics for case studies | |
| 3.3.2.b | Add FAQ in handbook with tips on prover tactics | |
| 3.3.3.a | Develop methods for combining SAT/SMT with ProB | |
| 3.3.3.b | Develop methods for state space compression and state hashing | |
| 3.3.4.a | Develop links between theory plug-in and SMT | |
| 3.3.4.b | develop links between theory plug-in and ProB | |
| 3.3.4.c | Develop links between theory plug-in and user tactics | |
| 3.4.1.a | Develop a theory of real arithmetic | |
| 3.4.1.b | Develop other domain-specific theories for case studies | |
| 3.4.2.a | Develop enabledness-preservation proof obligations | |
| 3.4.2.b | Link modelling of discrete behaviour with continuous behaviour | |
| 3.4.2.c | Develop Event-B extensions to specify temporal properties | |
| 3.4.2.d | Extend UML-B plug-in to support additional UML and SysML features | |
| 3.4.3.a | Develop mechanism for generic modelling and refinement patterns | |
| 3.4.3.b | Develop patterns for modelling timing properties | |
| 3.4.3.c | Develop other modelling and refinement patterns for case studies |
