Difference between pages "Theory Plug-in" and "User:Nicolas/Collections/ADVANCE D3.4 Model Checking"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
imported>Ladenberger
 
Line 1: Line 1:
Return to [[Rodin Plug-ins]]
+
== Overview ==
 +
{{TODO}}
  
The Theory plug-in is the successor of the Rule-based Prover (which will be referred to as RbP) plug-in. The Theory plug-in
+
== Motivations / Decisions ==
provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. If you are looking for the user manual or the latest news on the Theory plug-in, please refer to [[Theory News and Support|Theory News and Support]].
+
'''B to TLA+'''
This page provides useful information about the plug-in and its design.
 
  
===Motivation===
+
'''LTL Fairness'''
  
===Overview===
+
'''Theory Support'''
  
===Capabilities===
+
'''Physical Units'''
  
===Insider Look===
+
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.
  
:[http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.]
+
Further extension to the unit analysis include:
:[http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.]
+
* Support for the analysis of units throughout refinement relations.
 +
* Support for abstract units like "length" that can later be concretised to standard SI units.
  
===Improvements and Bugs===
+
{{TODO}}
  
See also the late [[Rule-based Prover Plug-in]], the last release of the which was v0.3. The Theory plug-in starts at version v0.5.
+
== Available Documentation ==
 +
 
 +
'''ProB'''<br>
 +
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.
 +
 
 +
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.
 +
 
 +
{{TODO}}
 +
 
 +
== Conclusion ==
 +
{{TODO}}
 +
 
 +
== References ==
 +
<references/>

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