Lesson 3: Accommodating Hardware Changes

Let’s suppose that a hardware change is made to the valve hardware interface requiring a one-time setup of valve parameters, such as hardware port number, before the valve can be moved. Furthermore, let’s assume that the ValveHALBase component will check the parameters and reject them if they are invalid. This introduces a new requirement:

R7:No valve movement is allowed unless and until a correct set of valve parameters has been accepted. Furthermore, once a set of parameters has been accepted, it is not permitted to change them.

In this lesson, we will adapt our software to implement the new requirement R7.

We decide that the valve parameters must be supplied to the ValveHALBase by its client, ValveControllerImpl, as a parameter to its setup(…) function and passed on to the ValveHALBase in order to satisfy R7. In order to satisfy the requirements R4 and R5, the ValveController has to be able to work with different types of valves, and must not be dependent on specifics such as the details of the parameters; we just want ValveController to be a conduit, passing the parameters as an undefined block of data.

Following the Coco workflow, we will implement requirements R4, R5 and R7 by:

  1. Extending the ValveHAL port to require the valve parameters.
  2. Modifying the SimulatorImpl component to implement the changes made to ValveHAL.
  3. Extending the ValveController port to accept valve parameters.
  4. Verifying all the ports and components to identify the changes necessary to the ValveControllerImpl component so that it uses its required ports correctly, and implements its provided port.
  5. Fixing the ValveControllerImpl component according to the verification results.

We will be introducing the following new language features in this lesson:

Step 1: Extending ValveHAL

We start by extending ValveHAL port to implement these requirements as follows:

  1. Declare a new external type for the valve parameter data.
  2. Declare a new function to set the valve parameters.
  3. Extend the state machine so that the parameters are set before the call to move the valve is allowed.
  4. Indicate whether the parameters are valid or not.

Declaring an External Type for the Valve Parameters

The format and semantics of the valve parameters do not need to be known by the clients of the ValveHALBase component, namely the ValveControllerImpl. The ValveControllerImpl is simply acting as a conduit that feeds the data as an opaque block from its clients through to the ValveHALBase. In Coco, such data are declared as an external type in the provided port ValveHAL of ValveHALBase.

Note

An external type declaration allows users to refer to a type that is not defined within their Coco program, but is defined somewhere else in the code. External types help integration of the generated code into the rest of the system.

The body of an external type is only used during the verification (same as for external functions), but no code is generated from it. A user-defined external type is not verifiable, and not defaultable. Users can specify that a custom external type is defaultable by declaring an instance of Default for it. A variable can be declared to be of some external type T, and if there is no instance of Default for T, then the variable declaration must either be given an explicit initialisation, or it must be declared to be of type Slot of type T instead. For further details, see external type. We will also explore the use of slots in Lesson 9: Introducing Slots.

Add the following external type declaration:

external type ValveParameters

Adding a New Function

Declare a new function interface in ValveHAL for setting the parameters as follows:

  function setParameters(setup : ValveParameters) : Bool

This function takes an instance of ValveParameters, and returns true if they are valid, and false otherwise.

Extending the State Machine

The ValveHALBase software is a simple piece of handwritten code necessary to make the hardware/software interface directly callable by the code generated from a Coco component. It is important that it is simple because there is no automated method of ensuring that handwritten code implements its Coco port specification; this has to be checked by manual review. To simplify this process, it is good practice to ensure that the structure of the Coco port is aligned as closely as possible to that of the handwritten code.

Therefore, instead of changing the current port state machine into one with several user-defined states, the new behaviour will be added to Main using a boolean variable to keep track of whether parameters have been specified or not, and to guard the new event transitions. This should ensure that the Coco port will closely align to the handwritten ValveHALBase code.

The new requirement is that a valve movement is only allowed after a correct set of valve parameters has been accepted by ValveHALBase. Furthermore, once a set of parameters has been accepted, it is not allowed to change them.

Declare a new boolean variable in the state machine as follows:

    var isValidSetup : Bool

By default, boolean variables are initialised to false.

Add the following event transition for the newly declared function setParameters(…) in Main:

    if (!isValidSetup) setParameters(_) = isValidSetup = nondet {
      true,
      false,
    }

This transition is guarded, and is therefore only enabled when the value of isValidSetup is false. The function is called with _ as its argument, which is the wildcard pattern, and means that it matches any value. The value passed as an argument to this function cannot be referenced in the port state machine. This is required because the parameter is an unverifiable type.

The body of the event handler for this transition is a block expression with the following effect:

  1. The nondet expression is evaluated to true or false, the choice being made nondeterministically;
  2. The resulting value is assigned to the Boolean variable isValidSetup;
  3. The value assigned, namely the value of the assignment expression, is returned as the value of the setParameters(…) function call.

Note

This port specifies that the parameters passed to the setParameters(…) function can be accepted or rejected nondeterministically. This does not mean that the component implementing it must reject the parameters; it simply states that it is allowed to do so. However, it does mean that any client using this port must be able to handle both cases.

