Lesson 6: Armouring the Valve Controller

Let’s consider the port ValveDriver, which defines the interface contract between two Coco components, namely ValveControllerImpl and ValveDriverImpl. Since both of these components are written in Coco, the verification checks whether ValveDriverImpl correctly implements ValveDriver as its provided port, and whether ValveControllerImpl uses ValveDriver correctly as its required port. If ValveControllerImpl does use ValveDriver correctly, then we say that ValveControllerImpl is a well-behaved client of that port (and by definition, of any implementation thereof), since it only makes calls on ValveDriver that are allowed, can handle any return values received, and can handle every signal sent by ValveDriver.

When a Coco component is used by a non-Coco client, the verification assumes that the non-Coco client is a well-behaved client of the Coco component’s provided port. However, this does not always reflect reality when interfacing with native code that has not been developed in Coco and verified. Although the native code can be tested with the code generated from Coco, this does not guarantee that the client will always behave correctly with the Coco component it uses.

To address this problem, we are going to use a technique called armouring, where we insert a new Coco component between the non-Coco client, and the Coco component that it is using. The purpose of this new component, called ArmourImpl, is to implement a robust version of ValveController, which will not allow any client misbehaviour to reach ValveControllerImpl. Since ArmourImpl is written in Coco, the verification will check that there is no execution scenario that will violate ValveController.

We will proceed as follows:

  1. Declare a port called Armour where every function is legal in every state, and returns a boolean value indicating whether the function can be called on ValveControllerImpl (i.e. it is legal according to its provided port ValveController), or is rejected because it is illegal to call it on ValveControllerImpl.
  2. Implement a new component called ArmourImpl, which implements Armour and will sit in between the Application external component and the ValveGroup. Its purpose is to intercept all calls made by Application on ValveGroup, and only forward those that are allowed according ValveController (which is the provided port of ValveControllerImpl). An armour component should not change the functionality of the component it is protecting; it’s only purpose is to prevent illegal function calls from reaching the protected component.
  3. Implement a new encapsulating component called ArmouredValveGroup, which will declare an instance of ArmourImpl and ValveGroup, and connect them together.

Step 1: Specifying the Armour port

Create a new port Armour.coco by copying the ValveController port and change the port declaration to name the port Armour. Analyse the new Armour port and identify those functions that are always permitted versus those that are sometimes not allowed. Examining the port, we can see that:

  1. isOpen() and isClosed() are allowed in every state, and can always be passed through.
  2. open() and close() are only allowed in Ready, and must be rejected in all other states.
  3. setup(…) is only allowed in Initial, and must be rejected in all other states.

We need to modify the signatures for those functions that can be rejected, namely open() and close() to return a boolean as follows:

  function open() : Bool
  function close() : Bool

The other signatures are unchanged.

We need to add top-level transitions for the function calls that are only allowed in certain states to reject the calls by default. These declarations form part of the Main state as follows:

    var position : ValveDriver.Status = .Unknown
    isOpen() = position == .Opened
    isClosed() = position == .Closed

    open() = false
    close() = false
    setup(_) = false

Finally, add return true; as the final statements to be executed when open() and close() are called in the Ready state.

Your modified state machine should look like the following:

  machine {
    var position : ValveDriver.Status = .Unknown
    isOpen() = position == .Opened
    isClosed() = position == .Closed

    open() = false
    close() = false
    setup(_) = false

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

    state Ready {
      open() = {
        nondet {
          {
            position = .Opened;
            moveEnded(position);
          },
          {
            setNextState(Moving(.Opened))
          },
        }
        return true;
      }
      close() = {
        nondet {
          {
            position = .Closed;
            moveEnded(position);
          },
          {
            setNextState(Moving(.Closed))
          },
        }
        return true;
      }
    }

    state Moving(target : ValveDriver.Status) {
      entry() = {
        position = .Unknown;
      }

      spontaneous = {
        position = nondet {
          target,
          .Unknown,
          .Error,
        };
        setNextState(Ready);
      }

      exit() = {
        moveEnded(position);
      }
    }
  }

The complete Coco for this port is in Example_06B/src/Armour.coco.

Step 2: Building the ArmourImpl Component

We now need to build the ArmourImpl component, which implements the Armour port, and requires the ValveController port. This component should return true on every allowed function call, and false otherwise.

As is common with armour components, the component state machine is very similar to the state machine in its provided port. This means that we can take the following steps as a shortcut to implement the ArmourImpl component:

  • Create a new module called ArmourImpl.coco, and declare a component called ArmourImpl.
  • Copy the state machine from the Amour port, and paste it into the ArmourImpl component declaration.
  • Modify the ArmourImpl component state machine to convert it into a proper implementation of its provided port, and add the necessary calls to its required port.
  • Verify your work after each step, and fix any verification errors that arise.

Declaring a skeleton component

Create a new module called ArmourImpl.coco. Details on how to create Coco modules can be found in Lesson 1.

The next step is to add the following lines to create a skeleton ArmourImpl component without a state machine:

import unqualified Armour
import unqualified ValveController
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ArmourImpl {
  val client : Provided<Armour>
  val valve : Required<ValveController>
}

Building the ArmourImpl State Machine

