imported>Nicolas |
imported>Colin |
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
| |
− | |
| |
− | |}
| |