Keywords

1 Introduction

Rigorous modelling and verification of software intensive systems is an actively developing area of software engineering that is well supported by variety of methods and tools, e.g., model-checking, automated theorem-provers, simulation and animation tools, satisfiability solvers, etc. Usually, these methods and tools allow the developer to construct a formal model of a system under construction and enable verification of critical system properties, such as performance, reliability, safety, etc. One of the goals of rigorous modelling approaches is the support for effective requirements engineering since capturing and structuring valid system requirements remains one of the main challenges in software engineering.

In refinement-based methods, such as Event-B [1], an induction principle is implicitly integrated. It is used for proving correctness properties by discharging proof obligations that are automatically generated. We refer to these features as implicit semantics, as they are provided by the underlying theory (in this case, semantics of Event-B). On the other hand, domain knowledges constitute explicit semantics as they provide external informations about the domain within which system operates. It has been shown that the domain knowledge [4, 5] is crucial and critical to design safe software-based systems which interact with and, or, respond to events originating in environment. For example, consider a data bus ensuring communication among software agents (nodes), and one agent is waiting for data expressed in the metric unit system, while another one requires same data in the imperial unit system. The data here, for example, can be the speed of some vehicle. In this case, respective unit system for each agent provides critical information for further processing the received data. Another case is the evaluation of the velocity of an aircraft, expressed in miles per hour, whereas some other interacting system or component requires a precision in kilometers per hour. As a one more example, consider the problem of positioning: a vehicle is guided by the control system and has the strong requirement to know where it is currently on the route. In this case, it is critical that validation of data on the route should make a clear distinction between an absolute data and a relative data.

Allowing formal methods users and developers to integrate — in a flexible and modular manner — both the implicit semantics, offered by the formal methods, and the explicit semantics, provided by external formal knowledge models (e.g., ontologies), is a major research challenge [3]. In an attempt to tackle this problem, we consider the case study of a Nose Gear velocity system [7]. It is a critical function responsible for estimating the ground velocity of an aircraft. We employ the Event-B modelling language and its inherent refinement technique to formally derive and verify the model of the system. We use this formal model for identifying and evaluating explicit features involved in this development. The case study has been developed using the Rodin platform – an integrated development environment for Event-B [2].

Related work on integrating domain contexts and formal methods includes notes of MacCarthy [8] proposing the introduction of contexts as abstract mathematical entities with useful properties for AI. Here, a context defines the frame related to the domain of the problem. More recently, Schmidtke and Woo [10] studied pervasive computing systems and proposed to formally describe pervasive computing systems as distributed concurrent systems operating on the background of a mereotopological context model. It allows to integrate the operating environment into the model. Finally, Ait-Ameur et al. [3] introduce questions related to the integration of implicit and explicit semantics in proof-based development method.

The paper is organised as follows. Section 2 introduces the Nose Gear velocity problem. In Sect. 3, we present an overview of the case study development and the reader can consult the link http://eb2all.loria.fr for obtaining the Event-B archive of the complete Nose Gear velocity model. Section 4 discusses the paper contribution and summarises the lessons learnt. Finally, in Sect. 5, we conclude by discussion of future research directions.

2 The Case Study and the Modelling Language

The system under consideration is a Nose Gear (NG) Velocity Update function. It is responsible for estimating the velocity of an aircraft while moving on the ground. This case study was first posed as a verification challenge in Third Workshop on Theorem Proving in Certification in 2013. We develop this case study since it represents a typical system consisting of multiple heterogeneous components working together to produce the expected output. It also represents components assuming different domain knowledge regarding received data. Hence, it is suitable for our goal of exposing the need for identifying and integrating explicit semantics in formal modelling. We briefly describe the system and introduce the Event-B modelling language in this section.

In the NG velocity system, the velocity is estimated by calculating an elapsed time for a complete rotation of a nose gear wheel. These rotations are monitored by an electro-mechanical sensor connected to a computer. Whenever there is a complete rotation of the nose gear wheel, the sensor generates a click (also called ‘pulse’), which subsequently generates a hardware interrupt. An interrupt service routine (ISR) of the system is then responsible for serving these interrupts. The ISR increments a 16-bit counter, NGRotations, to capture a complete rotation of the NG wheel, and stores the current time of an update in a 16-bit variable, NGClickTime.

