Formal Verification

Formal verification of the interactions of the API of the PRiME Framework has been performed using several methods, including using the Event-B language. These methods are described in this page.

Control Flow Diagrams

ERS (Event Refinement Structure) is a hierarchical technique to illustrate the explicit control flow of a system. ERS has been used within the formal Event-B model of the framework to manage and verify the control flows of the Framework's API and refine the relationships between them. In this wiki page, ERS diagrams present the control flows between the API functions in each module.

An ERS diagram is read from left to right, indicating the ordering between nodes. The following constructor parameters are defined that describe specific behaviour in some diagrams:

The and constructor eases the ordering of nodes, indicating that multiple nodes can be interleaved.
The loop constructor indicates that zero or more iterations of the associated node can be made at that point in the event structure.
The par constructor indicates that interactions are parameterised by the selection of an instance from a defined set.

Abstract ERS Diagram

Above is the abstract illustration of the Framework's API (red arrows in the block diagram on the Home page). The top level of the system, PRiME Framework is the root node. This is divided into interactions between the application and the RTM (app::RTM node) and interactions between the RTM and the device (RTM::dev node). The first set of interactions are parameterised by selecting application a from the set of applications APPS. There is no parameterisation of the device since the entire platform is captured under a single device.

The interactions between applications and RTM (app::RTM) is further divided into an application API node (app::API), and an RTM API node for interactions with the application (RTM::app::API).

The app::API node is refined in Application API Control Flows
The RTM::app::API node is refined in RTM-to-Application API Control Flows

The interactions between the RTM and the device (RTM::dev) is further divided into an RTM API node, for interactions with the device (RTM::dev::API), and a device API node (dev::API), for interactions from the device to the RTM.

The RTM::dev::API node is refined in RTM-to-Device API Control Flows
The dev::API node is refined in Device API Control Flows

Application API Control Flows

This section describes refinements of the app::API node.

Application Registration & Deregistration

The ERS for the application API (app::API) is divided into four sub-nodes. Function calls are defined in the following order:

application registration (reg)
application knob management (app::knob::manage)
application monitor management (app::mon::manage)
application de-registration (dereg)

The abstraction of application knob management functions (app::knob::manage) is refined in Application Knob Interactions and monitor management functions (app::mon::manage) are refined in Application Monitor Interactions)

Application ERS Diagram

Application Knobs

The ERS for the management of application knobs is divided into five sub-nodes. Function calls are defined in the following order:

knob registration (knob_reg)
loop 1 or more, knob minimum boundary update (knob_min)
loop 1 or more, knob maximum boundary update (knob_max)
loop 1 or more, get knob value (knob_get)
knob de-registration (knob_dereg)

The reg and dereg functions are placed first and last to indicate that the loop functions must occur after registration and before de-registration.

Application Knob ERS Diagram

Application Monitors

The ERS for the management of application monitors is divided into six sub-nodes. Function calls are defined in the following order:

monitor registration (mon_reg)
loop 1 or more, monitor minimum boundary update (mon_min)
loop 1 or more, monitor maximum boundary update (mon_max)
loop 1 or more, monitor weight update (mon_weight)
loop 1 or more, set monitor value (mon_set)
monitor de-registration (mon_dereg)

Application Monitor ERS Diagram

Combined Application Control Flow

The merged ERS diagram below illustrates control flows across different refinement levels. For example it illustrates the below requirements:

Application "must" be registered by the framework before application knobs and monitors can be registered, ensured by ordering of app::reg to app::knob::reg and app::mon::reg.
Application knobs and monitors "must" all be deregistered from the framework before an application can deregister, ensured by ordering of app::knob::dereg and app::mon::dereg to app::dereg.

Application Monitor ERS Diagram