Skip to main content

Verifier: Test a Software Component

This tutorial focuses on the Verify tool in Tangram Pro™. Verify allows you to run a software component in a container and test it against a message sequence model so you can be more confident that your software is doing what it's supposed to do. We made this tool to help streamline the verification of software behavior in an online collaborative workspace that links a component in a system design to actual software and user-defined test protocols.

You'll learn how to:

  • Configure a software component and test environment
  • Define test scenarios using protocols
  • Configure and run tests

What software will be tested in this tutorial?

  • We provide example source code in GitHub for a C++ software component that one might find on a mission-critical UAV (albeit a simplified version for demonstration purposes) that processes mission commands.
  • This source code utilizes Tangram Pro-generated interface libraries that enable processing messages defined by the OpenUxAS LMCP standard and communicating over a ZeroMQ transport.

What behavior will be tested in the example software component?

The software is expected to handle these two mission sequences:

  1. When it receives a MissionCommand message, a sequence of messages is expected to be exchanged
  2. When it receives a CameraAction message, a different sequence of messages is expected to be exchanged

Additionally, there are specific values or ranges of values that are expected within these messages. Tangram Pro can help verify those as well!

Step 1: Connect to GitHub​

Your Tangram Pro account can pull containers from GitHub and GitLab registries to run software executables and container images. For this tutorial, we provide example source code in GitHub.

Prerequisite

A GitHub account is required to complete this tutorial. If you do not have one, please go to https://github.com/ to set one up.

Once you've confirmed your GitHub login, go ahead and connect your Tangram Pro account to it:

  1. In Tangram Pro, go to User Settings by clicking your avatar image in the upper right corner of the page
  2. Scroll down to Source Control and click Add Hosting Service
  3. Choose GitHub.com
  4. Click the Register an OAuth App link to open GitHub
  5. Follow these instructions to complete the integration

Now you'll be able to link GitHub repositories to components in Tangram Pro. We'll do that in a later step.

Step 2: Create a Project​

To get started create a new project:

  1. Go to Projects and click New Project
  2. Enter a Project Name
  3. Select your account for Owner

Step 3: Add a Transport​

Add a transport (or networking) library to your project. The example software component requires the ZeroMQ library to send and receive messages. Let's add it:

  1. Find Transports on the lefthand side and click the + button
  2. Choose ZeroMQ

Step 4: Add a Component​

The example software is expected to be able to process a specific subset of LMCP formatted messages. Let's add those to a component.

Add components and messages in Flex​

Components and messages can also be added directly via a .flex file:

  1. Go to FlexLang in the top navigation bar

  2. Click on Package Manager and then the blue New button

  3. Enter a name for your package using the Namespace::PackageName format (e.g. Tutorial::Package), and choose an owner

  4. Click Create Package and wait for the Flex environment to load

  5. Create a new file by hovering over your package in the left side file viewer and clicking the File icon (the first icon to the right of your package name)

  6. Enter the name "protocols.flex" and hit enter

  7. Paste the following code below the module name:

import OpenUxAS::LMCP::v3.afrl.cmasi (
  MissionCommand,
  CameraAction,
  CameraConfiguration,
  CameraState,
  GoToWaypointAction,
  AirVehicleState )
  1. Save the file by pressing the hot-key Ctrl + S / Cmd + S

Step 5: Resolve Package Dependencies​

  1. To get rid of the import errors, click the Dependencies icon between the magnifying glass and the checkmark in the Package Manager (Hint: it should look like a box or package)
  2. Search for and add OpenUxAS::LMCP::v3 as a dependency
  3. Select the dependency package's version or leave it as the default, which in this case should be release r0.

Step 6: Configure Repository​

  1. Select the "MissionComputer" component on the left
  1. Click the Code tab
  2. For Host URL choose https://github.com (this is what you setup at the beginning)
  3. For Repository type in the following name tangrampro-verify-examples and select it
  4. The Branch Name will auto-populate with master. Keep that as is.

Step 7: Create Test Protocols​

Nice work! Now let's start defining our test protocols inside our Flex package.

IMPORTANT: Since your Flex package is not a Source of Truth for your new project, you must edit the package from the Flex editor within the project. Click the "Flex" button in the top right of the project header bar, and open your package there.

A protocol is an ordered list of constrained messages that will be input to and should be output by your component-under-test. You can add multiple protocols to cover as many test scenarios as you need.

Let's start by adding the following "Rescue" mission protocol, which our software component should support.

  • Our component receives a MissionCommand from a control station
  • Our component reports the UAV's location in 3D space via an AirVehicleState message
  • Our component receives a GoToWaypointAction command to fly the UAV to a new location
  • Our component again reports an AirVehicleState to send updated UAV location data

To add this protocol:​

  1. Inside Protocols.flex, paste the following code below the line declaring your MissionComputer component:
  component MissionComputer;
  component ControlStation;

  local protocol Rescue in MissionComputer {                          // From the perspective of MissionComputer,
    recv let mission_command: MissionCommand assuming                 // expect to receive a MissionCommand from the ControlStation
        mission_command.FirstWaypoint == 0 &&                         // such that the first waypoint's
        mission_command.WaypointList[0].Number == 0 &&                //  * number is 0,
        mission_command.WaypointList[0].Latitude >= 19.50139 &&       //  * latitude falls between [19.50139, 64.85694)
        mission_command.WaypointList[0].Latitude < 64.85694 &&
        mission_command.WaypointList[0].Longitude >= -161.75583 &&    //  * longitude falls between [-161.75583, -68.01197)
        mission_command.WaypointList[0].Longitude < -68.01197
      from ControlStation;                                            // this MissionCommand should come from the ControlStation (i.e. Verifier's role)

    send any AirVehicleState to ControlStation;                       // To which we'll respond with an AirVehicleState message

    recv let new_location: GoToWaypointAction assuming                            // After which the ControlStation will send a GoToWaypointAction
        mission_command.WaypointList[0].Number == new_location.WaypointNumber     // matching the MissionCommand's first waypoint's Number
      from ControlStation;

    send let new_destination: AirVehicleState where                                         // Finally, we'll send our updated coordinates
        new_destination.Location.Latitude == mission_command.WaypointList[0].Latitude &&    // matching those from the received MissionCommand message's first waypoint
        new_destination.Location.Longitude == mission_command.WaypointList[0].Longitude
      to ControlStation;                                                                    // back to the ControlStation
  }

