Difference between pages "Railway Interlocking Feedback" and "Refactoring Framework"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
m (link)
 
imported>Renato
 
Line 1: Line 1:
−
{{TOCright}}
+
{| align="right"
−
A case study has been carried by [[Systerel]] to verify the specification of an automated
+
| __TOC__
−
interlocking system by means of system modeling with event-B. This paper gives
+
|}
−
an overview of the work done and of some of the results.
+
 
 +
==News ==
 +
* ''5th November 2009'': [[#Version_0.0.4|Version 0.0.4]] released. It is based on Rodin 1.1.0.
 +
* ''2nd November 2009'': [[#Version_0.0.4|Version 0.0.4]] released. It is based on Rodin 1.1.0.
 +
* ''3rd July 2009'': [[#Version_0.0.2|Version 0.0.2]] released. It is based on Rodin 1.0.
 +
* ''1st July 2009'': [[#Version_0.0.1|Version 0.0.1]] released. It is based on Rodin 1.0.0 RC1.
 +
 
 +
==The Rename Refactoring Plug-in ==
 +
 
 +
[[User:Renato]] at [[Southampton]] is in charge of the [[Refactoring Framework]].
 +
 
 +
One of the most recurring requirement from users of the Rodin platform is to have simple means for renaming modeling elements.  Users want to have a unique operation that will rename an element both at its declaration and all its occurrences. Moreover, they require that renaming an element doesn't modify their existing proof state (no loss of proof).
 +
 
 +
This requirement falls in the more general context of ''refactoring''. In software engineering, "refactoring" source code means improving it without changing its overall results, and is sometimes informally referred to as "cleaning it up". In the case of the Rodin platform, the refactoring framework is related to the first option, where refactoring should not change the overall behaviour of the files/elements, nor loosing proofs.
 +
 
 +
The following diagram shows the architecture of the refactoring framework.
 +
 
 +
[[Image:Architecture_refactoring_framework.jpg]]
 +
 
 +
==The Rename Refactoring Framework Architecture ==
 +
 
 +
Currently, it is being developed the application of such framework to event-b files (context, machines, proofs obligations, etc) and elements (constants, variables, carrier sets, etc). There are still some tests to be run for the different elements of contexts and machines. The next goal would be to apply and use this framework on Rodin (together with file editors or perspectives).
 +
 
 +
[[Image:RefTree.jpg‎]]
 +
 
 +
==== Refactoring Trees after processing the extension points ====
 +
 
 +
Since there are proof obligations associated with Event-B files, while renaming the goal would be to cause the less effort as possible on re-proving and if possible re-using the proofs that are already discharged. The refactoring should not change the semantic of any of the elements/files. Instead, it should just change names or labels, so the proofs should not have to be re-generated (nor re-discharged). That is one of final goals while applying of this framework to Event-B.
 +
 
 +
==Initial Work ==
 +
 
 +
Initial work towards implementation of this framework is described in [http://www.stups.uni-duesseldorf.de/thesis_detail.php?id=9 Sonja Holl's Bachelor thesis]
 +
 
 +
==Installing/Updating ==
  
−
This study was supported by the [http://www.ratp.fr RATP] (French organization in charge of Paris
+
The installation or update for the renaming/refactoring plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates). Like always, after the installation, restarting the application is recommended.
−
transportation).
 
  
−
== Context and Goals ==
+
==Usage ==
−
Some RATP units are responsible for evolution and maintenance of an automated
 
−
interlocking specification document.
 
  
−
In order to improve their paper and pencil process, RATP asked Systerel if
+
The Renaming/Refactory plug-in allows the renaming of:
−
Event-B could be useful to them. An eight month study was launched  whose 
 
−
main goal was to help RATP improving their confidence in their interlocking
 
−
specification, by applying an Event-B approach on rewriting their requirement
 
−
document.
 
  
−
== Description of Work ==
+
* Variables
−
The main difficulty that arose at the very beginning of the study was to
+
* Parameters
−
answer the initial question: ''what does a "working interlocking system"
+
* Carrier Sets
−
mean?''
+
* Constants
 +
* Events
 +
* Other labelled elements (invariants, axioms, guards, etc)
  
−
In an attempt to both answer this question and stay within the expectations of
+
====Requirements before using ====
−
the railway's people, we chose to allocate a great chunk of time to the
 
−
elaboration of our own requirements specification, by rewriting the RATP specification
 
−
with the organization and the wording of our choice. This task was carried
 
−
before doing any modeling work and was aimed at introducing safety principles
 
−
and safety concepts step by step.
 
  
−
The obtained requirement specification was to be approved by the domain
+
Before using the renaming/refactory, all the files in the project should be saved ( it will be asked to save in there are any unsaved files). There should be no errors in the project, otherwise it could lead to even more errors after applying the renaming.
−
experts and to serve as a reference for the modeling task.
 
  
−
Our modeling process was thus broken down as follow:
+
==== Steps of usage ====
−
# Writing an autonomous requirements specification approved by the domain experts,
 
−
# Designing a refinement plan,
 
−
# Modeling the system and proving it correct.
 
−
The whole process was highly iterative. Indeed, it often appears while
 
−
modeling that some concepts still need refinements or adjustments which  in
 
−
turn lead to a rework of the refinement plan or the model.
 
  
−
<center>
+
# User selects element to be renamed at the Event-B Explorer
−
{{SimpleHeader}}
+
# By right clicking in the element, there should appear an option 'Refactory...'. Selecting that option should open a wizard [[Image:refactory menu.png]]
−
|+Structure of the B model.
+
# User introduces new element name in the first page of the wizard. Then click in 'Next'. [[Image:new_name_wizard.png]]
−
|-
+
# A list of related files is created and the plug-in check for possible clashes and returns a report
−
|Collision avoidance
+
# User decides if he wants to execute renaming (by clicking in 'Finish')
  
−
(2 levels)
 
−
|-
 
−
| Environment structures
 
  
−
(5 levels)
+
 
−
|-
+
       
−
| Control principles
+
[[Image:refactory_report_wizard.png]]
  
−
(4 levels)
 
−
|-
 
−
| Instantiation (4 levels)
 
−
* signal
 
−
* switch command
 
−
* transit locking
 
−
* opposing locking
 
−
|}
 
−
</center>
 
  
−
The achieved model, which overall structure is shown in table here before,  
+
== Bugs, Features and Comments ==
−
contains fifteen levels of refinement.  
+
 
 +
''Any reports of bugs, features or comments are welcome. You can add any of them here.''
 +
 
 +
====Bugs ====
 +
* Renaming does not work when renamed element is in variant (fixed in v0.0.5)
 +
* Renaming proofs did not propagate over related files (fixed in v0.0.5)
 +
 
 +
====Features Request====
 +
* Implement UNDO for renaming
 +
 
 +
====Comments ====
 +
* -
 +
 
 +
== Releases ==
 +
 
 +
=====Version 0.0.4 =====
 +
 
 +
''5th November 2009''
 +
 
 +
A release of renaming/refactory (v0.0.4) compatible with Rodin v1.1.0 is available in the main Rodin update site (bug fix from 0.0.3). Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated (IMPORTANT).
 +
 
 +
*Bug fix
 +
** Renaming of proofs would not save the proof files after renaming
 +
** Renaming of labelled elements would not update the proofs.
  
−
== Results ==
+
*Possible Problem
−
The study led to several interesting results either by giving some clues about
+
** If you try to rename and the operation runs successfully without any errors but does not have any effect, you should:
−
a better way for building an event-B model for a real world system, or about
+
*** First, try to fix the renaming manually on the respective file (or using the renaming framework, revert to the original name)
−
the quality of the automated interlocking specification, object of this study.
+
*** Try to make a CLEAN and BUILD to ensure that the Rodin indexer is updated before the renaming.
 +
*** Run the renaming again and should be working fine.
  
−
=== Organization ===
+
=====Version 0.0.3 =====
−
Our first intention was to teach some basics of event-B to the domain experts
 
−
in order to allow them to at least follow, and at best approve, the modeling
 
−
steps.
 
−
It proves as a bit utopian. It would certainly have needed a lot more of
 
−
teaching effort to be efficient.  
 
  
−
It is of interest to note that at the end of the study, the results were
+
''2nd November 2009''
−
perceived by the domain experts as ''magical'' ones:  the failure scenarios
 
−
exhibited seem to come from nowhere (in fact, proof obligations of the
 
−
B model that couldn't be discharged), in contrast to the
 
−
scenario they are used to, which come from several decades of field
 
−
feedbacks. Those ''magical scenario'' nonetheless were pertinents.
 
  
−
=== Modeling Process ===
+
A release of renaming/refactory (v0.0.3) compatible with Rodin v1.1.0 is already available in the main Rodin update site. Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated.
−
The modeling process we have planned had some place for improvements (some of
 
−
which were applied during the study). They are summed up hereafter:
 
  
−
==== Process for Industrial Strength Models ====
+
*Features
−
There is a need for a more robust modeling process, perhaps somewhat similar
+
** Renaming of machines and contexts is possible using the indexers. After the renaming of a machine/context, the change is propagated over the related files
−
to those being used at the software level. An industrial modeling process
+
** Renaming of proofs: after the renaming, the proof obligations are also updated to reflect the renaming. It might be necessary to manually refresh the status of some proof obligations (although the proof is already discharged). This renaming is not fully-functional at the moment and some discharged proof obligations may have to be discharged again. We intend to fix this problem in the future.
−
probably needs the following phases:
 
−
* Requirements specification,
 
−
* Validation tests definition,
 
−
* Refinement planning,
 
−
* Modeling and proving,
 
−
* Validating.
 
  
−
The requirements specification rewriting phase done at the beginning of the
+
=====Version 0.0.2 =====
−
study involved a lot of refactoring and lead to a final document that was too
 
−
far from the domain experts expectations to be fully approved.
 
−
Animation looks like ''a must have'' to ease model validation by domain
 
−
experts.
 
  
−
It is also worth to note that seeking for a posteriori justification, as was done
+
''3rd July 2009''
−
in this study, is very difficult. Indeed, the system was obviously not designed
 
−
to be proved.  In fact, it appears to us that most of existing industrial
 
−
systems were not designed with validation in mind.
 
  
−
==== Modeling Techniques ====
+
*Bugs
−
Our model didn't explicitly take into account  degraded cases
+
** Validate if new name is in the list of reserved words of Event-B (dom,ran, card, etc)
−
for the system.  It proved to be a bad design choice and it was a burden for
 
−
the proof of the model, as event guards become more and more complex
 
−
throughout the refinement levels.  As a consequence, it appears that models
 
−
need to be totally closed, and thus should not only take into
 
−
account the controller and its environment, but also degraded
 
−
cases.
 
  
−
Models also appears to contribute to at least two goals:
+
=====Version 0.0.1 =====
−
* prove properties over the system modelled,
 
−
* help the conceptualization (as an intellectual tool for reasoning)
 
  
−
As a conclusion, we can also say that refinement appears more and more as an
+
''1st July 2009''
−
essential concept for successful modeling.
 
  
−
=== DIR 41 Analysis ===
+
A release of renaming/refactory (v0.0.1) compatible with Rodin v1.0.0 is already available in the main Rodin update site.  
−
Some essential concepts for the railway domain were refined during the study.
 
−
For example the ''safety statement'' was refined to a ''safety preservation''
 
−
one: the interlocking system actions should not decrease the  
 
−
current safety level.
 
  
−
And probably the most prominent result is that four potential
+
Note that this version is still a prototype so prone to errors. So it is suggested to back up the projects before starting to use the renaming plug-in. The plug-in uses the most recent version of Rodin Indexer. Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated.
−
safety flaws were exhibited (with an expected low
 
−
probability of occurrence), which are now being tackled by the RATP teams. It
 
−
also revealed the existence of several implicit hypotheses on the environment
 
−
behaviour or on the design of the railway network.
 
  
−
== Conclusion ==
+
Although one of the goals is to the rename the respective proof obligations, this feature is not available in this version. It should be available in the next release. If you find bugs or errors, please let me know by updating this wiki-page or [mailto:ras07r@ecs.soton.ac.uk email].
−
Modeling a system with event B proved to be very interesting for pointing out
 
−
potential safety flaws and for proving global safety.
 
  
−
This way of modeling allows a B expert with little knowledge in an industrial
+
[[Category:Design]]
−
domain to quickly grasp the domain core concepts. It is still
 
−
very difficult to involve the domain experts in the whole process and we have
 
−
high expectations that model animation would improve this.
 

Revision as of 16:08, 13 January 2010

News

  • 5th November 2009: Version 0.0.4 released. It is based on Rodin 1.1.0.
  • 2nd November 2009: Version 0.0.4 released. It is based on Rodin 1.1.0.
  • 3rd July 2009: Version 0.0.2 released. It is based on Rodin 1.0.
  • 1st July 2009: Version 0.0.1 released. It is based on Rodin 1.0.0 RC1.

The Rename Refactoring Plug-in

User:Renato at Southampton is in charge of the Refactoring Framework.

One of the most recurring requirement from users of the Rodin platform is to have simple means for renaming modeling elements. Users want to have a unique operation that will rename an element both at its declaration and all its occurrences. Moreover, they require that renaming an element doesn't modify their existing proof state (no loss of proof).

This requirement falls in the more general context of refactoring. In software engineering, "refactoring" source code means improving it without changing its overall results, and is sometimes informally referred to as "cleaning it up". In the case of the Rodin platform, the refactoring framework is related to the first option, where refactoring should not change the overall behaviour of the files/elements, nor loosing proofs.

The following diagram shows the architecture of the refactoring framework.

Architecture refactoring framework.jpg

The Rename Refactoring Framework Architecture

Currently, it is being developed the application of such framework to event-b files (context, machines, proofs obligations, etc) and elements (constants, variables, carrier sets, etc). There are still some tests to be run for the different elements of contexts and machines. The next goal would be to apply and use this framework on Rodin (together with file editors or perspectives).

RefTree.jpg

Refactoring Trees after processing the extension points

Since there are proof obligations associated with Event-B files, while renaming the goal would be to cause the less effort as possible on re-proving and if possible re-using the proofs that are already discharged. The refactoring should not change the semantic of any of the elements/files. Instead, it should just change names or labels, so the proofs should not have to be re-generated (nor re-discharged). That is one of final goals while applying of this framework to Event-B.

Initial Work

Initial work towards implementation of this framework is described in Sonja Holl's Bachelor thesis

Installing/Updating

The installation or update for the renaming/refactoring plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates). Like always, after the installation, restarting the application is recommended.

Usage

The Renaming/Refactory plug-in allows the renaming of:

  • Variables
  • Parameters
  • Carrier Sets
  • Constants
  • Events
  • Other labelled elements (invariants, axioms, guards, etc)

Requirements before using

Before using the renaming/refactory, all the files in the project should be saved ( it will be asked to save in there are any unsaved files). There should be no errors in the project, otherwise it could lead to even more errors after applying the renaming.

Steps of usage

  1. User selects element to be renamed at the Event-B Explorer
  2. By right clicking in the element, there should appear an option 'Refactory...'. Selecting that option should open a wizard Refactory menu.png
  3. User introduces new element name in the first page of the wizard. Then click in 'Next'. New name wizard.png
  4. A list of related files is created and the plug-in check for possible clashes and returns a report
  5. User decides if he wants to execute renaming (by clicking in 'Finish')



Refactory report wizard.png


Bugs, Features and Comments

Any reports of bugs, features or comments are welcome. You can add any of them here.

Bugs

  • Renaming does not work when renamed element is in variant (fixed in v0.0.5)
  • Renaming proofs did not propagate over related files (fixed in v0.0.5)

Features Request

  • Implement UNDO for renaming

Comments

  • -

Releases

Version 0.0.4

5th November 2009

A release of renaming/refactory (v0.0.4) compatible with Rodin v1.1.0 is available in the main Rodin update site (bug fix from 0.0.3). Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated (IMPORTANT).

  • Bug fix
    • Renaming of proofs would not save the proof files after renaming
    • Renaming of labelled elements would not update the proofs.
  • Possible Problem
    • If you try to rename and the operation runs successfully without any errors but does not have any effect, you should:
      • First, try to fix the renaming manually on the respective file (or using the renaming framework, revert to the original name)
      • Try to make a CLEAN and BUILD to ensure that the Rodin indexer is updated before the renaming.
      • Run the renaming again and should be working fine.
Version 0.0.3

2nd November 2009

A release of renaming/refactory (v0.0.3) compatible with Rodin v1.1.0 is already available in the main Rodin update site. Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated.

  • Features
    • Renaming of machines and contexts is possible using the indexers. After the renaming of a machine/context, the change is propagated over the related files
    • Renaming of proofs: after the renaming, the proof obligations are also updated to reflect the renaming. It might be necessary to manually refresh the status of some proof obligations (although the proof is already discharged). This renaming is not fully-functional at the moment and some discharged proof obligations may have to be discharged again. We intend to fix this problem in the future.
Version 0.0.2

3rd July 2009

  • Bugs
    • Validate if new name is in the list of reserved words of Event-B (dom,ran, card, etc)
Version 0.0.1

1st July 2009

A release of renaming/refactory (v0.0.1) compatible with Rodin v1.0.0 is already available in the main Rodin update site.

Note that this version is still a prototype so prone to errors. So it is suggested to back up the projects before starting to use the renaming plug-in. The plug-in uses the most recent version of Rodin Indexer. Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated.

Although one of the goals is to the rename the respective proof obligations, this feature is not available in this version. It should be available in the next release. If you find bugs or errors, please let me know by updating this wiki-page or email.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Railway_Interlocking_Feedback&oldid=6723’