The NG velocity system is equipped with a millisecond counter called Millisecs. This counter is incremented once every millisecond and provides a read-only access of its current value to all components in the system.

Another component of the system is a real time operating system (RTOS), responsible for invoking the update function. The RTOS makes sure that this function is invoked at least once every 500 ms. However, the exact time of each invocation relative to a hardware interrupt is not predictable.

Finally, the update function is responsible for estimating the current velocity of an aircraft on the ground. This estimation is based on currently available values of accessible counters. Estimated velocity is stored in a variable called estimatedGroundVelocity. Update function has a read-only access to Millisecs counter along with NGRotations counter and a global variable NGClickTime. Also, the diameter of the NG wheel is vailable to the function as a compile time constant called, WHEEL_DIAMETER. Moreover, the function can store all the necessary private data required for calculating an estimation of the ground velocity. These values are protected from invocation to invocation.

There is one explicit requirement for this system, EXFUN-1: While the aircraft is on the ground, the estimated velocity shall be within 3 km/hr of the true velocity of the aircraft at some moment within the past 3 s. Along with EXFUN-1, we have systematically extracted several other implicit/derived requirements from this requirements description. In the next section, we present the formal model of the system and address these requirements.

Event-B [1] is a formal modelling language for expressing state-based models of reactive systems. It is supported by two proof-assistant-based environments, namely Rodin [2]. The construction of an Event-B model is based on concepts like sets, constants, axioms, theorems, variables, invariants, events; these syntactic constructions are organised in two kinds of structures, namely contexts for modelling static informations and machines or expressing events modifying state variables satisfying invariants and safety properties. The validity of a context and a machine is achieved by discharging generated proof obligations using proof assistants. Proof obligations states conditions derived from the principles for deriving safety and invariance properties. We are not giving details of syntax and semantics of Event-B and we will progressively add more details when developing the case study in the next section.

3 Development of Nose Gear Velocity

In this section, we present our attempt on formal modelling of the NG velocity update function. This development has been performed with a traditional Event-B modelling approach. That is, we do not treat domain features (explicit semantics) differently in this development but rather use it as a starting point for that purpose, and identify them.

The development strategy employed for this modelling is such that we start with a very unconstrained view of the system. We introduce all components of the system independently in an incremental fashion, and then, in later refinement steps, we establish relationships between these components as per requirements. As we proceed, we gradually unfold a detailed representation of the system, with an attempt to address a single functionality (or a system component) at each refinement level. Finally, once all necessary relationships between components have been established, we address the main requirement, EXFUN-1.

3.1 Initial Model: Updating Ground Velocity

The initial model is the most abstract specification of the system. It introduces the most fundamental functionality of the system – estimation of the ground velocity – at utmost abstract level. Hence, this model consists of a single event addressing an estimation of the ground velocity, which states what is expected of our system and not how this estimation is performed.

A state variable esmt_velocity stores a current estimated velocity of an aircraft, while event updateGroundVelocity states that esmt_velocity holds some value in MPH unit. A variable old_velocity records an old estimated value when esmt_velocity variable is updated with a new estimation. The record of the old velocity is required to specify system properties (for instance, “estimated velocity is always available”) later in the development.

figure a
figure b

The context for this model introduces new type MPH (stands for miles per hour) to model estimated ground velocity. This type is abstractly specified by a set MPH and (constant) injective function \(mph \in \mathbb {N}\rightarrowtail MPH\).Footnote 1 Note that we make use of explicit types to model units in this development. This design decision based on two observations – (1) model is easier to communicate with other stakeholders (designers, developers, etc.), as it becomes explicit regrading manipulations of types and their use; (2) from modelling perspective, assigning types (rather than treating them subsets of \(\mathbb {N}\)) creates distinct entities which results in more transparent proofs.

3.2 First Refinement: Introducing Time Progression

