User:Nicolas/Collections/ADVANCE D3.4 Language extension - Revision history

imported>Asiehsalehi: /* Conclusion */

2014-11-19T15:34:32Z

Conclusion

← Older revision		Revision as of 15:34, 19 November 2014
Line 42:		Line 42:

	== Conclusion ==		== Conclusion ==
	Theory plugin plays an important role in enhancing the useability of the Rodin in terms of extending the Event-B modelling language and provers. The latest release (2.0.2) can be considered as a stable release for Rodin v2.8, and is used in WP1 and WP2 as below:		The Theory plugin plays an important role in enhancing the useability of the Rodin in terms of extending the Event-B modelling language and provers. The latest release (2.0.2) can be considered as a stable release for Rodin v2.8, and is used in WP1 and WP2 as below:

	* In WP1 it was used to develop theories of graphs and chains to represent rail network topology, train positions and train movements.		* In WP1 it was used to develop theories of graphs and chains to represent rail network topology, train positions and train movements.
	* In WP2 is was used for modelling arithmetic operations on data collections (generalised product and sum) for the voltage controller.		* In WP2 is was used for modelling arithmetic operations on data collections (generalised product and sum) for the voltage controller.

	Also an external industrial user, Thales, has used the Theory plug-in for representing variability in modelling of railway interlocking systems. In particular Thales developed a generic model of an interlocking system and represented operational rules specific to particular rail operators as mathematical operators in theories. Different rules are represented as different theories for the same generic model.		Also an external industrial user, Thales, has used the Theory plug-in for representing variability in modelling of railway interlocking systems. In particular Thales developed a generic model of an interlocking system and represented operational rules specific to particular rail operators as mathematical operators in theories. Different rules are represented as different theories for the same generic model. The Thales presentation at ADVANCE Industry Day is available [http://www.advance-ict.eu/industry_days here].

	== References ==		== References ==

imported>Asiehsalehi: /* Conclusion */

2014-11-07T13:00:52Z

Conclusion

← Older revision		Revision as of 13:00, 7 November 2014
Line 47:		Line 47:
	* In WP2 is was used for modelling arithmetic operations on data collections (generalised product and sum) for the voltage controller.		* In WP2 is was used for modelling arithmetic operations on data collections (generalised product and sum) for the voltage controller.

	Also an external industrial user, Thales, has used the ~~theory~~ plug-in for representing variability in modelling of railway interlocking systems. In particular Thales developed a generic model of an interlocking system and represented operational rules specific to particular rail operators as mathematical operators in theories. Different rules are represented as different theories for the same generic model.		Also an external industrial user, Thales, has used the Theory plug-in for representing variability in modelling of railway interlocking systems. In particular Thales developed a generic model of an interlocking system and represented operational rules specific to particular rail operators as mathematical operators in theories. Different rules are represented as different theories for the same generic model.

	== References ==		== References ==

imported>Asiehsalehi: /* Conclusion */

2014-11-07T13:00:03Z

Conclusion

← Older revision		Revision as of 13:00, 7 November 2014
Line 45:		Line 45:

	* In WP1 it was used to develop theories of graphs and chains to represent rail network topology, train positions and train movements.		* In WP1 it was used to develop theories of graphs and chains to represent rail network topology, train positions and train movements.
	* In WP2 is was used for modelling arithmetic operations on data collections (generalised product and sum) for the voltage controller		* In WP2 is was used for modelling arithmetic operations on data collections (generalised product and sum) for the voltage controller.

	Also an external industrial user, Thales, has used the theory plug-in for representing variability in modelling of railway interlocking systems. In particular Thales developed a generic model of an interlocking system and represented operational rules specific to particular rail operators as mathematical operators in theories. Different rules are represented as different theories for the same generic model.		Also an external industrial user, Thales, has used the theory plug-in for representing variability in modelling of railway interlocking systems. In particular Thales developed a generic model of an interlocking system and represented operational rules specific to particular rail operators as mathematical operators in theories. Different rules are represented as different theories for the same generic model.

imported>Asiehsalehi: /* Conclusion */

2014-11-07T12:59:44Z

Conclusion

← Older revision		Revision as of 12:59, 7 November 2014
Line 42:		Line 42:

	== Conclusion ==		== Conclusion ==
	Theory plugin plays an important role in enhancing the useability of the Rodin in terms of extending the Event-B modelling language and provers. The latest release (2.0.2) I can be considered as a stable release for Rodin v2.8, and is used in WP1 and WP2 as below:		Theory plugin plays an important role in enhancing the useability of the Rodin in terms of extending the Event-B modelling language and provers. The latest release (2.0.2) can be considered as a stable release for Rodin v2.8, and is used in WP1 and WP2 as below:

	* In WP1 it was used to develop theories of graphs and chains to represent rail network topology, train positions and train movements.		* In WP1 it was used to develop theories of graphs and chains to represent rail network topology, train positions and train movements.

imported>Asiehsalehi: /* Conclusion */

2014-11-07T12:58:57Z

Conclusion

← Older revision		Revision as of 12:58, 7 November 2014
Line 42:		Line 42:

	== Conclusion ==		== Conclusion ==
	~~{{TODO}}~~		Theory plugin plays an important role in enhancing the useability of the Rodin in terms of extending the Event-B modelling language and provers. The latest release (2.0.2) I can be considered as a stable release for Rodin v2.8, and is used in WP1 and WP2 as below:

			* In WP1 it was used to develop theories of graphs and chains to represent rail network topology, train positions and train movements.
			* In WP2 is was used for modelling arithmetic operations on data collections (generalised product and sum) for the voltage controller

			Also an external industrial user, Thales, has used the theory plug-in for representing variability in modelling of railway interlocking systems. In particular Thales developed a generic model of an interlocking system and represented operational rules specific to particular rail operators as mathematical operators in theories. Different rules are represented as different theories for the same generic model.

	== References ==		== References ==

imported>Asiehsalehi: /* Motivations / Decisions */

2014-11-07T12:46:40Z

Motivations / Decisions

← Older revision		Revision as of 12:46, 7 November 2014
Line 10:		Line 10:
	In the past 5 months:		In the past 5 months:

	* Two versions of the Theory plug-in is released. <ref>http://wiki.event-b.org/index.php/Theory_Release_History</ref> The releases include several bug fixes~~. The latest release (2.0.2) is considered as a stable release for Rodin v2.8~~.		* Two versions of the Theory plug-in is released. <ref>http://wiki.event-b.org/index.php/Theory_Release_History</ref> The releases include several bug fixes.

	* A set of standard theories and some models using these theories are developed . The standard library of the theories is available to download [https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.1.zip/download here].		* A set of standard theories and some models using these theories are developed . The standard library of the theories is available to download [https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.1.zip/download here].

imported>WikiSysop: /* Overview */

2014-11-07T11:12:44Z

Overview

← Older revision		Revision as of 11:12, 7 November 2014
Line 1:		Line 1:
	== Overview ==		== Overview ==
	Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this ~~new~~ feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).		Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).

	The Theory plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plug-in provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.		The Theory plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plug-in provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.

