Difference between revisions of "Tool Development Roadmap"

From Event-B
Jump to navigationJump to search
imported>Nicolas
imported>Tommy
m
 
(One intermediate revision by one other user not shown)
Line 11: Line 11:
 
!Status
 
!Status
 
|-
 
|-
|rowspan="4"|'''Platform maintenance'''<br/>[Systerel / Dusseldorf]
+
|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'''<br/>[Systerel / Dusseldorf / Southampton]
+
|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'''<br/>[Southampton / Systerel / Dusseldorf / All Partners]
+
|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

ADVANCE Tool Roadmap.png

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