Now let's add the following "Scan" mission, which our software component should also support, as a protocol.

  • Our component receives a CameraAction from a control station
  • Our component reports the UAV camera's CameraConfiguration message
  • Our component receives another CameraAction command
  • Our component reports the UAV camera's CameraState

To add this protocol add the following flex code to your Protocols.flex file:​

local protocol Scan in MissionComputer {                            // Again from the perspective of MissionComputer,
  recv let camera_action: CameraAction from ControlStation;         // once we receive a CameraAction message from the ControlStation (i.e. Verifier),

  send let camera_config: CameraConfiguration where                                               // send back a CameraConfiguration with a MinHorizontalFieldOfView between [20.0, 150.0)
      camera_config.MinHorizontalFieldOfView >= 20.0 &&
      camera_config.MinHorizontalFieldOfView < 150.0 &&
      camera_config.MaxHorizontalFieldOfView >= camera_config.MinHorizontalFieldOfView &&         // and MaxHorizontalFieldOfView of [MinHorizontalFieldOfView, 150.0)
      camera_config.MaxHorizontalFieldOfView < 150.0
    to ControlStation;

  recv let camera_action2: CameraAction assuming                                                  // The ControlStation should then send another CameraAction with a field of view within the ranges we sent
      camera_action2.HorizontalFieldOfView >= camera_config.MinHorizontalFieldOfView &&
      camera_action2.HorizontalFieldOfView < camera_config.MaxHorizontalFieldOfView
    from ControlStation;

  send let camera_state: CameraState to ControlStation;
}

Understanding these protocols​

The where and assuming clauses of each message indicate constraints. By adding these conditions, messages can be called "valid" or "invalid" based on their contents, including how the messages of one field relate to a message that came previously in a sequence.

Let's examine the constraints found in the Rescue protocol. Because the MissionCommand message contains a list of Waypoints, it also 'has' the members of the Waypoint struct for each waypoint in its list -- just one waypoint in this example. The lines following assuming within the MissionCommand message specify valid ranges for the fields Number, Latitude, and Longitude within the Waypoint message structure, which will be used as input to our component. The latitude and longitude ranges encompass the continental US.

Since GoToWaypointAction is also an input, these constraints are controlling what values will be input to our component. By referencing MissionCommand_1, you're able to pull in data from the MissionCommand message at the beginning of the sequence.

The contents of the first AirVehicleState are relatively unimportant, but the second AirVehicleState should contain coordinates that match those provided within the original MissionCommand, and because AirVehicleState is an output, Tangram Pro will check the field values sent by our software component and verify they fit within these constraints when we run the test.

Next, let's review the constraints within the Scan sequence.

CameraConfiguration is an output, so when we run the test, Tangram Pro will check the field values sent by our software component and verify they fit within these constraints.

Conversely, CameraAction is an input, so these constraints are controlling the values that will be input to our component, making sure they fit within the range of what our software component specified in its CameraConfiguration message. For reference check out the logic in the source code here

Step 8: Run Tests​

Great work! Now let's run these tests.

  1. Click the Setup New Test button.
  2. Select Use Container Registry option, you will need to ensure that your registry is configured. See User Guide: Container Registrises
Container Registry Config information

Container registry host: ghcr.io

Path to the image: ghcr.io/tangramflex/tutorial-mission-computer:latest

  1. Keep all other options set as the defaults. For more information about these options see User Guide: Verify
  2. Click Begin Verifier Test

When a test is running, Tangram Pro provides live reporting as it processes and analyzes each protocol, including the contents of the messages being sent. When complete, the test summary is saved for you to view all of those details later.

Note: If a Timeout occurs, try running the test again.

Success! The two missions that our software component was expected to support have been verified!

How to read the results​

Tangram Pro reports a protocol as "Satisfied" if both of these conditions are met:

  • The messages were sent and received in the order specified by protocols
  • The message contents met all specified conditions

A protocol will be "Unsatisfied" if either of the above conditions are not met. It is important to note a protocol may be "Unsatisfied" if the wait time between subsequent messages exceeds the "Message Timeout" or if the number of retries reaches the "Max Path Retries".

Tangram Pro also provides two real-time log streams.

  • Component Logs: These are the logs output by your software component
  • Debug Logs: These are the logs output by Tangram Pro's test environment

To view previous tests​

  1. Go to View Tests
  2. Click on a test to view its results in more detail

What does an "Unsatisfied" test look like?​

  • Try adding add another message to one of the sequences, and run the test again.
  • Try removing a constraint, and run the test again.

Cheers!​

By completing this tutorial, you've learned how to use the Verify tool in Tangram Pro to test a software component against a message sequence model.

Check out what you accomplished:

  • Linked a component to GitHub repository
  • Defined test sequences and message field conditions
  • Linked a verifier test to Github registry
  • Verified the two missions are supported by our software component