Difference between pages "Tool Development Roadmap" and "User:Nicolas/Collections/ADVANCE D3.4 Model Checking"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
 
imported>Ladenberger
 
Line 1: Line 1:
−
== Task Plan ==
+
== Overview ==
−
[[File:ADVANCE_Tool_Roadmap.png]]
+
{{TODO}}
  
−
== Task Status ==
+
== Motivations / Decisions ==
 +
'''B to TLA+'''
  
−
{| border="1"
+
'''LTL Fairness'''
−
!Task
+
 
−
!Task Id
+
'''Theory Support'''
−
!Deliverable
+
 
−
!Title
+
'''Physical Units'''
−
!Status
+
 
−
|-
+
The physical units analysis has been further stabilised, several reported bugs have been fixed.
−
|rowspan="4"|Platform maintenance
+
Support for physical units has been extended to theories along with the general theory-related improvements of ProB mentioned in the previous paragraph.
−
|3.2.1
+
The plug-in was ported to Rodin 3, all bugfixes and changes could be back ported to Rodin 2 successfully.
−
|D3.2, D3.3, D3.4
+
 
−
|Answer questions from ADVANCE partners
+
Further extension to the unit analysis include:
−
|
+
* Support for the analysis of units throughout refinement relations.
−
|-
+
* Support for abstract units like "length" that can later be concretised to standard SI units.
−
|3.2.2
+
 
−
|D3.2, D3.3, D3.4
+
{{TODO}}
−
|Process feature requests and platform issues
+
 
−
|
+
== Available Documentation ==
−
|-
+
 
−
|3.2.3
+
'''ProB'''<br>
−
|D3.2, D3.3, D3.4
+
The ProB Website<ref>http://www.stups.uni-duesseldorf.de/ProB</ref> is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.
−
|Maintain and evolve model editors
+
 
−
|
+
In addition we run a bug tracking system<ref>http://jira.cobra.cs.uni-duesseldorf.de/</ref> to document known bugs, workarounds and feature requests.
−
|-
+
 
−
|3.2.4
+
{{TODO}}
−
|D3.2, D3.3, D3.4
+
 
−
|Ensure Event-B handbook consistency
+
== Conclusion ==
−
|
+
{{TODO}}
−
|-
+
 
−
|rowspan="9"|Automated Proof and Model-checking
+
== References ==
−
|3.3.1.a
+
<references/>
−
|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 13:03, 15 October 2014

Overview

TODO

Motivations / Decisions

B to TLA+

LTL Fairness

Theory Support

Physical Units

The physical units analysis has been further stabilised, several reported bugs have been fixed. Support for physical units has been extended to theories along with the general theory-related improvements of ProB mentioned in the previous paragraph. The plug-in was ported to Rodin 3, all bugfixes and changes could be back ported to Rodin 2 successfully.

Further extension to the unit analysis include:

  • Support for the analysis of units throughout refinement relations.
  • Support for abstract units like "length" that can later be concretised to standard SI units.

TODO

Available Documentation

ProB
The ProB Website[1] is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.

In addition we run a bug tracking system[2] to document known bugs, workarounds and feature requests.

TODO

Conclusion

TODO

References

  1. ↑ http://www.stups.uni-duesseldorf.de/ProB
  2. ↑ http://jira.cobra.cs.uni-duesseldorf.de/
Retrieved from ‘https://wiki.event-b.org/index.php?title=Tool_Development_Roadmap&oldid=10924’