Modelling nondeterminism in port state machines highlights a fundamental difference between ports and components. Ports abstract away the implementation details of how functions are implemented, and simply specify a partial view of the visible behaviour of a component on a specific boundary. In contrast, a component state machine is not allowed to be nondeterministic, as it has to specify the complete implementation of the component from which code can be generated. In this example, the component would have to specify the logic necessary to determine whether the parameters are valid or not.

Finally, we must amend the event transition for the function move(…) by adding the following guard:

    if (isValidSetup) move(_) = {}

This transition is now only enabled when isValidSetup evaluates to true.

After making these changes, your ValveHAL port should look like the following:

external type ValveParameters

port ValveHAL {
  enum Moves {
    case Open
    case Close
  }

  function setParameters(setup : ValveParameters) : Bool
  function move(target : Moves) : Nil

  machine {
    var isValidSetup : Bool

    // Accept or reject valve parameters and remember result
    if (!isValidSetup) setParameters(_) = isValidSetup = nondet {
      true,
      false,
    }
    // Move valve if parameters are valid
    if (isValidSetup) move(_) = {}
  }
}

The complete Coco for this port can be found in Example_03B/src/ValveHAL.coco.

Step 2: Extending SimulatorImpl

We have just added a new function, setParameters(…) to ValveHAL and before going further, we should implement this in SimulatorImpl as it has to implement ValveHAL as its provided port. To do this, we will modify its state machine by adding a transition to implement the setParameters(…) function as follows:

  machine {
    client.setParameters(_) = true
    client.move(_) = sleep(seconds(10))
  }

The SimulatorImpl assumes the parameters are always valid.

The complete Coco for this component is in Example_03B/src/SimulatorImpl.coco.

Verifying your Changes (Example_03B)

Run the verification on the modified Coco files in this example. Popili finds errors in both the SimulatorImpl and the ValveControllerImpl. Let’s start by analysing the error found in the SimulatorImpl component.

The SimulatorImpl is failing to implement its provided port with the following counterexample:

client client User User SimulatorImpl SimulatorImpl move(Moves.Open) move(Moves.Open) move(Moves.Open) move(Moves.Open) return nil return nil Main Main Main Main Main The provided port expected the last function call to be illegal. Trace counterexample

Analysis

The SimulatorImpl component fails to implement its provided port correctly, because it allows move(…) to be called before setParameters(…) has been called with valid parameters, which is not allowed by ValveHAL. In the counterexample above, the move(…) function can be called as the first interaction with the SimulatorImpl.

Modifying the SimulatorImpl

Inspecting the ValveHAL port we can see the following:

  1. When setParameters(…) has been called and returns true, it cannot be called again.
  2. The move(…) function can only be called after a successful call to setParameters(…).

To make SimulatorImpl comply with these requirements, we need to modify it to remember when a successful call has been made to the setParameters(…) function. Before this has occurred, the move(…) function must not be allowed. After this has occurred, the move(…) function must be allowed, but all further calls on setParameters(…) must be forbidden.

To achieve this, we are going to use transition guards. Modify the SimulatorImpl state machine as follows:

  machine {
    var isSetup : Bool
    if (!isSetup) client.setParameters(_) = isSetup = true
    if (isSetup) client.move(_) = sleep(seconds(10))
  }

The following line declares a variable called isSetup of type Bool, which is initialised to false by default:

    var isSetup : Bool

The following line defines a guarded transition for the setParameters(…) function; it is only enabled if isSetup is false; its handler always returns true, and sets isSetup to true:

    if (!isSetup) client.setParameters(_) = isSetup = true

The following line defines a guarded transition for the move(…) function so that the transition is only enabled when isSetup is true:

    if (isSetup) client.move(_) = sleep(seconds(10))

The complete Coco for this component is in Example_03C/src/SimulatorImpl.coco.

Verifying your Changes (Example_03C)

After modifying SimulatorImpl, re-run the verification. All of the assertions for your SimulatorImpl component should now pass.

However, Popili finds an error in one of the assertions for the ValveControllerImpl component. ValveHAL is also a required port of the ValveControllerImpl component, and with the changes we made to it above, the ValveControllerImpl no longer uses this required port correctly. Popili gives the following counterexample:

User User ValveControllerImpl ValveControllerImpl hal hal setup() setup() return nil return nil close() close() move(Moves.Close) move(Moves.Close) Initial Main Unknown Unknown Closed The last function call was illegal; it could not be handled by hal because no transition matched. Illegal function call counterexample

Analysis

The assertion fails because the ValveControllerImpl component has not yet been modified to handle the changes made to its required port hal (which is an instance of the port ValveHAL). In particular, the counterexample shows how the ValveControllerImpl can call the function move(…) on its required port hal before the setParameters(…) function has been called with valid parameters, which is not allowed by ValveHAL.

