Tool Development Roadmap

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