Difference between pages "Theory Plug-in" and "Tool Development Roadmap"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Asiehsalehi
 
imported>Nicolas
 
Line 1: Line 1:
−
Return to [[Rodin Plug-ins]]
+
== Task Plan ==
 +
[[File:ADVANCE_Tool_Roadmap.png]]
  
−
See also [[Theory Release History]]
+
== Task Status ==
  
−
The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities.
+
{| border="1"
−
 
+
!Task
−
===Motivation===
+
!Task Id
−
Up to Rodin v2.0, the mathematical language used in Event-B has been fixed. As such, it was not possible to define reusable polymorphic operators. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the Event-B language lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator (which was present in classical B mathematical language) and the bag operator.
+
!Deliverable
−
 
+
!Title
−
In Rodin v2.0, support for customised syntactic symbols was introduced. The Theory plug-in, as a result, evolved from being just a component to define rewrite rules to a versatile platform to define and validate proof and language extensions.
+
!Status
−
 
+
|-
−
===Overview===
+
|rowspan="4"|Platform maintenance
−
The Theory plug-in is a Rodin extension that provides the facility to define '''''mathematical extensions''''' as well as '''''prover extensions'''''.
+
|3.2.1
−
Mathematical extensions are new operator definitions and new datatype definitions and axiomatic definitions. Operator definitions can be expression operators (e.g., ''card'') and predicate operators (e.g., ''finite''). Datatypes extensions can be used to define enumerated datatypes (e.g., ''DIRECTION'') as well as inductive datatypes (e.g., ''Tree'').
+
|D3.2, D3.3, D3.4
−
 
+
|Answer questions from ADVANCE partners
−
The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, axiomatic definitions, inference and rewrite rules as well as polymorphic theorems. The [http://wiki.event-b.org/images/Theory_Plugin.pdf user manual] provides a guide to developing and using theories.
+
|
−
 
+
|-
−
=== Installation & Update ===
+
|3.2.2
−
 
+
|D3.2, D3.3, D3.4
−
The installation or update for the Theory plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates) under the category "Modelling Extensions". Like always, after the installation, restarting Rodin is recommended.
+
|Process feature requests and platform issues
−
 
+
|
−
===User Manual===
+
|-
−
The user manual is available here: [http://wiki.event-b.org/images/Theory_Plugin.pdf Theory User Manual].
+
|3.2.3
−
 
+
|D3.2, D3.3, D3.4
−
===Worked Examples===
+
|Maintain and evolve model editors
−
In this section, you find examples of theories and models using theories. Below is the presentation of a simple theory:
+
|
−
 
+
|-
−
[[Image:SeqThoery.pdf|center|thumb|800px|'''Theory of Sequence''']]
+
|3.2.4
−
 
+
|D3.2, D3.3, D3.4
−
You can find an example of a theory and a model using that [[Media:ProdSum.pdf|''here'']].
+
|Ensure Event-B handbook consistency
−
 
+
|
−
===Capabilities===
+
|-
−
The Theory plug-in has the following capabilities:
+
|rowspan="9"|Automated Proof and Model-checking
−
 
+
|3.3.1.a
−
* Theory Definition:
+
|D3.2, D3.3
−
** Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
+
|Enrich SMT support for Event-B mathematical language
−
** Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is ''card''. A predicate operator is one that "returns" a predicate, an example existing predicate operator is ''finite''.
+
|
−
** Definition of axiomatic definitions: axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms.
+
|-
−
** Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
+
|3.3.1.b
−
** Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
+
|D3.2, D3.3
−
** Definition of polymorphic theorems: theorems can be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
+
|Assess SMT solvers effectiveness
−
** Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
+
|
−
*Theory Deployment: this step signifies that a theory is ready for use. Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.
+
|-
−
Once a theory has been deployed to its designated project, all its extensions (mathematical and prover extensions) can be used in models.
+
|3.3.2.a
−
 
+
|D3.2
−
===Insider Look===
+
|Develop specialised prover tactics for case studies
−
The Theory plug-in partially satisfies the requirements outlined in the following document:
+
|
−
* [http://deploy-eprints.ecs.soton.ac.uk/80/ Abrial, Jean-Raymond and Butler, Michael and Schmalz, Matthias and Hallerstede, Stefan and Voisin, Laurent. Mathematical Extensions Proposal]
+
|-
−
 
+
|3.3.2.b
−
A more accurate description of the implemented functionalities of the plug-in can be found in the following document:
+
|D3.2
−
* [http://deploy-eprints.ecs.soton.ac.uk/251/ Michael Butler, Issam Maamria. Mathematical Extensions Summary]
+
|Add FAQ in handbook with tips on prover tactics
−
 
+
|
−
The following two papers describe rewriting and well-definedness issues that has to be accounted for:
+
|-
−
 
+
|3.3.3.a
−
* [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.]
+
|D3.2, D3.3
−
* [http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.]
+
|Develop methods for combining SAT/SMT with ProB
−
 
+
|
−
 
+
|-
−
[[Category:Plugin]]
+
|3.3.3.b
−
[[Category:User documentation]]
+
|D3.3
−
[[Category:Proof]]
+
|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:53, 9 September 2013

Task Plan

ADVANCE Tool Roadmap.png

Task Status

Task Task Id Deliverable Title Status
Platform maintenance 3.2.1 D3.2, D3.3, D3.4 Answer questions from ADVANCE partners
3.2.2 D3.2, D3.3, D3.4 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
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
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
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

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
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
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
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
Retrieved from ‘https://wiki.event-b.org/index.php?title=Theory_Plug-in&oldid=10410’