Generic Instantiation User Guide

User:Son at ETH Zurich is in charge of the plug-in.

Introduction

The Generic Instantiation plug-in provides supports for instantiating an Event-B Models by providing concrete values for carrier sets and constants.

Installing and Updating

The plug-in is available through the main Rodin Update Site under Composition and Decomposition category.

News

• 11.05.2012: Version 0.2.2 released for Rodin 2.5.*

Usage

We use a small example to illustrate the usage of the Generic Instantiation plug-in. The archive of the example is available here, which can be imported into the Rodin platform. The archive contains to projects called Channel and Negotiation. Channel is the abtract base project. Negotiation is the concrete target project: models of Channel will be instantiated within the contexts of Negotiation.

The Channel project contains the following components:

• Context message_ctx contains carrier set MESSAGE representing the set of possible messages exchanged.

• Machine channel sees message_ctx. The machine specifies transfering of some messages from a sender to a receiver.

• Context size_ctx contains constant channel_size representing the maximum number messages allowed in a channel.

• Machine EO sees message_ctx, size_ctx and refines channel. The machine specifies that the messages are sent exactly-one.

• Machine EOIO sees message_ctx, size_ctx and refines EO. The machine specifies that messages are sent exactly-one and in-order.

The Negotiation project contains the following contexts:

• Context bandwidth_ctx contains constant bandwidth representing the bandwidth of the connection between partners

• Context proposal_ctx contains carrier set PROPOSAL representing the proposals sending between partners, constant proposal_size representing the size of each proposal, and constant package_size respresenting the maximum number of proposals within each message.

Instantiation

We are going to instantiate the development in Channel, in particular the refinement up to EOIO by instantiating the abstract carrier set MESSAGE and abstract constant channel_size. Each message contains a number of proposals (no more than package_size), each proposal has the size specified by proposal_size. As a result, we instantiate MESSAGE by POW(PROPOSAL) and channel_size by bandwidth / (proposal_size * package_size). The instantiation is done via a wizard as follows.

• Open the New Wizard Dialog (File/New/Other) and choose Event-B Generic Instantiation.

• The first page of the wizard is for choosing the different components for instantiation.

1. Base machine: The abstract base machine. Choose Channel as the base project and EOIO as the base machine.
2. Seen contexts: The contexts in the target projects that will be used. Choose Negotiation as the target project, and select both bandwidth_ctx and proposal_ctx. Select Next to go to the next page.

• The second page of the wizard is for entering instantiation for carrier sets and constants.

1. Enter POW(PROPOSAL) for MESSAGE
2. Enter bandwidth / (proposal_size * package_size) for channel_size

The expressions will be translated to Event-B mathematical expressions.

Select Next to go to the next page.

• The third page of the wizard is for saving the instantiation information for later use. We save the information into a file named GenInst.

Select Finish to complete the wizard.

• The following components are generated by the wizard.

1. A generic instantiation file named GenInst.
2. A context named GenInst.
3. A machine named channel.
4. A machine named EO.
5. A machine named EOIO.

The machines are copied of the original abstract machines in Channel with replacement appropriately of the carrier set and constant.

All machines see the new context GenInst. The context is as followed where the axioms of the original abstract context are instantiated accordingly and specified as theorems of the new context. At the moment the original abstract thoerems are instantiated and specified as thoerems of the new context, but the proof obligations associated with these instantiated theorems can be ignored.

Explanations for some warning and error messages

• Undefined based machine. No based machine is chosen.

Additional features to be investigated/implemented

• There is currently no sanity checking for the instantiation. Users need to make sure that their instantiated model can be analysed and proved by Rodin.
• Supressing proof obligations for instantiated theorems.
• Often ones instantiate a small part of the context rather than the whole context. Idealy, the tool should take the some minimum input and instantiate the model accordingly.