To get started, reuse the state machine from Armour by copying and pasting it into the ArmourImpl component. This will give a number static errors as expected. To convert the copied port state machine into a proper component state machine, follow these steps:

  • Delete the declaration of the variable position. This is not needed in the component state machine, because the valve state will be obtained directly from the ValveControllerImpl component (via ValveController).

  • Add the provided port name, client, as a prefix to all of the incoming function events. For example, isOpen() becomes client.isOpen().

  • Modify the transitions for the client.isOpen(), client.isClosed(), client.open(), client.close(), and setup(…) functions as follows:

        client.isOpen() = valve.isOpen()
    client.isClosed() = valve.isClosed()
    client.open() = false
    client.close() = false
    client.setup(_) = false

  • Modify the client.setup(…) transition in state Initial as follows:

          client.setup(settings : ValveParameters) = {
        val result : Bool = valve.setup(settings);
        if (result) setNextState(Ready);
        return result;
      }

    The variable result is declared as a constant, because it is not modified once it has been initialised.

  • Modify the transitions in the Ready state as follows:

        state Ready {
      client.open() = {
        valve.open();
        setNextState(Moving);
        return true;
      }
      client.close() = {
        valve.close();
        setNextState(Moving);
        return true;
      }
    }

  • Delete the parameters from the Moving state declaration.

  • Delete the entry function from the Moving state.

  • Add the transitions for the isOpen() and isClosed() functions to the Moving state and replace the spontaneous transition state with a transition for the incoming signal event valve.moveEnded(…) as follows:

        state Moving {
      client.isOpen() = false
      client.isClosed() = false

      valve.moveEnded(result) = {
        client.moveEnded(result);
        setNextState(Ready);
      }
    }

The complete Coco for this component is in Example_06B/src/ArmourImpl.coco.

Verifying your Changes (Example_06B)

The verification finds the ArmourImpl component is not well-formed, because its queue capacity is exceeded:

User User ArmourImpl ArmourImpl valve valve setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) [nondet ] ValidParameters [nondet ] ValidParameters return true return true return true return true open() open() open() open() [nondet 0] posi…r.Status.Opened [nondet 0] position = Valve…er.Status.Opened (queued): moveE…(Status.Opened) (queued): moveEnded(Status.Opened) Initial Initial Initial Initial Initial Ready Ready Ready Ready Ready Ready Ready Ready Ready Queue full. Exception counterexample

This counterexample illustrates how the ArmourImpl component can receive a signal from its required port valve. This immediately exceeds its queue capacity, because we didn’t specify a queue for ArmourImpl that can hold any signals.

Specifying a Queue

To fix the verification error above, we need to add the following line immediately in front of the ArmourImpl component’s declaration:

@queue(1)

The complete Coco for this component is in Example_06C/src/ArmourImpl.coco.

Verifying your Changes (Example_06C)

All of the ports and components verify successfully.

Understanding the Moving state

When completing the changes to the Moving state of the ArmourImpl component, we added transitions for the isOpen() and isClosed() so that when called in this state, they always return false. Why is this necessary? There are top level transitions defined in Main for these two functions that return the actual state of the valve by calling the corresponding functions on the ValveController port.

As an exercise, comment out these two transitions in the Moving state, run the verification and display the resulting counter example.

As a general rule, we don’t want an armour component to do anything except protect the system from runtime failures if a client misbehaves. That is, if the client makes a function call when that function call is not allowed. In this example, ArmourImpl is not concerned with whether the valve is opened or closed because this has no bearing on whether function calls are allowed. ArmourImpl only has to keep track of whether the valve is moving or stationary. This is why isOpen() and isClosed() are implemented by calling the corresponding functions provided by ValveControllerImpl instead of maintaining a copy of the valve’s state.

When the client calls open() or close(), isOpen() and isClosed() must both return false until ArmourImpl sends a moveEnded(…) signal to its client. It will only do this when it has processed the corresponding moveEnded(…) signal received from ValveControllerImpl.

However, ValveControllerImpl performs valve movements asynchronously with respect to ArmourImpl. Therefore, there is a window during which calls to the ValveController functions isOpen() or isClosed() could return true before ArmourImpl has sent the moveEnded(…) signal to its client. This is because ArmourImpl has not yet processed the moveEnded(…) signal sent by ValveControllerImpl. The two transitions in ArmourImpl in the Moving state ensure that until ArmourImpl has processed the moveEnded(…) signal sent by ValveController, it always gives a consistent response to the isOpen() and isClosed() function calls.

Step 3: Building the ArmouredValveGroup Encapsulating Component

To make it more convenient for a client application using the armoured version of the ValveControllerImpl, we will make a new encapsulating component called ArmouredValveGroup. Clients that want to use the armoured version can then instantiate ArmouredValveGroup while clients that want the unarmoured version can instantiate ValveGroup. The armoured version would typically be used by clients not written in Coco, because their correct use of the ValveControllerImpl cannot be verified by the Coco Platform. In contrast, clients written in Coco would typically use the unarmoured version, because verifying these clients guarantees that they use the ValveControllerImpl correctly.

The new encapsulating component is declared as follows:

import unqualified Armour
import unqualified ArmourImpl
import unqualified TestValveGroup

@runtime(.MultiThreaded)
component ArmouredValveGroup {
  val client : Provided<Armour>

  val armour : ArmourImpl
  val testValve : TestValveGroup

  init() = {
    connect(client, armour.client);
    connect(armour.valve, testValve.client);
  }
}

The following architecture diagram is a graphical representation of ArmouredValveGroup:

ArmouredValveGroup armour : ArmourImpl testValve : TestValveGroup client : Armour client : Armour client : ValveController valve ENC ENC

This binds the TestValveGroup encapsulating component, which consists of instances of ValveControllerImpl, ValveDriverImpl and SimulatorImpl, to the ArmourImpl component, thereby forming a testable stack of software components. In turn, this means that a C++ program can then instantiate and access these components in a straightforward way.

Verifying Your Project (Example_07A)

The project verifies without errors.