ADVANCE D3.3 General Platform Maintenance - Revision history

imported>Ladenberger: /* Overview */

2013-10-08T14:05:09Z

Overview

← Older revision		Revision as of 14:05, 8 October 2013
Line 95:		Line 95:
	The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref> The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and formal models.		The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref> The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and formal models.

	~~Significant~~ contributions to the latest version of the ProR/Rodin integration plugin have been made ~~on phenomena~~ support (maintaining a glossary and tracing phenomena) ~~and the integration~~ of the tracing method<ref name="req1ref">http://www.stups.uni-duesseldorf.de/mediawiki/images/e/ec/Pub-HalJasLad2013.pdf</ref> ~~during the second period of the ADVANCE project.~~		The following significant contributions to the latest version of the ProR/Rodin integration plugin have been made during the second period of the ADVANCE project:
			* Phenomena support (maintaining a glossary and tracing phenomena)
			* Integration of the tracing method for producing a high quality system description<ref name="req1ref">http://www.stups.uni-duesseldorf.de/mediawiki/images/e/ec/Pub-HalJasLad2013.pdf</ref>

	Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners.		Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners.

imported>Ladenberger: /* ProR */

2013-10-08T14:03:40Z

ProR

← Older revision		Revision as of 14:03, 8 October 2013
Line 95:		Line 95:
	The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref> The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and formal models.		The ProR/Rodin integration plugin is developed and maintained by Lukas Ladenberger and Michael Jastram at the University of Duesseldorf. ProR is a tool for working with requirements in natural language. It is part of the Eclipse Requirements Modeling Framework (RMF).<ref>http://www.eclipse.org/rmf/</ref> The goal of the ProR/Rodin integration plugin is to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. The ProR/Rodin integration plugin supports the user by maintaining a traceability between natural language requirements and formal models.

	Significant contributions to the latest version of the ProR/Rodin integration plugin have been made on phenomena support (maintaining a glossary and tracing phenomena) and the integration of the tracing method ~~for producing a system description of high quality as presented in~~ <ref name="req1ref">http://www.stups.uni-duesseldorf.de/mediawiki/images/e/ec/Pub-HalJasLad2013.pdf</ref>.		Significant contributions to the latest version of the ProR/Rodin integration plugin have been made on phenomena support (maintaining a glossary and tracing phenomena) and the integration of the tracing method<ref name="req1ref">http://www.stups.uni-duesseldorf.de/mediawiki/images/e/ec/Pub-HalJasLad2013.pdf</ref> during the second period of the ADVANCE project.

	Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners.		Other improvements will include more general improvements, such as usability, and any features required by the projects industrial partners.

imported>Ladenberger: /* Motivations / Decisions */

2013-10-08T13:59:04Z

Motivations / Decisions

← Older revision		Revision as of 13:59, 8 October 2013
Line 107:		Line 107:
	'''Tracing Method Integration'''		'''Tracing Method Integration'''

	While all required data structures exist to support the tracing method, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas ~~design decisions~~ and platform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A ''requriements analyzer'' that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such requriements analyzer by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase.		While all required data structures exist to support the tracing method, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas specification elements and platform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A ''requriements analyzer'' that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such requriements analyzer by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase.

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

imported>Ladenberger: /* Motivations / Decisions */

2013-10-08T13:55:20Z

Motivations / Decisions

← Older revision		Revision as of 13:55, 8 October 2013
Line 107:		Line 107:
	'''Tracing Method Integration'''		'''Tracing Method Integration'''

	While all required data structures exist to support the tracing method, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and ~~plaform~~ properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A ''requriements analyzer'' that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such requriements analyzer by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase.		While all required data structures exist to support the tracing method, the ProR/Rodin integration plugin would benefit from more sophisticated reporting. In particular, the tracing method lists a number of properties of a correct system description. For example, the existence of a trace between an artifact and its used phenomenon, or the fact that domain properties, requirement items and design decisions may only be expressed referring to phenomena that are visible in the environment, whereas design decisions and platform properties may only be expressed referring to phenomena that are visible to the system. While the presence of such properties does not guarantee correctness, their absence indicates a problem. A ''requriements analyzer'' that lists all violations of those properties would be valuable to support the user by maintaining a system description of high quality. We developed a first system description for such requriements analyzer by means of the tracing method. We applied Event-B for modelling and validating the different artefacts of the system description and demonstrated how the formal model can be used as a first prototype in the early development phase.

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

imported>Andy: /* Code generation */

2013-09-26T10:35:04Z

Code generation

