A contract-based method to specify stimulus-response requirements

TL;DR

This paper introduces a novel method for specifying and verifying stimulus-response requirements by translating declarative specifications into imperative programs and using program provers for validation, demonstrated on an aircraft landing gear system model.

Contribution

It presents a new approach to specify and verify stimulus-response requirements through imperative routines and formal verification, bridging the gap between declarative specifications and executable programs.

Findings

Successfully applied to an ASM model of the Landing Gear System

Enables direct verification of requirements against imperative programs

Provides a practical framework for formal specification and validation

Abstract

A number of formal methods exist for capturing stimulus-response requirements in a declarative form. Someone yet needs to translate the resulting declarative statements into imperative programs. The present article describes a method for specification and verification of stimulus-response requirements in the form of imperative program routines with conditionals and assertions. A program prover then checks a candidate program directly against the stated requirements. The article illustrates the approach by applying it to an ASM model of the Landing Gear System, a widely used realistic example proposed for evaluating specification and verification techniques.

Figures

Equations

$$stimulus\iff$$

$$thehandleisDOWN"$$

$$response\iff (stimulus⟹$$

$$thedoorsareclosed")$$

$$f(t_1,..,t_j):=t_0$$

$$R_1||...||R_k$$

$$a,b:=max(a-b,b),min(a-b,b)$$

Full text

I Overview and Main Results

The present article describes a technique for specification and verification of stimulus-response requirements using a general-purpose programming language (Eiffel) and a program prover (AutoProof [1]) based on the principles of Design by Contract [2].

Real-time, or reactive, systems are often run by a software controller that repeatedly executes one and the same routine and it is specified to take actions at specific time intervals or according to external stimuli [3]. This architecture is reasonable when the software has to react timely to non-deterministic changes in the environment. In this case the program should react to the external stimuli in small steps, so that in the event of a new change it responds timely.

Computation tree logics (CTL) [4] represent a frequent choice when it comes to capturing stimulus-response requirements. Although it may be easier to reason about requirements using declarative logic like CTL, the reasoning may be of little value for the software developer who will implement the requirements. Mainstream programming languages are all imperative, and the translation between declarative requirements and imperative programs is semi-formal.

Requirements have to be of imperative nature from the beginning. This would bridge the gap in how customers and developers understand them. For a software developer it is preferable to reason about the future program without switching to an additional formalism, notation and tools not connected to the original programming language and the IDE. The present article describes a technique to achieve this goal, in particular:

• •

Introduces the Landing Gear System (LGS) case study and the LGS baseline requirements (Section II).

• •

Generalizes the LGS baseline requirements, maps them to a well-established taxonomy, and complements the taxonomy (Section III).

• •

Provides a general scheme for capturing semantics of the stimulus-response requirements in the form of imperative program routines with assertions (Section IV).

• •

Exercises utility of the approach by applying it to an Abstract State Machine (ASM) specification of the Landing Gear System case study (Section V).

• •

Concludes the possibility of statically checking a sequential imperative program directly against a stimulus-response requirement whose semantics is expressed in the same programming language through conditionals, loops, and assertions (Section VII).

Application of the technique leads to discovery of an error in the published model of the LGS ASM [5]. The error is not present in the specification the authors have actually used for proving the properties, but the error has found its way into the publication.

II The Landing Gear System

Landing Gear System was proposed as a benchmark for techniques and tools dedicated to the verification of behavioral properties of systems [6]. It physically consists of the landing set, a gear box that stores the gear in the retracted position, and a door attached to the box (Figure 1). The door and the gear are actuated independently by a digital controller. The controller reacts to changes in position of a handle in the cockpit by initiating either gear extension or retraction process. The task is to program the controller so that it correctly aligns in time the events of changing the handle’s position and sending commands to the door and the gear actuators.

III Stimulus-Response requirements

The LGS case study defines a number of requirements, including several for the normal mode of operation (Figure 2). The requirements communicate a common meaning of the form:

• •

If stimulus holds, then response will eventually hold in the future.

For requirement $R_{11}bis$,

[TABLE]

and

[TABLE]

The implication in the definition of $response$ reflects the “and stays DOWN” part of the original requirement.

In addition to that, requirements $R_{21}$ and $R_{22}$ communicate something else:

• •

Once response holds in the presence of stimulus, and stimulus holds forever, response will hold forever.

III-A Temporal interpretation of the requirements

The authors of the LGS ASM specification start with a ground model that satisfies a subset of requirements, and then refine the model to satisfy more requirements. The present article focuses on their ground model and the corresponding baseline requirements it covers (Figure 2). The work expresses the baseline requirements as CTL properties. The CTL interpretation assigns precise meanings to the requirements by assuming small-step execution semantics of ASM’s. In particular, for requirements $R_{11}bis$ and $R_{12}bis$ “the future” means “after a finite number of execution steps”, while for $R_{21}$ and $R_{22}$ “the future” means “after one execution step”.

The finite number of steps in $R_{11}bis$ and $R_{12}bis$ may be unacceptably large though for a system like an LGS of an aircraft. In particular, flights have some expected durations, and the gears have to react to commands in some limited time frame as well. The following two major categories of stimulus-response requirements stem from the speculations above:

• •

*If stimulus holds, then response will hold in not more than k execution steps.

*Requirements of this form are also called maximal distance requirements [7].

• •

*If stimulus holds, then response will hold in exactly k execution steps.

*Requirements of this form are also called exact distance, or delay requirements.

These two categories are not enough though for capturing stimulus-response requirements. For example, if according to $R_{11}bis$ the gears are locked down and the doors seen closed as the result of the handle staying down, we want this state to be stable if the handle stays down. This leads us to stimulus-response requirements of the following form:

• •

*If response holds under stimulus, it will still hold after one execution step in the presence of that stimulus.

*Let us call such requirements response stability requirements.

It makes sense to complement requirements $(R_{11}bis)$ and $(R_{12}bis)$ with the corresponding response stability requirements (Figure 3): not only do we want the LGS to respond to a change in the handle’s position, but we also want it to maintain the response if the position does not change.

IV Translation of Stimulus-Response Requirements

Assuming the presence of an infinite loop from until False loop main end that runs a reactive system, a temporal stimulus-response requirement (Section III-A) takes the form of a routine with an assertion (check end construct in Eiffel). The authors draw this idea from the notion of a specification driver [8] - a contracted routine that forms a proof obligation in Hoare logic. AutoProof is a prover of Eiffel programs that makes it possible to statically check the assertions.

IV-A Maximal distance

In the representation of a maximal distance requirement (Figure 4) the “if stimulus then” clause captures the presence of the stimulus before the up-to-$k$-length execution fragment, and the “check response end” assertion expresses the need for the response upon completion of the sub-execution. The sub-execution may complete for two possible reasons: either occurrence of the response or consumption of all of the available $k$ steps. In the both cases the response has to hold.

IV-B Exact distance

Representation of an exact distance requirement (Figure 5) is very similar to that one of a maximal distance, with the “check (response and (steps $=\,$ k)) end” assertion that makes the difference. Regardless of whether the loop terminates because of response or steps$=\,$k, the both have to hold upon the termination.

IV-C Response stability

Representation of a response stability requirement (Figure 6) says: whenever response holds under stimulus in a state, it will still hold in the presence of the same stimulus in the next state.

V Applying the Translation Scheme to the Landing Gear Example

The article exercises the approach on the LGS ASM specification, which is operational by the definition and thus is a subject for translation into an imperative program. For this reason the present section starts with explanation of the rules according to which the authors converted the original specification into an Eiffel program.

V-A Translation of ASM specifications

An ASM specification is a collection of rules taking one of the following three forms [9]: assignment (Section V-A1), do-in-parallel (Section V-A2), and conditional (Section V-A3). If we have general rules for translating these operators into Eiffel then we will be able to translate an arbitrary ASM into an Eiffel program.

V-A1 Assignment

An ASM assignment looks as follows:

[TABLE]

The semantics is: update the current content of location $\lambda=(f,(a_{1},..,a_{j}))$, where $a_{i}$ are values referenced by $t_{i}$, with the value referenced by $t_{0}$.

In Eiffel locations are represented with class attributes, so an ASM’s location update corresponds in Eiffel to an attribute assignment.

V-A2 Do-in-parallel

An ASM can apply several rules simultaneously in one step:

[TABLE]

In order to emulate a parallel assignment in a synchronous setting, one needs to assign first to fresh variables and then assign their values to the original ones. For example, an ASM do-in-parallel statement

[TABLE]

in Eiffel would look like

⬇

local

a_intermediate, b_intermediate: INTEGER

do

a_intermediate :$=\,$ max (a-b, b)

b_intermediate :$=\,$ min (a-b, b)

a :$=\,$ a_intermediate

b :$=\,$ b_intermediate

end

An attempt to update in parallel identical locations in an ASM corresponds semantically to a crash. The translation scheme not only preserves but strengthens this semantics: an Eiffel program with two local variables declared with identical names will not compile.

V-A3 Conditional

An ASM conditional if $t$ then $R_{1}$ else $R_{2}$ carries the same meaning as in Eiffel, so the translation is straightforward.

V-B Ground model

Translation of the original LGS ASM specification into Eiffel is publicly available in a GitHub repository [10] and needs clarification too.

The baseline LGS requirements (Figure 2) talk about normal mode of operation. The ground ASM specification captures the normal mode through a model invariant, while the Eiffel translation introduces a special boolean query is_normal_mode for this purpose. The reason for that is rather technical and has to do with the current limitations in the underlying verification technology. The translation also contains a number of annotations for disabling the complications of the underlying verification methodology [11]. Special comments highlight the annotations and tell explicitly that they have nothing to do with the problem at hand.

The repository contains two versions of the ground model, GROUND_MODEL_ORIGINAL and GROUND_MODEL. The original one keeps the error from the ASM model, which is not handling opening doors case in the extension sequence. The second version contains the translation without the error.

V-C Requirements

The two classes include the translations of the baseline requirements plus the response stability requirements introduced in the present article. We do not discuss all of them here: requirements $(R_{11}bis)$ and $(R_{12}bis)$, $(R_{21})$ and $(R_{22})$, $(R_{11}rs)$ and $(R_{12}rs)$ are pairwise similar, which is why we prefer to pick one from each pair.

Translation of requirement r11_bis (Figure 7) is an application of the response_holds_within_k_steps pattern (Figure 4), where:

• •

stimulus equates to:

⬇

is_normal_mode and

(handle_status$=\,$is_handle_down)

• •

response equates to:

⬇

(not (is_normal_mode and

(handle_status$=\,$is_handle_down))) or

((gear_status$=\,$is_gear_extended) and

(door_status$=\,$is_door_closed))

The idea behind the response is that there may be two reasons for the gear not to extend and the door not to close:

• •

An abnormal situation that leads to quitting the normal mode.

• •

The crew changes their mind and pushes the handle up.

VI Related work

Modeling of real-time computation and related requirements is a well-investigated matter [12]. Representation of real-time requirements, expressed in general or specific form, is a challenging task that has been attacked by the use of several formalisms both in sequential and concurrent settings, and in a broad set of application domains. The difficulty (or impossibility) to fully represents general real-time requirements other than in natural language, or making use of excessively complicated formalisms (unsuitable for software developers), has been recognized.

In [13] the domain of real-time reconfiguration of system is discussed, emphasizing the necessity of adequate formalisms. The problem of modeling real time in the context of services orchestration in Business Process, and in presence of abnormal behavior has been examined in [14] and [15] by means, respectively, of process algebra and temporal logic. Modeling of protocols also requires real-time aspects to be represented [16]. Event-B has also been used as a vector for real-time extension [17] in order to handle embedded systems requirements.

In all these studies, the necessity emerged of focusing on specific typology of requirements using ad-hoc formalisms and techniques, and making use of abstractions. The notion of “real-time” is often abstracted as number of steps, a metric commonly used. In this paper we follow the same approach, inheriting both strength (simplicity of the model and effectiveness for applicative purposes) and limitations (temporal logic and time automata themselves miss to capture a precise notion of real-time).

VII Conclusions and future work

Software developers reason in an imperative/operational manner. This claim is supported both by anecdotal experience and by empirical evidence [18]. Requirements expressed in imperative/operational fashion would therefore results of easier comprehensions for developers and would simplify the process of negotiation behind requirements elicitation.

In the method described in this paper, requirements are expressed in a formalism (or language) that seamlessly stay the same along the whole process, without the need of switching between different instruments or mental paradigms. At the same time, the linguistic tool used to define them also allows for automatic verification of correctness.

The meaning of correctness here remains subject to the assumption that requirements engineers and stakeholders agree on a list of desiderata that is indeed the intended one. Assuming a non-faulty process of intention transferring (and this assumption is common to any other approach too), requirements are now more easily manageable by software engineerings all the way from elicitation to verification.

The result of elicitation process is a set of requirements in natural language. The full realization of the presented method would imply an automatic (or semi-automatic) translation from natural language into a structured representation that, although completely intuitive for software developers, it is possibly not easy to manage for average stakeholders. The first part of this process, i.e., the translation from natural language into the current representation (and back) is under development. A tool automatically translates semi-structured natural language into the Hoare-triple-based representation [19], allowing also the opposite direction, i.e. back to natural language [20], so that software engineers would be able to negotiate back requirements with stakeholders using a format they would comprehend. The role of the requirement engineers would then consist in concluding the elicitation phase with a set of requirements in semi-structured natural language, which the tool would be able to process in an entirely automatic manner.

This paper supports the idea of seamless development describing a method supported by a formalism that stay the same along the whole process, from requirements to deployment. Alternative approaches have also been experimented which make use of formalism-based toolkits, where ad hoc notations are adopted for each development phase [21].