Difference between pages "Tool Development Roadmap" and "UML-B release notes for 0.5.8"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
 
imported>Colin
(New page: ==New Features== '''Statemachine Refinement''' '''Manual invocation of U2B translator''' '''Migration tool''' '''Improve Diagram management''' '''Improve Event-B file management''' '...)
 
Line 1: Line 1:
== Task Plan ==
+
==New Features==
[[File:ADVANCE_Tool_Roadmap.png]]
 
  
== Task Status ==
+
'''Statemachine Refinement'''
  
{| border="1"
+
'''Manual invocation of U2B translator'''
!Task
+
 
!Task Id
+
'''Migration tool'''
!Deliverable
+
 
!Title
+
'''Improve Diagram management'''
!Status
+
 
|-
+
'''Improve Event-B file management'''
|rowspan="4"|Platform maintenance
+
 
|3.2.1
+
'''Improve properties view'''
|D3.2, D3.3, D3.4
+
 
|Answer questions from ADVANCE partners
+
==Bug Fixes==
|
+
 
|-
+
Improvements to synchronise diagram editing so that unsaved changes are not lost.
|3.2.2
+
 
|D3.2, D3.3, D3.4
+
Default names of new elements were not unique
|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
 
|
 
|-
 
|rowspan="9"|Automated Proof and Model-checking
 
|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
 
|
 
|-
 
|rowspan="9"|Language extension
 
|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
 
|
 
|-
 
|rowspan="5"|Composition and decomposition
 
|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
 
|
 
|-
 
|rowspan="6"|Multi-simulation framework development
 
|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
 
|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
 
|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
 
|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
 
|
 
|}
 

Revision as of 14:48, 4 March 2009

New Features

Statemachine Refinement

Manual invocation of U2B translator

Migration tool

Improve Diagram management

Improve Event-B file management

Improve properties view

Bug Fixes

Improvements to synchronise diagram editing so that unsaved changes are not lost.

Default names of new elements were not unique