D32 Scalability

Overview

Regarding scalability of the Rodin platform, the following contributions has been made:

• Flows plug-in development. The main purpose of the Flows plug-in is to give a modeller a clean and concise view of the control flow aspects of a model without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tool is developed by Newcastle University with the requirements and suggestions from Bosch and SAP.

• Group Refinement. Group refinement plug-in is a tool realising an alternative set of Event-B refinement laws in the Rodin platform. It lets a modeller to switch to differing style of event atomicity refinement for the scope of a single refinement steps. For a certain case of atomicity refinement the alternative laws result in a more natural and compact model with fewer and simpler proof obligations. The method and the tool were development by Newcastle University, the pattern of refinement was discovered by the Bosch formal modelling team.

• Modes. The Mode and Fault Tolerance Views plug-in is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. As many systems are developed using the notion of operation modes, the tool allows to separate the modal modelling as a refinement chain from the main Event-B models. This makes possible to model explicitly modal behaviour and certain fault tolerance aspects of systems and formally show the consistency between the models and their views. The theory and plug-in were developed by Newcastle University.

• Emre Yilmaz and Thai Son Hoang (ETH Zurich) has developed a plug-in supporting an extension of Event-B with qualitative reasoning. The extension allows developer to declare an event converges probabilistically (with probability 1). This is in contrast with standard certain termination, where convergent events must decrease the declared variant. Provided that the variant is bounded above, an event probabilistically converges if it might decrease the variant. The extension enables Event-B to model systems with almost certain termination properties, e.g. IEEE 1394 Firewire protocol or Rabin's Choice Coordination algorithm .

Motivations

Flow plug-in

The flows tool was applied by Bosch in the development of the cruise control model to verify deadlock-freedom and liveness properties of the model. Being a sizable case-study, this was an important test for the ideas and techniques behind the plug-in. The general conclusion was that a tool of this kind is essential and the current version should be improved in many directions. This experience has uncovered a rather fundamental issues with the size and complexity of the generated proof obligations. These were the largest theorems ever generated in Rodin and the only positive aspect is that this helped to stress-test and debug the proof handling facilities of the Rodin. It was clear that such proof obligations can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.

Group Refinement

One of the project industrial partners (Bosch) has identified a recurring refinement pattern that did not fit well the existing laws of refinement. It is a case of atomicity refinement where a previously atomic action (event) is split into a number of steps which combined effect achieves the effect of the abstract atomic event. The Event-B approach is to introduce new variables in a refinement machine and thus have a hidden concrete state on which the steps are defined. There is a further event summarising the effect of the computations accomplished on the hidden state and explicitly relating it to the abstract state. This is the event for which the refinement relation is demonstrated while the events defining the actual computation steps would have no formal link to the abstract event.

When the hidden state does not naturally follow as a part of the modelling process this refinement style leads to a contrived model. There appear auxiliary variables and auxiliary events that play no part in the characterisation of the system behaviour but are a codification of the refinement relation to an abstract model. Since such elements accumulate during refinement this has a profound effect on the development of a large model.

Modes

(Ilya)

Qualitative Reasoning

Probability is used in many distributed systems for breaking the symmetry between different components/processes, e.g. IEEE 1394 Firewire protocol , Rabin Choice Coordination algorithm . For such systems, termination cannot be guaranteed for certain. Instead, a slightly weaker property is mostly appropriate: termination with probability one. As an example for this type of systems is to consider tossing a coin until it comes up tail. Provided that the coin is fair (in that sense that no face is ignored forever), eventually, the coin will eventually come up head.

Qualitative probabilistic reasoning has been integrated into Event-B : a new kind of actions is added, namely probabilistic actions with an assumption that the probability for each possible alternative is bounded away from 0 or 1. Most of the time, probabilistic actions behave the same as (standard) non-deterministic actions (e.g. invariant preservation). The difference between probabilistic and non-deterministic actions is with convergence proof obligation: probabilistic actions are interpreted angelically, whereas non-deterministic actions are interpreted demonically. The result is a practical method for handling qualitative reasoning that generates proof obligations in the standard first-order logic of Event-B.

