D32 Code generation - Revision history

imported>Tommy at 15:08, 27 January 2011

2011-01-27T15:08:27Z

← Older revision		Revision as of 15:08, 27 January 2011
Line 1:		Line 1:
	= General Overview =		= General Overview =

	The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">[[Event_Model_Decomposition]]</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">[[EMF_framework_for_Event-B]]</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">[[Flows]]</ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.		The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">http://wiki.event-b.org/index.php/EMF_framework_for_Event-B</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">http://wiki.event-b.org/index.php/Flows</ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.

	= Motivations =		= Motivations =

	The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> [[D23_Code_Generation]]</ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.		The decision was taken in 2009 to include code generation as a project goal <ref name = "d23">http://wiki.event-b.org/index.php/D23_Code_Generation</ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.

	= Choices / Decisions =		= Choices / Decisions =
Line 19:		Line 19:
	The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://deploy-eprints.ecs.soton.ac.uk/260/2/CGSlidesAndy%2520Edmunds%2520-%2520Code%2520Generation%2520Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.		The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://deploy-eprints.ecs.soton.ac.uk/260/2/CGSlidesAndy%2520Edmunds%2520-%2520Code%2520Generation%2520Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.

	Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing ~~Events]]~~) to facilitate code generation.		Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see Events<ref name="taskext">http://wiki.event-b.org/index.php/D32_Code_generation#Implementing</ref>) to facilitate code generation.

	A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). In our approach we make use of the Event-B EMF extension mechanism which allows addition of new constructs to a model. The tasking extension consists of the constructs in the following table.		A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). In our approach we make use of the Event-B EMF extension mechanism which allows addition of new constructs to a model. The tasking extension consists of the constructs in the following table.
Line 134:		Line 134:
	== For Users ==		== For Users ==

	There is an overview at [[Tasking Event-B Overview for D32 ]]		There is an overview at Tasking Event-B Overview for D32<ref name="tasking">http://wiki.event-b.org/index.php/Tasking_Event-B_Overview_for_D32</ref>

	There is a wiki page at [[Code_Generation_Activity]]		There is a wiki page at Code Generation Activity<ref name="CodegenAct">http://wiki.event-b.org/index.php/Code_Generation_Activity</ref>

	There is a tutorial at [[Code_Generation_Tutorial]]		There is a tutorial at Code Generation Tutorial<ref name="Code_Generation_Tutorial">http://wiki.event-b.org/index.php/Code_Generation_Tutorial</ref>

	= Planning =		= Planning =

imported>Tommy at 11:17, 27 January 2011

2011-01-27T11:17:50Z

← Older revision		Revision as of 11:17, 27 January 2011
Line 73:		Line 73:
	** Branch - choice between a number of mutually exclusive events.		** Branch - choice between a number of mutually exclusive events.
	** Loop - event repetition while it's guard remains true.		** Loop - event repetition while it's guard remains true.
	** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do no share state. The synchronization construct also provides the means to specify parameter passing, both in and out of the task.		** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do not share state. The synchronization construct also provides the means to specify parameter passing, both in and out of the task.
	** Event wrappers - The event synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for synchronizing). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.		** Event wrappers - The event synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for synchronizing). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.

imported>Andy: /* For Users */

2011-01-26T10:48:54Z

For Users

← Older revision		Revision as of 10:48, 26 January 2011
Line 134:		Line 134:
	== For Users ==		== For Users ==

	There is an overview at [[Tasking Event-B Overview ]]		There is an overview at [[Tasking Event-B Overview for D32 ]]

	There is a wiki page at [[Code_Generation_Activity]]		There is a wiki page at [[Code_Generation_Activity]]

imported>Tommy at 11:12, 21 December 2010

2010-12-21T11:12:00Z