imported>Asiehsalehi: /* Motivations / Decisions */

2014-10-20T14:32:15Z

Motivations / Decisions

← Older revision		Revision as of 14:32, 20 October 2014
Line 22:		Line 22:
	* Queue project: using Seq theory		* Queue project: using Seq theory
	* SimpleNetwork project: using closure theory		* SimpleNetwork project: using closure theory

			During last 4 months, the migration of Theory plug-in for Rodin v3.1 is being perfumed. This work involves major changes in managing the compatibilities in the Theory plug-in using the APIs from Rodin core v3.1.

	== Available Documentation ==		== Available Documentation ==

imported>Asiehsalehi: /* Motivations / Decisions */

2014-10-20T14:29:08Z

Motivations / Decisions

← Older revision		Revision as of 14:29, 20 October 2014
Line 12:		Line 12:
	* Two versions of the Theory plug-in is released. <ref>http://wiki.event-b.org/index.php/Theory_Release_History</ref> The releases include several bug fixes. The latest release (2.0.2) is considered as a stable release for Rodin v2.8.		* Two versions of the Theory plug-in is released. <ref>http://wiki.event-b.org/index.php/Theory_Release_History</ref> The releases include several bug fixes. The latest release (2.0.2) is considered as a stable release for Rodin v2.8.

	* A set of standard theories and some models using these theories are developed . The standard library of the theories is available to download [https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.1.zip/download here]. This library includes:		* A set of standard theories and some models using these theories are developed . The standard library of the theories is available to download [https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.1.zip/download here].
	** BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.		This library includes:
	** RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.		* BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.
	** RealTheory project: including theory of Real.		* RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.
			* RealTheory project: including theory of Real.

	Also it includes three Event-B models that use these theories:		Also it includes three Event-B models that use these theories:
	** Data project: using SUMandPRODUCT theory		* Data project: using SUMandPRODUCT theory
	** Queue project: using Seq theory		* Queue project: using Seq theory
	** SimpleNetwork project: using closure theory		* SimpleNetwork project: using closure theory

	== Available Documentation ==		== Available Documentation ==

imported>Asiehsalehi: /* References */

2014-10-20T14:26:32Z

References

← Older revision		Revision as of 14:26, 20 October 2014
Line 43:		Line 43:
	== References ==		== References ==
	<references/>		<references/>

			[[Category:ADVANCE D3.4 Deliverable]]