The plug-in allows developers to declare an event to be probabilistic convergent and generate appropriate proof obligations. Since the obligations are in standard first-order logic supported by the Rodin platform, we do not need to make any extension for the provers to handle the new proof obligations.

Choices/Decisions

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.

Group Refinement

In this work one obvious source of inspiration is the Classical B method where an abstract atomic statement may be refined into an operation which body is made of a sequence of assignments. However, the introduction of the semicolon operator in Event-B is a substantial change affecting most aspects of the method. This would also reintroduce one of the problems of the Classical B that Event-B tries to address: proof scalability. Accumulation of sequential composition through refinement steps may result in unmanageable proof obligations. It is also more difficult to conduct subsequent refinement of events with sequential actions.

Actions Systems has an atomicity refinement technique where one can refine an atomic action into a loop of new actions. This is general enough to address the problem but, seemingly, the associated proof cost is prohibitively high and there is no evidence that such proofs may be efficiently mechanised.

The challenge was addressed by offering a method that lets a modeller to select an alternative set of refinement laws whenever the identified pattern of refinement is encountered. The new refinement laws are based on a different interpretation of a model: split refinement (a case of event refinement when an abstract event is refined into two or more concrete alternatives) is understood as a refinement into a composite event made of the concrete events arranged in some way. One simple arrangement case is when the concrete events are understood to execute sequentially. Then the refinement relation is demonstrated for the after-state produced by executing one event after another.

The method is not limited to sequential composition and there is also a form of parallel composition. An essential property of the method is that the group refinement relation is demonstrated not just for a single arrangement of concrete events but for a whole set of traces of concrete events. There is a simple notation for the removal of undesired traces and constraining the model to specific traces. For each trace there appears one instance of action simulation proof obligation (and possibly other refinement and consistency proof obligations). Thus, for practical reasons, it is necessary to keep number of traces low. This is best accomplished by doing small refinement steps with few concrete events.

Modes

(Ilya)

Qualitative Reasoning

• Ideally, we would like to have a new value for the convergence attribute of Event-B events. However, this is not currently supported by the Rodin platform. Instead, a new probabilistic attribute is defined for events, with the value is either standard or probabilistic.

• Since standard refinement does not maintain probabilistic convergent property, we put a restriction on the development method for almost-certain termination systems in two steps as follows.
  1. Establish the model of the systems with various anticipated events
  2. While proving convergence properties of events (either standard or probabilistic), we keep the variable and event system the same (i.e. no refinement is allowed).

• For probabilistic convergence, the variant need to be bounded above. A combination of standard and probabilistic convergence events results in a probabilistic convergence system. Moreover, the use of anticipated events and refinement allowed us to construct an lexicographic variant by combining the sub-variant at different level of refinements. For probabilistic convergence system, this lexicographic variant need to be bounded above, which require all the sub-variants to be bounded above (not only those variant concern with probabilistic events).

More details of our approach is in our report at AVoCS'10 .

Available Documentation

Flow plug-in

• An extensive example of the application of the flows in the modelling (the old version) is available to the DEPLOY Project members as a part of the Bosch cruise control case study.
• There is a wiki page describing the core proof obligations generated by the tool - Flows
• Tutorial slides available from the project file share

Group Refinement

• There is a wiki page - Group refinement plugin - briefly introducing the approach and the tool
• Slides

Qualitative Reasoning

• Master thesis of Emre Yilmaz on developing tool support for qualitative reasoning in Event-B .

• The development of Rabin's Choice Coordination Algorithm is available at the DEPLOY Repository .

• A paper describing the development of Rabin Choice Coordination algorithm and tool support in the Proceedings of AVoCS'10 .

Planning

Flow plug-in

The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and feature requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.

Group Refinement

The immediate plan is to produce a technical report on the semantics of group refinement during the first quarter of 2011. Long term plans are the tool maintenance and the investigation of the possibility of more expressive form of group refinement permitting branches and loops.

Modes

(Ilya)

Qualitative Reasoning

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.