In order to implement its provided port, the ValveControllerImpl component needs to obtain the valve parameters it must supply on to ValveHALBase. We decide that the ValveControllerImpl client will supply these as a parameter to the setup(…) call.

We will take the following steps to implement these changes:

  1. Extend the ValveControllerImpl interface by extending its provided port, ValveController.
  2. Extend the ValveControllerImpl component to adopt the changed interface, and call setParameters(…) on the ValveHAL port.

Step 3: Extending ValveController

The modified ValveHAL port above requires parameters to be set before the first valve movement is allowed. These will be supplied by the client of the ValveControllerImpl component as part of the initialisation process. This requires extending the ValveControllerImpl interface, which we achieve by making the following changes to its provided port ValveController:

  1. Import the ValveHAL module to bring the declaration of ValveParameters into scope.
  2. Extend the setup(…) function interface declaration so that it has an input parameter, and returns a Bool.
  3. Modify the state machine so that the setup(…) transition’s handler returns true if the parameters are valid, and false, otherwise.

Importing ValveHAL Module Declarations

Add the following line to bring the declaration of ValveParameters into scope:

import unqualified ValveHAL

Extending the setup(…) Function with Parameters

Amend the setup(…) function interface declaration so that it has an input parameter, and returns a boolean, which reflects whether the parameters are valid or not:

  function setup(settings : ValveParameters) : Bool

Modifying the state machine

Modify the state machine to reflect the changes made to the initialisation process. Specifically, in state Initial, the transition specified for the function setup(_) needs to reflect the possibility that the parameters might be rejected. The reasons for rejection are unknown by the port, not least because ValveParameters is an external data type, and therefore opaque to Coco. However, the port can reflect this behaviour by modelling it as nondeterministic choice between the parameters being accepted as valid or rejected as invalid.

Modify the transition as follows:

      setup(_) = nondet {
        InvalidParameters:
        {
          return false;
        },
        ValidParameters:
        {
          setNextState(Operational);
          return true;
        },
      }

The body of the event handler is now a nondet expression with two clauses. The first clause returns false and remains in the same state, indicating invalid parameters; and the second one returns true, and transitions to the state Operational, indicating valid parameters.

Note

As highlighted in Lesson 2: Adding Query Functions, the syntax above is equivalent to the following form with implicit returns, where the nondet clauses evaluate to false and true respectively:

      setup(_) = nondet {
        InvalidParameters: false,
        ValidParameters:
        {
          setNextState(Operational);
          true
        },
      }

Each nondet clause is labelled with a @represents attribute, which annotates these actions in any verification counterexamples that are generated.

The resulting ValveController port is as follows:

import unqualified ValveHAL

port ValveController {
  function setup(settings : ValveParameters) : Bool
  function open() : Nil
  function close() : Nil
  function isOpen() : Bool
  function isClosed() : Bool

  machine {
    enum Position {
      case Opened
      case Closed
      case Unknown
    }

    var position : Position = .Unknown

    isOpen() = position == .Opened
    isClosed() = position == .Closed

    state Initial {
      setup(_) = nondet {
        InvalidParameters:
        {
          return false;
        },
        ValidParameters:
        {
          setNextState(Operational);
          return true;
        },
      }
    }

    state Operational {
      open() = {
        position = .Opened;
      }
      close() = {
        position = .Closed;
      }
    }
  }
}

The complete Coco for this port is in Example_04A/src/ValveController.coco.

Step 4: Extending ValveControllerImpl

Popili will highlight the fact that ValveControllerImpl component is no longer well-formed, because the setup(…) function signature in the ValveController port differs from how it is used in ValveControllerImpl.

The ValveControllerImpl component needs to be modified to work correctly with the changes that we have made to its provided and required ports.

We will start by editing ValveControllerImpl to make it well-formed again, and then re-verify it to determine what modifications are needed. Check your changes by re-verifying the component as you make them.

Your new ValveControllerImpl component should look like the following:

import unqualified ValveController
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveControllerImpl {
  val client : Provided<ValveController>
  val hal : Required<ValveHAL>

  machine {
    client.isOpen() = false
    client.isClosed() = false

    state Initial {
      client.setup(settings : ValveParameters) = if (hal.setParameters(settings)) {
        setNextState(Unknown);
        return true;
      } else {
        return false;
      }
    }

    // Valve position unknown until the first move request is received
    state Unknown {
      client.open() = setNextState(Opened)
      client.close() = setNextState(Closed)
    }

    state Opened {
      entry() = hal.move(.Open)
      client.isOpen() = true
      client.open() = {}
      client.close() = setNextState(Closed)
    }

    state Closed {
      entry() = hal.move(.Close)
      client.isClosed() = true
      client.open() = setNextState(Opened)
      client.close() = {}
    }
  }
}

The complete Coco for this component is in Example_04A/src/ValveControllerImpl.coco.

Verifying your Changes (Example_04A)

All of the updated ports and components verify successfully.