D32 Scalability - Revision history

imported>Tommy at 15:28, 27 January 2011

2011-01-27T15:28:28Z

← Older revision		Revision as of 15:28, 27 January 2011
Line 83:		Line 83:

	== Group Refinement ==		== Group Refinement ==
	* There is a wiki page - ~~[[Group refinement plugin]] -~~ briefly introducing the approach and the tool		* There is a wiki page<ref name="grp">http://wiki.event-b.org/index.php/Group_refinement_plugin</ref> briefly introducing the approach and the tool
	* Slides		* Slides

	== Modes ==		== Modes ==
	* There is a [http://wiki.event-b.org/index.php/Mode/FT_Views ~~wiki page]~~ with details of the plug-in functionality, installation guide, and a simple example.		* There is a wiki page<ref>http://wiki.event-b.org/index.php/Mode/FT_Views</ref> with details of the plug-in functionality, installation guide, and a simple example.
	* Papers on modal specifications <ref>[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.148.6369&rep=rep1&type=pdf A.Iliasov, A.Romanovsky, F.L.Dotti. Structuring Specifications with Modes. Fourth Latin-American Symposium on Dependable Computing - LADC 09, September 1-4, 2009]</ref> and <ref>[http://deploy-eprints.ecs.soton.ac.uk/153/1/paper105%2DICFEM09.pdf F.L.Dotti, A.Iliasov, L.Riberiro, A.Romanovsky. Modal Systems: Specification, Reﬁnement and Realisation. In: International Conference on Formal Engineering Methods - ICFEM 09 , December 9 -12, 2009, Rio de Janeiro, Brazil]</ref>, and fault tolerance <ref>[http://www.cs.ncl.ac.uk/publications/trs/papers/1188.pdf I.Lopatkin, A.Iliasov, A.Romanovsky. On Fault Tolerance Reuse during Refinement. In: 2nd International Workshop on Software Engineering for Resilient Systems - SERENE 2010, April 13-16, 2010, London]</ref>.		* Papers on modal specifications <ref>[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.148.6369&rep=rep1&type=pdf A.Iliasov, A.Romanovsky, F.L.Dotti. Structuring Specifications with Modes. Fourth Latin-American Symposium on Dependable Computing - LADC 09, September 1-4, 2009]</ref> and <ref>[http://deploy-eprints.ecs.soton.ac.uk/153/1/paper105%2DICFEM09.pdf F.L.Dotti, A.Iliasov, L.Riberiro, A.Romanovsky. Modal Systems: Specification, Reﬁnement and Realisation. In: International Conference on Formal Engineering Methods - ICFEM 09 , December 9 -12, 2009, Rio de Janeiro, Brazil]</ref>, and fault tolerance <ref>[http://www.cs.ncl.ac.uk/publications/trs/papers/1188.pdf I.Lopatkin, A.Iliasov, A.Romanovsky. On Fault Tolerance Reuse during Refinement. In: 2nd International Workshop on Software Engineering for Resilient Systems - SERENE 2010, April 13-16, 2010, London]</ref>.
	* Also, we are working on a medium-scale case study		* Also, we are working on a medium-scale case study

imported>Tommy: /* References */

2010-12-21T11:25:05Z

References

← Older revision		Revision as of 11:25, 21 December 2010
Line 116:		Line 116:
	In DEPLOY's fourth year, we plan to implement the missing proof obligations. More importantly, we will investigate the interaction between refinement and almost certain termination. This allows us to prove convergence properties early in the development and guarantee that refinement will maintain these convergent properties.		In DEPLOY's fourth year, we plan to implement the missing proof obligations. More importantly, we will investigate the interaction between refinement and almost certain termination. This allows us to prove convergence properties early in the development and guarantee that refinement will maintain these convergent properties.

	=== References ===		== References ==
	<references/>		<references/>

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

imported>Tommy at 12:45, 20 December 2010

2010-12-20T12:45:16Z

← Older revision		Revision as of 12:45, 20 December 2010
Line 120:		Line 120:

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]
	~~[[Category:Books]]~~

imported>Tommy: /* Choices/Decisions */

2010-12-20T10:24:09Z

Choices/Decisions

← Older revision		Revision as of 10:24, 20 December 2010
Line 46:		Line 46:

	== Flow plug-in ==		== Flow plug-in ==
	The single most important feature of the new version of the Flows plug-in is the introduction of a new form of diagram structuring to prevent the appearance of large proof obligations. The typical source of such proof obligations is demonstrating that an event enables one or more events from a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be a simple atomic event.		The single most important feature of the new version of the Flows plug-in is the introduction of a new form of diagram structuring to prevent the appearance of large proof obligations. The typical source of such proof obligations is demonstrating that an event enables one or more events from a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be a simple atomic event.


	== Group Refinement ==		== Group Refinement ==

imported>Tommy at 10:23, 20 December 2010

2010-12-20T10:23:47Z

Show changes

imported>Ilya.lopatkin: /* Modes */

2010-12-03T14:12:13Z

Modes

← Older revision		Revision as of 14:12, 3 December 2010
Line 108:		Line 108:

	==== Modes ====		==== Modes ====
	~~(Ilya)~~		Current status is version 1.0.0 for Rodin 2.0
			In a long term we plan:
			* A few usability improvements
			* Integration with ProR requirements tracing framework
			* Event-B model generation and editing driven by FT patterns

	==== Qualitative Reasoning ====		==== Qualitative Reasoning ====

imported>Ilya.lopatkin: /* Available Documentation */

2010-12-03T13:38:54Z

Available Documentation

← Older revision		Revision as of 13:38, 3 December 2010
Line 86:		Line 86:
	* There is a wiki page - [[Group refinement plugin]] - briefly introducing the approach and the tool		* There is a wiki page - [[Group refinement plugin]] - briefly introducing the approach and the tool
	* Slides		* Slides

			==== Modes ====
			* There is a [http://wiki.event-b.org/index.php/Mode/FT_Views wiki page] with details of the plug-in functionality, installation guide, and a simple example.
			* Papers on modal specifications <ref>[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.148.6369&rep=rep1&type=pdf A.Iliasov, A.Romanovsky, F.L.Dotti. Structuring Specifications with Modes. Fourth Latin-American Symposium on Dependable Computing - LADC 09, September 1-4, 2009]</ref> and <ref>[http://deploy-eprints.ecs.soton.ac.uk/153/1/paper105%2DICFEM09.pdf F.L.Dotti, A.Iliasov, L.Riberiro, A.Romanovsky. Modal Systems: Specification, Reﬁnement and Realisation. In: International Conference on Formal Engineering Methods - ICFEM 09 , December 9 -12, 2009, Rio de Janeiro, Brazil]</ref>, and fault tolerance <ref>[http://www.cs.ncl.ac.uk/publications/trs/papers/1188.pdf I.Lopatkin, A.Iliasov, A.Romanovsky. On Fault Tolerance Reuse during Refinement. In: 2nd International Workshop on Software Engineering for Resilient Systems - SERENE 2010, April 13-16, 2010, London]</ref>.
			* Also, we are working on a medium-scale case study

	==== Qualitative Reasoning ====		==== Qualitative Reasoning ====

imported>Ilya.lopatkin: /* Modes */

2010-12-03T13:31:41Z

Modes

← Older revision		Revision as of 13:31, 3 December 2010
Line 59:		Line 59:

	==== Modes ====		==== Modes ====
	~~We have conducted a study of approaches~~ to ~~complex critical systems development, and the requirements documents within DEPLOY, and arrived at the following:~~		The main objective in the tool design was to make a simple to use environment that can be used by a non-Event-B user (e.g. requirements engineer, fault tolerance specialist), yet provides the necessary functionality for an Event-B modeller. The tool was designed to be as much an external environment to Event-B models as possible.
	* Separation of concerns is a ~~major approach~~ to ~~tackle the complexity of the systems development.~~		* We decided not to extend the Rodin database with modal and fault tolerance elements and to keep them as separate models. This led to less platform dependencies and easier maintenance.
	* A large amount of critical systems are developed using a ~~notion of operation modes.~~		* The static check is separated from the Rodin SC, and realized by the GMF validation since it does not logically belong to Rodin / Event-B. However, since the proofs are a part of the modelling process, we properly extended the Rodin proof obligation generator.
	* All critical systems involve operations with important aspects of human activity (e.g. ~~lives~~, finance) hence critical. And all of them inevitably have faults due to changing environmental conditions, hardware failures etc. A high percentage of requirements to such systems (up to 40% according to our study within DEPLOY) include fault tolerance ~~as a way to mitigate the consequences of errors.~~		* A modal/FT documents form a refinement chain that mimics the Event-B refinement. This allows our tool to be used with the existing types of decomposition / modularisation.
	* Requirements evolve, ~~including FT.~~		* During the initial experiments we have identified a possible need for multiple views on a single model. The tool supports this by keeping the references to the models in the views and not the opposite.

	~~There were neither mode nor fault tolerance viewpoints in~~ the ~~state of the art~~ Event-B ~~development~~. The ~~UML-B approach of statecharts is closely related~~ to ~~modal views. However, the statecharts drive the development by generating~~ Event-B models as ~~opposed~~ to the ~~mode views which facilitate~~ the ~~development~~ by ~~leaving~~ the Event-B ~~modelling activity with the user~~. On the ~~fault tolerance side, we~~ are ~~aware~~ of the ~~work on ProR framework for tracing requirements~~, ~~and~~ we ~~plan to integrate~~ the ~~tracing framework with our modelling approach~~.

	~~The Mode~~/FT ~~Views approach is to assist~~ the ~~main~~ Event-B ~~development by an additional set of abstractions and a toolset~~ to ~~facilitate modal and fault tolerance development. We were motivated by the following stimuli:~~
	* Facilitate the modal and fault tolerance development in Event-B with ~~a comprehensible modelling approach.~~
	* Stimulate the ~~consideration~~ of ~~fault tolerance at the very first phases of development~~.
	* ~~Explicitly covering mode and fault tolerance concerns,~~ we ~~wanted to improve the requirement traceability and fulfilment~~.
	* Help make planning decisions. Focusing the ~~developer attention on specific aspects of development leads~~ to ~~better understanding of~~ the ~~problem~~ and ~~planning of~~ the ~~solution.~~
	* Provide consistent way of stepwise development of mode and FT aspects by a notion of views refinement.

	==== Qualitative Reasoning ====		==== Qualitative Reasoning ====

imported>Ilya.lopatkin: /* Modes */

2010-12-03T13:25:17Z

Modes

@@ Line 21: / Line 21: @@
 ==== Modes ====
-(Ilya)
+We have conducted a study of approaches to complex critical systems development, and the requirements documents within DEPLOY, and arrived at the following:
 ==== Qualitative Reasoning ====

imported>Ilya.lopatkin: /* Modes */

2010-12-03T13:24:54Z

Modes

@@ Line 46: / Line 46: @@
 ==== Modes ====
-(Ilya)
+We have conducted a study of approaches to complex critical systems development, and the requirements documents within DEPLOY, and arrived at the following:
 ==== Qualitative Reasoning ====