The NG velocity system is primarily constrained by the time. Our first refinement introduces a milliseconds counter incrementing for each millisecond. With this counter we capture the progression of time for the system. As stated in the system description, we have to model milliseconds counter with a 16-bit capacity constraint. We assume that the counter is unsigned. Hence, the counter is modelled with a modular semantics.

To model the progressing time, we introduce four new variables Millisec, dummyTick, updateTime, updateRecords and one new event MillisecTicks in this refinement.

figure c

    Context for this refinement introduces a new set MILLISECOND and three constants. The set MILLISECOND is used as a distinct type to represent the time in milliseconds.

figure d
figure e

   Event MillisecTicks models the progression of time for the system.

Introduction of the time here is necessary to establish various properties of the system in the later development. As Millisec counter has to be 16-bit, the problem is to model and establish properties related to continuous progression of time within Event-B. For this purpose, we introduce a new state variable, dummyTick, which is modelled as an always incrementing counter and assigned to Millisec. Variable dummyTick is a dummy variable used to establish time related system properties in this model – for example, “ground velocity update is done at some time in the future”.

    Finally, updateTime records the last update time for esmt_velocity, while set variable updateRecords keeps track of all previous ground velocity estimation times.

figure f

3.3 Second Refinement: Introducing Interrupt Service Routine

ISR in the NG velocity system is responsible for updating rotation counter and records the service request time. As per the system description, NGRotations counter is a 16-bit counter. However, it is observed that NGRotations counter can be modelled as an always incrementing counter– taking into account possible diameters of an aircraft wheel, a 16-bit rotations counter is more than enough for the longest existing runway. To model the ISR functionality, we introduce

figure g

four state variables NG Rotations, NGClick Time, oldRotationCount and interruptRecords, as well as one new event serviceInterrupt.

figure h

As discussed earlier, NGRotations is modelled as always incrementing counter that records the number of complete rotations of a nose gear wheel. We increment it by one each time an interrupt is serviced (see event serviceInterrupt below). A new state variable, oldRotationCount, is used to record previous value of NGRotations after it is updated with a new value. Variable NGClickTime is confined automatically to modular semantics as it receives values from Millisec counter.

In the same spirit of collecting information about the system states, interruptRecords is used as a set for recording time for each invocation of ISR. With the help of this information we can prove that “NG Velocity system will start estimating ground velocity only after at least one interrupt is serviced”.

Invariants (3,4,5,6) establish new properties related to serving an interrupt introduced by a serviceInterrupt event. Finally, one more detail is revealed in this refinement – velocity estimations occur only after at least one interrupt has been serviced. This is achieved by strengthening guards of updateGroundVelocity: interruptRecords \(\ne \varnothing \).

3.4 Third Refinement: Introducing an Electro-Mechanical Sensor

The sensor is responsible for generating a click. We model it as a hardware interrupt generated after each complete rotation. click is represented by either 0 or 1, where 0 indicates that there is no hardware interrupt or a requested interrupt has been served, while 1 indicates that there is a new hardware interrupt and it needs to be served. To model this sensor we introduce events for monitoring rotation progress and detection of a complete rotation. Finally, this refinement also addresses that no false-positive click is generated and each complete rotation takes some time.

To model the sensor, we introduce three new variables click, rotationAngle, clickRecords and two new events – one for monitoring rotation progress of a wheel (monitorRotationProgress) and one for generation of a click on a complete rotation (detectRotationComplete). We do not list actions of these events here, but rather discuss them in order to give overall idea. The model invariants are presented below:

figure i

The context for this refinement step defines a new explicit type DEGREE to model rotation progress for the NG wheel. As before, we also define a mapping \(degree \in \mathbb {N} \rightarrowtail DEGREE\).

Event monitorRotationProgress can be considered as a first part for the required functionality of the sensor. Its action captures the progression of a rotation angle (rotationAngle). Event detectRotationComplete then constitutes the second part of the functionality. This event is triggered when a complete rotation is detected. State variable click is set to 1 to indicate that there is a new hardware interrupt generated by the sensor. The event monitorRotationProgress is a non-blocking event. That is, after reporting a new hardware interrupt, sensor continues its work of monitoring the next rotation. With these two events, we establish four new properties targeted for this refinement step – invariants 3,4,5,6,7,8. Variable clickRecords is used for keeping record of all interrupts generated since initialisation.