@@ Line 88: / Line 88: @@
 The current aims are to complete the remaining improvements to the statemachines plug-in and complete the release of the Class diagrams plug-in.
 It is hoped that these plug-ins will provide a very flexibly diagrammatic modelling notation. The plug-ins will then be evaluated on a case study.
 == ProR ==

imported>Andy: /* Motivations / Decisions */

2013-09-23T14:33:27Z

Motivations / Decisions

← Older revision		Revision as of 14:33, 23 September 2013
Line 98:		Line 98:
	Many of the tool improvements in this area have been achieved in tandem (50-50 split) with a separate, but parallel running, piece of work. The tandem project was a feasibility study with an industrial partner (Thales Transportation - Germany). The study involved the modelling of controller software, and of the hardware environment, of a small fan controller. It is the first significant analysis of Tasking Event-B by anyone in industry; since the code generation feature had not matured to the point where it was of interest in previous projects. The aim of the feasibility study was to evaluate the complete Event-B methodology, from abstract specification to Java implementation. This was done as part of an assessment of the tool-set, to judge if Event-B was suitable for use in a large-scale railway signalling project. Details of this work are included in a paper, yet to be submitted. One result of the study was a list of feature requests, which have been added to the Rodin SourceForge repository at<ref>http://sourceforge.net/p/rodin-b-sharp/code-generation/?source=navbar</ref>.		Many of the tool improvements in this area have been achieved in tandem (50-50 split) with a separate, but parallel running, piece of work. The tandem project was a feasibility study with an industrial partner (Thales Transportation - Germany). The study involved the modelling of controller software, and of the hardware environment, of a small fan controller. It is the first significant analysis of Tasking Event-B by anyone in industry; since the code generation feature had not matured to the point where it was of interest in previous projects. The aim of the feasibility study was to evaluate the complete Event-B methodology, from abstract specification to Java implementation. This was done as part of an assessment of the tool-set, to judge if Event-B was suitable for use in a large-scale railway signalling project. Details of this work are included in a paper, yet to be submitted. One result of the study was a list of feature requests, which have been added to the Rodin SourceForge repository at<ref>http://sourceforge.net/p/rodin-b-sharp/code-generation/?source=navbar</ref>.

	In separate work, the generation of code from Event-B models for use as Functional Mock-up Units (FMUs), has been evaluated. Hand coded versions of would-be generated code has been produced, in order to understand ~~what is required to be done~~. Investigations are under-way to explore the methodology of, and technical issues with, the use of an FMU (code) generator.		In separate work, the generation of code from Event-B models, for use as Functional Mock-up Units (FMUs), has been evaluated. A code generator for creating FMUs is important, since the generated code can be packaged into FMUs, and used to simulate the behaviour of controllers, and the environment, in the ADVANCE multi-simulation framework. Hand coded versions of would-be generated code has been produced, in order to understand the task. Investigations are under-way to explore the methodology of, and technical issues with, the use of an FMU (code) generator.

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

imported>Nicolas: /* Motivations / Decisions */ Took M. Butler remarks into account.

2013-09-20T12:59:23Z

Motivations / Decisions: Took M. Butler remarks into account.

← Older revision		Revision as of 12:59, 20 September 2013
Line 17:		Line 17:
	Besides implementing the features needed and fixing the bugs detected by the case studies, which always have top priority, the maintenance of the core platform in the second period of the project was devoted to fixing soundness bugs in the core platform, cleaning up the API and providing structure to the Rodin database.		Besides implementing the features needed and fixing the bugs detected by the case studies, which always have top priority, the maintenance of the core platform in the second period of the project was devoted to fixing soundness bugs in the core platform, cleaning up the API and providing structure to the Rodin database.

	Starting from a usability issue reported by the WP2 case study, we ~~digged~~ into the roots of the reported problem. This led us to find out that the core platform, although working well in general, was too permissive as concerns mathematical extensions. It was possible to declare meaningless empty data types, to freely mix incompatible mathematical extensions and several other oddities. In all these cases, the invariants normally guaranteed by the core platform and on which the soundness of the proofs rely were violated. It was therefore needed to strengthen the way mathematical extensions could be added to the mathematical language to ensure that proofs are always sound.		Starting from a usability issue reported by the WP2 case study, we dug into the roots of the reported problem. This led us to find out that the core platform, although working well in general, was too permissive as concerns mathematical extensions. It was possible to declare meaningless empty data types, to freely mix incompatible mathematical extensions and several other oddities. In all these cases, the invariants normally guaranteed by the core platform and on which the soundness of the proofs rely were violated. Although the Rodin editors did not allow the users to input such invalid entries, these API weaknesses were a major concern as regards overall platform reliability. It was therefore needed to strengthen the way mathematical extensions could be added to the mathematical language to ensure that proofs are always sound.

	The latest major version of the Rodin platform was Rodin 2.0, released in October 2010. Since that release, a lot of new features have been developed, but always keeping the API backward compatible, to comply with the Eclipse standard of release numbering. Consequently, old versions of features, marked as deprecated, had to be kept along with new ones. The middle of the ADVANCE project was considered the best time for performing a clean up of old API parts by releasing a new major version.		The latest major version of the Rodin platform was Rodin 2.0, released in October 2010. Since that release, a lot of new features have been developed, but always keeping the API backward compatible, to comply with the Eclipse standard of release numbering. Consequently, old versions of features, marked as deprecated, had to be kept along with new ones. The middle of the ADVANCE project was considered the best time for performing a clean up of old API parts by releasing a new major version.

