Tool Development Roadmap: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Nicolas
imported>Tommy
mNo edit summary
 
(8 intermediate revisions by one other user not shown)
Line 5: Line 5:


{| border="1"
{| border="1"
!Task
!Task Id
!Task Id
!Deliverable
!Deliverable
Line 10: Line 11:
!Status
!Status
|-
|-
|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
|Answer questions from ADVANCE partners
|Answer questions from ADVANCE partners
|
|Done, covered in D3.3.
|-
|-
|3.2.2
|3.2.2
|D3.2, D3.3, D3.4
|D3.2, D3.3, D3.4
|Process feature requests and platform issues
|Process feature requests and platform issues
|
|Done, covered in D3.3.
|-
|-
|3.2.3
|3.2.3
|D3.2, D3.3, D3.4
|D3.2, D3.3, D3.4
|Maintain and evolve model editors
|Maintain and evolve model editors
|
|Done, covered in D3.3.
|-
|-
|3.2.4
|3.2.4
Line 30: Line 32:
|
|
|-
|-
|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
|Enrich SMT support for Event-B mathematical language
|Enrich SMT support for Event-B mathematical language
|
|Done, covered in D3.3.
|-
|-
|3.3.1.b
|3.3.1.b
|D3.2, D3.3
|D3.2, D3.3
|Assess SMT solvers effectiveness
|Assess SMT solvers effectiveness
|
|Done, covered in D3.3.
|-
|-
|3.3.2.a
|3.3.2.a
|D3.2
|D3.2
|Develop specialised prover tactics for case studies
|Develop specialised prover tactics for case studies
|
|Not done yet, expecting feedback from case studies
|-
|-
|3.3.2.b
|3.3.2.b
|D3.2
|D3.2
|Add FAQ in handbook with tips on prover tactics
|Add FAQ in handbook with tips on prover tactics
|
|Partially done, paragraph exists: [http://handbook.event-b.org/current/html/use_provers_effectively.html], to be enriched
|-
|-
|3.3.3.a
|3.3.3.a
Line 75: Line 78:
|
|
|-
|-
|rowspan="9"|'''Language extension'''<br/>[Southampton / Systerel / Düsseldorf / All Partners]
|3.4.1.a
|3.4.1.a
|D3.3
|D3.3
Line 120: Line 124:
|
|
|-
|-
|rowspan="5"|'''Composition and decomposition'''<br/>[Southampton / Düsseldorf / Systerel]
|3.5.1.a
|3.5.1.a
|D3.2
|D3.2
Line 142: Line 147:
|3.5.2.a
|3.5.2.a
|D3.3
|D3.3
|Add team working support for merging proofs,
|Add team working support for comparing and merging proofs,
model checking, composition and decomposition
model checking, composition and decomposition
|
|-
|rowspan="6"|'''Multi-simulation framework development'''<br/>[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
|
|-
|rowspan="5"|'''Model simulation with ProB'''<br/>[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
|
|-
|rowspan="4"|'''Model-based testing'''<br/>[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
|
|-
|rowspan="4"|'''Code generation'''<br/>[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
|
|
|}
|}

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
Retrieved from ‘https://wiki.event-b.org/index.php?title=Tool_Development_Roadmap&oldid=10416’