click establisesh the relationship between the electro-mechanical sensor and the ISR in the previous refinement step – once a hardware interrupt is generated (i.e., \(click := 1\)), ISR can immediately serve that interrupt – it updates the rotations counter and records that click time. Essentially we model the fact that some time progresses with each rotation of a wheel. Hence, in this refinement step we strengthen the guards of serviceInterrupt event so that it is enabled only when there is a new (unserviced) hardware interrupt.

3.5 Fourth Refinement: Modelling Basic Functionality of RTOS

A real time operating system (RTOS) invokes the update function at least once every 500 ms. The case study document [7] explicitly mentions that the exact invocation time relative to a hardware interrupt is not predictable. The only assurance we have here is that RTOS will invoke the function once every 500 ms. We also need to model the case that, once invoked, velocity estimation must complete within 500 ms.

figure j

We model the basic functionality of RTOS explained above and we introduce two new state variables – a variable updateInvoked that flags the invocation of update function, and variable invokeTime used to record the exact time at which update function has been invoked. The invocation of the update function is modelled by event invokeUpdate.

figure k

In this refinement step, we also add constraints on event MillisecTicks to establish following system properties – “ground velocity function is invoked at least once every 500 ms” and “once invoked, update should finish within 500 ms”.

These properties are totally time dependent, and since we have already introduced the notion of progressing time in our model, these properties are addressed in a straightforward manner at this step (invariants 4 and 5).

The condition (guard) for executing updateGroundVelocity is now changed – it can now be entered when there is an invocation by an RTOS: updateInvoked = TRUE. Earlier abstract models had information related to serviced interrupts only, so event could be entered when there is at least one interrupt is serviced, which is ultimately the effect of an invocation by RTOS.

3.6 Fifth Refinement: Modelling the Estimation Process

Now that we have introduced all functional components of the system, in this refinement we model how an update function estimates the ground velocity. This step addresses two specific cases – (1) the aircraft travels some distance in a given time interval and an update occurs; (2) zero distance is travelled in a given time interval and an update occurs.

Modelling the estimation process requires to take into account the computation of a travelled distance and an elapsed time before the actual estimation of the current velocity. There are six new variables introduced in this refinement step – elapsedTime, travldDist, lastRotations, lastClickTime, et_computed and td_computed – as well as three new events for modelling the estimation – update_zeroTravlDist, computeDistance and computeElapsedTime.

figure l

Context for this refinement introduces three new explicit types – INCH, MILE, HOUR. Constructing functions are also introduced for respective explicit types, such as inch, mile, hour. These are required for mapping between Event-B supported integer types and our explicit types. Moreover, we define three additional constants WHEEL_CIRC, cmpElpsdTime and mph_velo. The first one represents the circumference of the aircraft wheel (computed from given wheel diameter), the second one is the abstract function that computes the elapsed time, and the last one is the abstract function that converts estimated velocity form inches per millisecond into miles per hour.

figure m

A new event update_zeroTravlDist is enabled when there is no distance travelled (see guard \(travldDist = inch(0)\)) and an update process is initiated. With this event we model that even though there is no distance travelled, update is performed for a newly calculated elapsed time. The necessary condition to perform velocity update is that the computation of a travelled distance and an elapsed time must have been performed earlier. That is, new state variables et_computed and td_computed are set to TRUE.

Events computeDistance and computeElapsedTime are modelled as sort of ‘sub-states’. They are indeed part of the overall velocity estimation process. Once there is an invocation by RTOS, either of the two events can be executed. Once both these events have been executed, then, based on the value of travldDist, either event updateGroundVelocity or update_zeroTrvalDist is triggered.

figure n
figure o
figure p

Finally, a new variable lastClickTime is used for calculating total elapsed time between two consecutive invocations. Event computeElapsedTime updates the value of this variable for each invocation. This updated value is then used for calculating elapsed time for the subsequent invocation. A new state variable lastRotations is used in a similar manner but for the calculation of a travelled distance.