← Older revision		Revision as of 11:12, 21 December 2010
Line 144:		Line 144:
	During 2011 we plan to develop the code generation tools further, taking on board any feedback from interested parties. The tool support should advance to the prototype stage, with improvements in the tool's usability in terms of features and user experience.		During 2011 we plan to develop the code generation tools further, taking on board any feedback from interested parties. The tool support should advance to the prototype stage, with improvements in the tool's usability in terms of features and user experience.

	=== References ===		== References ==

	<references/>		<references/>

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Tommy at 10:20, 20 December 2010

2010-12-20T10:20:50Z

Show changes

imported>Andy: /* For users */

2010-12-13T12:05:45Z

For users

← Older revision		Revision as of 12:05, 13 December 2010
Line 132:		Line 132:
	There are technical notes available <ref name = "techNotes">http://wiki.event-b.org/images/Translation.pdf</ref>, that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.		There are technical notes available <ref name = "techNotes">http://wiki.event-b.org/images/Translation.pdf</ref>, that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.

	=== For ~~users~~ ===		=== For Users ===

	There is an overview at [[Tasking Event-B Overview ]]		There is an overview at [[Tasking Event-B Overview ]]

imported>Andy at 12:04, 13 December 2010

2010-12-13T12:04:51Z

← Older revision		Revision as of 12:04, 13 December 2010
Line 1:		Line 1:
	== General Overview ==		== General Overview ==

	The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">Event_Model_Decomposition</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">EMF_framework_for_Event-B</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">Flows </ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.		The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">[[Event_Model_Decomposition]]</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">[[EMF_framework_for_Event-B]]</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">[[Flows]]</ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.

	== Motivations ==		== Motivations ==

	The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> D23_Code_Generation </ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.		The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> [[D23_Code_Generation]]</ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.

	== Choices / Decisions ==		== Choices / Decisions ==

imported>Andy at 12:03, 13 December 2010

2010-12-13T12:03:12Z

← Older revision		Revision as of 12:03, 13 December 2010
Line 1:		Line 1:
	== General Overview ==		== General Overview ==

	The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">~~http://wiki.event-b.org/index.php/~~Event_Model_Decomposition</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">~~http://wiki.event-b.org/index.php/~~EMF_framework_for_Event-B</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">~~http://wiki.event-b.org/index.php/~~Flows </ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.		The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">Event_Model_Decomposition</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">EMF_framework_for_Event-B</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">Flows </ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.

	== Motivations ==		== Motivations ==

	The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> ~~http://wiki.event-b.org/index.php/~~D23_Code_Generation </ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.		The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> D23_Code_Generation </ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.

	== Choices / Decisions ==		== Choices / Decisions ==
Line 134:		Line 134:
	=== For users ===		=== For users ===

	There is ~~a wiki page~~ at ~~http://wiki.event~~-~~b.org/index.php/Code_Generation_Activity~~		There is an overview at [[Tasking Event-B Overview ]]

	There is a tutorial at ~~http://wiki.event-b.org/index.php/~~Code_Generation_Tutorial		There is a wiki page at [[Code_Generation_Activity]]

			There is a tutorial at [[Code_Generation_Tutorial]]

	== Planning ==		== Planning ==

imported>Andy at 09:47, 7 December 2010

2010-12-07T09:47:23Z

← Older revision		Revision as of 09:47, 7 December 2010
Line 1:		Line 1:
	~~'''THIS DOCUMENT IS NOT YET COMPLETE !!!'''~~

	== General Overview ==		== General Overview ==

imported>Andy at 15:12, 3 December 2010

2010-12-03T15:12:51Z

← Older revision		Revision as of 15:12, 3 December 2010
Line 19:		Line 19:
	=== The Tasking Extension for Event-B ===		=== The Tasking Extension for Event-B ===

	The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://~~bscw~~.cs.~~ncl~~.ac.uk/~~bscw/bscw.cgi~~/~~d108734~~/~~Andy~~%~~20Edmunds~~%20-%~~20Code~~%~~20Generation~~%~~20Slides~~.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.		The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://deploy-eprints.ecs.soton.ac.uk/260/2/CGSlidesAndy%2520Edmunds%2520-%2520Code%2520Generation%2520Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.

	Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code generation.		Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code generation.