imported>Andy: /* Planning */

2013-09-11T09:45:52Z

Planning

← Older revision		Revision as of 09:45, 11 September 2013
Line 104:		Line 104:

	=== Planning ===		=== Planning ===
	Efforts will continue ~~with~~ extending the ~~existing~~ code generation approach, developing new techniques~~, and building a stable platform~~. The automatic generation of code for FMUs, and the methodology required to achieve this will continue to be investigated.		Efforts to build a stable platform from the existing infrastructure will continue; as will work on extending the code generation approach, and developing new techniques. The automatic generation of code for FMUs, and the methodology required to achieve this, will continue to be investigated.

	== ProR ==		== ProR ==

imported>Andy: /* Planning */

2013-09-11T09:37:17Z

Planning

← Older revision		Revision as of 09:37, 11 September 2013
Line 104:		Line 104:

	=== Planning ===		=== Planning ===
	Efforts will continue with extending the existing code generation approach, developing new techniques, and building a stable platform. The automatic generation of code for FMUs, ~~from Event-B~~ will be investigated.		Efforts will continue with extending the existing code generation approach, developing new techniques, and building a stable platform. The automatic generation of code for FMUs, and the methodology required to achieve this will continue to be investigated.

	== ProR ==		== ProR ==

imported>Andy: /* Motivations / Decisions */

2013-09-11T09:35:09Z

Motivations / Decisions

← Older revision		Revision as of 09:35, 11 September 2013
Line 98:		Line 98:
	Many of the tool improvements in this area have been achieved in tandem (50-50 split) with a separate, but parallel running, piece of work. The tandem project was a feasibility study with an industrial partner (Thales Transportation - Germany). The study involved the modelling of controller software, and of the hardware environment, of a small fan controller. It is the first significant analysis of Tasking Event-B by anyone in industry; since the code generation feature had not matured to the point where it was of interest in previous projects. The aim of the feasibility study was to evaluate the complete Event-B methodology, from abstract specification to Java implementation. This was done as part of an assessment of the tool-set, to judge if Event-B was suitable for use in a large-scale railway signalling project. Details of this work are included in a paper, yet to be submitted. One result of the study was a list of feature requests, which have been added to the Rodin SourceForge repository at<ref>http://sourceforge.net/p/rodin-b-sharp/code-generation/?source=navbar</ref>.		Many of the tool improvements in this area have been achieved in tandem (50-50 split) with a separate, but parallel running, piece of work. The tandem project was a feasibility study with an industrial partner (Thales Transportation - Germany). The study involved the modelling of controller software, and of the hardware environment, of a small fan controller. It is the first significant analysis of Tasking Event-B by anyone in industry; since the code generation feature had not matured to the point where it was of interest in previous projects. The aim of the feasibility study was to evaluate the complete Event-B methodology, from abstract specification to Java implementation. This was done as part of an assessment of the tool-set, to judge if Event-B was suitable for use in a large-scale railway signalling project. Details of this work are included in a paper, yet to be submitted. One result of the study was a list of feature requests, which have been added to the Rodin SourceForge repository at<ref>http://sourceforge.net/p/rodin-b-sharp/code-generation/?source=navbar</ref>.

	In separate work, the generation of code from Event-B models for use as Functional Mock-up Units (FMUs), has been evaluated. Hand coded versions of would-be generated code has been produced, in order to understand what is required to be done.		In separate work, the generation of code from Event-B models for use as Functional Mock-up Units (FMUs), has been evaluated. Hand coded versions of would-be generated code has been produced, in order to understand what is required to be done. Investigations are under-way to explore the methodology of, and technical issues with, the use of an FMU (code) generator.

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