3.7 Sixth Refinement: Establishing EXFUN-1

We address the main requirement for the system – EXFUN-1: “Estimated ground velocity of the aircraft is available only if it is within 3 KPH of the true velocity at some moment in within past 3 s”. However, there is one more important requirement derived from the requirements description – “published velocity should be available all the time”. To address these two requirements, we have to consider three different cases here – (1) estimated ground velocity is published if EXFUN-1 is satisfied; (2) old ground velocity is published if the latest velocity is not yet available and the old velocity continues to satisfy EXFUN-1 (update is in progress); (3) zero velocity is published if EXFUN-1 is not satisfied.

The property EXFUN-1 adds time constraints on the system’s velocity estimation process. Also, this estimated velocity needs to be available all the time. To model these two requirements we have made distinction between the estimated velocity and the published velocity.

The state flow is such that after an invocation by RTOS (1) velocity estimation is performed (as discussed earlier); (2) once the velocity estimation process is complete, a new velocity is checked against constraints for EXFUN-1; (3.a) if these constraints are satisfied, we publish the new velocity; (3.b) if they are not satisfied, but an old velocity is still valid, we keep publishing the old velocity (3.c) if none of the constraints are satisfied, we publish the zero velocity. With this design we achieve the second requirement of having velocity published all the time.

There are three new variables introduced in this refinement step – published_ velocity, esmt_velo_avlbl and actual_velocity – and four new events modelling the state flow explained above – validateVelocity, publishZeroVelocity, publish Velocity and publishOldVelocity. Moreover, context for this refinement step introduces a new explicit type, KPH, in order to address EXFUN-1, which states its constraints in SI units system. Here, we also need to handle conversions between MPH to KPH. For these conversions we introduce a new constructed type, mphTokph.Footnote 2

figure q

Event validateVelocity is enabled only when a new estimated velocity is available, and all constraints related to EXFUN-1 are satisfied. A new state variable esmt_velo_avlbl is used to flag the availability of a new, valid, velocity for publishing. In this same event, a new state variable actual_velocity is assigned a value from a local parameter of the event, which represents true velocity of the aircraft at that instant. Once the esmt_velo_avlbl is set to TRUE, a new event publishVelocity can be executed to update the value of a new state variable published_Velocity. We use this variable to denote the published velocity by the NG velocity system.

As discussed earlier, we also model the case where a new velocity estimation is not available or invalid, but old velocity is still valid with respect to EXFUN-1. Event publishOldVelocity models this case. Finally, when new and old velocities are not valid any more with respect to EXFUN-1, we publish zero velocity. For this, we update published_velocity with \(0\,\mathrm{{KPH}}\) in a new event publishZeroVelocity. These four new events allows us to meet the functional requirement that the published velocity is always available.

figure r
figure s
figure t
figure u

We have addressed all requirements (both explicit and derived) that we could extract from the requirements document for the NG velocity system. Hence, we can conclude that the development of a formal model for the system (with an adopted refinement strategy) is complete at this stage.

4 Discussion and Lessons Learnt

We make use of explicit types to model units in NG velocity development. Making use of explicit types for numerical units is a design decision based on two observations – (1) model is easier to communicate with other stakeholders (individuals that interact with formal models in some way), as it becomes explicit regarding manipulations of types and their use; (2) from the modelling perspective, assigning types (rather than treating them subsets of \(\mathbb {N}\)) creates distinct entities which results in clearer proofs.

Our first goal was to develop a case study which would help us to study properties and scenarios we were looking for implicit and explicit semantics, and also to evaluate the suitability of Event-B and Rodin platform for that purpose. Even though the development was undertaken by people with significant background in formal verification, the initial modelling attempt was rather unsuccessful. Probably the main reason behind that was the fact that our first model involved too detailed representation of domain entities. Since the NG velocity system was a kind of test bed for investigating potentially good ways for incorporating explicit semantics into Event-B, the excessively detailed model soon become too cumbersome for its purpose. As a result, we made a decision that in the NG velocity model, we only abstractly define all the required entities, while their complete definitions should be left for the future work. Also, in order to validate our modelling decisions, the development was constantly accompanied by discussions with domain experts. On one hand, such discussions allowed us to reveal new, subtle yet important, properties that our model was lacking in, yet on the other hand, they resulted in multiple redevelopment of the model.

Based on this experience we argue that, even if formal models are less famed in software engineering community (one of the reasons may be of being less indirect in transition from specification to code, which is not a mature area yet), formal models could at least be used for extracting all requiredsy stem properties and requirements correctly and unambiguously, before proceeding to the software design phase. Software and/or hardware systems’ clients in this case should ask for proved formalisations of their requirements specification from prime contractors. Finally, we can say that refinement-based modelling method demonstrated a positive impact on requirement traceability and detection of missing and contradicting requirements.

Our second goal was to identify and separate domain descriptions, that is explicit semantics, mixed in the formal model of the NG velocity system. After realizing the process of specifying domain descriptions from domain engineering perspective [4, 5] (genericity, extendability, and reusability), it is clear how a classical formal modelling approach bundles everything together in the same model, with implicit semantics (i.e. semantics of the underlying theory used for modelling). A task similar to reverse engineering was performed to extract probable domain descriptions from the NG velocity system Event-B model. As a results, we were able to separate two distinct vocabularies from this model. First vocabulary, describing units and their conversions, is more abstract and relevant to upper ontology model. That is, the same vocabulary can be used by many other domain specific vocabularies, such as science and engineering domains. Second vocabulary is specific to aeronautics domain, which essentially sits lower in hierarchy to the first one. Future work in this direction is discussed in detail in the next section.

Our third goal was twofold. We call it separation and integration. By separation we mean that one should be able to model explicit semantics separately as the first class objects. By integration we mean that one should be able to integrate and (re)use explicit semantics within formal models. Unfortunately, despite all the strengths of Rodin platform, out of the box it does not provide modelling support sufficient for achieving this goal. Theory feature is an external plugin available for Rodin platform and which enables to create reusable components [6]. However, our experiments with the theory plugin have shown that, at the current state, it is also not capable of dealing with the separation aspect. In particular, there is no appropriate way to define inheritance.

Hence, our solution is to employ ontologies as formal concept models suitable to tackle the separation problem. After a comparative survey, PLIB ontology model was chosen because of its formal, yet executable representation of concepts, and context-explication mechanisms [9]. Our experiment with PLIB model suggests that it potentially satisfies all criteria for handling the separation aspect of the problem.

5 Conclusion and Future Work

We have made a first important step towards the separation and seamless integration of explicit semantic features into the formal development in Event-B. To explicitly define domain knowledge, we abstractly specified all the required entities (data types) and relationships between them in model’s contexts. However, as per the main properties of domain descriptions, these descriptions should be generic, extendable, and reusable. Therefore, the next important step is to develop an independent Event-B component – ontology/domain description library – that will contain formal definitions of data types and functions for all (not only fundamental) units of physical quantities related to the NG velocity development (i.e., velocity, distance and time) in two most widely used systems of measurement (i.e., metric and imperial). Unlike the definitions presented in contexts of the NG velocity development, these new definitions will be fully axiomatised using standard physical metrics, which will allow us to guarantee that each definition in the library is sound and complete. Also, to make our definitions more flexible/usable we aim at redefining some of them as instances of the real numbers and to see whether pre-existing upper ontologies can be re-used for our purpose.

We plan to use PLIB ontology model approach both to create the ontology library and to properly define the set of real numbers. Future research directions would be towards automated and seamless integration of PLIB concept model instances and/or schema into Event-B models. This work involves many criteria to consider, such as automated inferences to discover new logical relationships among modelled entities. This will require changes/extensions to Rodin platform side in order to cope-up with automated integration and support reasoning on explicitly modelled relations in proof obligations. Clearly, once we create, verify and validate the library for time, distance and velocity, it is important to elaborate on this work and extend the library with other physical quantities (e.g., weight, mass, temperature, energy). Future plan also includes more case studies including heterogeneous systems targeting various domains.