Conform Tutorial

In this tutorial we will write and evaluate a specification for an example system from the Modality tracing.rs library (opens new window).

# Before You Start

This tutorial builds off of the Modality tutorial. (opens new window) Specifically, we will write and evaluate specifications against the data generated in that tutorial. If you haven't yet, follow the instructions in the Modality tutorial, then return here.

# Setup

First, install Conform. Make sure you complete the steps in the installation guide to tell the Conform CLI where it can access the modalityd API and to make an auth token available to the CLI. For simplicity, in this tutorial we will assume you are installing conform on the same machine where you have installed modality and modalityd and followed the Modality tutorial, since this is the easiest way to proceed.

$ sudo apt-get install conform

# A Simple Specification

We will start by writing a simple specification.

# Components of a Specification

Specifications in Conform use a syntax which naturally lends itself to describing system behavior and requirements. Each specification is made up of one or more behaviors, and each behavior contains one or more cases, as well as a single optional when block.

There are 3 types of case:

nominal case blocks describe how your system should behave.
recovery case blocks describe how your system is expected to deal with adverse conditions.
prohibited case blocks describe things your system should never do.

The when block changes the semantics of the behavior so that its cases must match every time the when block is matched, rather than only needing to satisfy the cases a single time.

# The Example System

The example system is a simplified simulation of a system with 3 components. There is a producer component which takes some measurements. It then sends these measurements to a consumer component, which acknowledges their receipt. In addition, both the producer and consumer regularly send heartbeat messages to a monitor component.

For this tutorial we will focus on the messages that go between the producer and consumer. To start, let's write a specification to verify that every message sent by the producer is received by the consumer. We will put the following specification in a file named tutorial.speqtr:

behavior "Messages should be received"
    when "The producer sends a message"
        "Producer sending measurement message"@producer AS SentMessage
    end

    nominal case "The consumer receives the message"
        SentMessage FOLLOWED BY
          "Received measurement message"@consumer AS ReceivedMessage
          AND SentMessage.sample = ReceivedMessage.sample
    end
end

This specification has a when block to describe a precondition and a nominal case block to describe the system's expected behavior. In plain English, the specification says "Every time I see the producer send a message, I should then see the consumer receive a message with the same sample value".

SpeQTr

For more information on how to write specifications and all the different ways you can describe system behavior check out the SpeQTr documentation. (opens new window)

# Creating and Evaluating Specifications

Now that we have a specification written in a file, let's create the specification so Conform can track its revisions and evaluation results.

$ conform spec create tutorial --file tutorial.speqtr
Created spec 'tutorial' at version 'cf318f03-ba70-4555-a1a2-fea61f09dffd'

The output tells us we've successfully created the specification and gives us the current version ID (more on that later). Now that we have a specification, let's evaluate it!

Note

We're using example data that we generated during the Modality tutorial. (opens new window) If you haven't yet, follow the steps in that tutorial to generate data to evaluate this specification against.

Conform and Modality ship with a default setup to automatically select the set of data from your most recent run, so we will just use that default setup to evaluate this specification against our run of the example system.

$ conform spec eval --name tutorial
No explicit workspace provided. Using the default workspace.
evaluation of spec "tutorial"
[ ✔ ] segment "Run 0e60118a-50f0-4326-85b4-ba8eb802fd60"
[ ✔ ]   behavior "Messages should be received"
All Evaluations Passed
Behaviors: [1: Passed] [0: Inconclusive] [0: Failed] (stored as d3ca18f3-71fc-442e-a025-64eff17dea1b)

Great news, we've confirmed that every single message sent by the producer was received by the consumer. The output also shows us the evaluation result ID at the end, which will allow us to recall these results if we need them later.

# Updating a Specification

Now, let's make our specification just a bit more demanding. It turns out our system requirement isn't just for every message to be received eventually, but that we need the consumer to receive messages within 850 microseconds. We can easily add this constraint to our specification by updating the relationship connective from FOLLOWED BY to FOLLOWED BY WITHIN 850us. We'll put the new version of the specification in a file named updated-tutorial.speqtr. It looks like this:

behavior "Messages should be received in a timely manner"
    when "The producer sends a message"
        "Producer sending measurement message"@producer AS SentMessage
    end

    nominal case "The consumer receives the message within allowable time"
        SentMessage FOLLOWED BY WITHIN 850us
          "Received measurement message"@consumer AS ReceivedMessage
          AND SentMessage.sample = ReceivedMessage.sample
    end
end

We can now update our tutorial specification to reflect this new constraint:

$ conform spec update tutorial --file updated-tutorial.speqtr
Updated spec 'tutorial' to version 'a659500e-2c6d-49b4-8137-cf2704246765'

To confirm our specification is updated let's inspect tutorial to see its version history:

$ conform spec inspect tutorial
Spec: tutorial

Updated By:		tutorial
Updated At:		2022-08-25 01:45:35 UTC
Current Version:	a659500e-2c6d-49b4-8137-cf2704246765

Other Versions:
	* a659500e-2c6d-49b4-8137-cf2704246765	Created at 2022-08-25 01:45:35 UTC by tutorial
	■ cf318f03-ba70-4555-a1a2-fea61f09dffd	Created at 2022-08-25 01:35:29 UTC by tutorial
Spec Evaluations: 0

This shows us that we have two versions of the tutorial spec, and that the current one has never been evaluated. Let's evaluate it and see what we get:

$ conform spec eval --name tutorial
No explicit workspace provided. Using the default workspace.
evaluation of spec "tutorial"
[ ✘ ] segment "Run 0e60118a-50f0-4326-85b4-ba8eb802fd60"
[ ✘ ]   behavior "Messages should be received"
Failures Detected
Behaviors: [0: Passed] [0: Inconclusive] [1: Failed] (stored as 61f0854a-4822-43e9-a7a3-7bab137c15b2)

  |
1 | behavior "Messages should be received"
  |
6 |   nominal case "The consumer receives the message"
7 |     SentMessage FOLLOWED BY WITHIN 850us "Received measurement message"@consumer AS ReceivedMessage AND
  |                             ^^^^^^^^^^^^ Did not match
8 |     SentMessage.sample = ReceivedMessage.sample
9 |   end
  |
  = error: When evaluating the behavior 'Messages should be received', no expected
           cases matched. The case 'The consumer receives the message' partially
           matched, but an event matching the subexpression 'WITHIN 850us' was
           not found.

Note

Depending on how long you ran the example system it is possible that this specification will pass for you. If you would like to explore what happens with a failing specification try running the example system for longer and it is likely to produce failing data.

This time our specification fails. Conform's logical analysis helpfully indicates that the violation is because of the time constraint—it can find a "received message" event for every "sent message" event, but not always within the time limit.

# Adding Recovery Behavior

So far we have described our system's expected behavior in the nominal case. SpeQTr also lets us use a recovery case to say how our system is expected to handle situations outside of standard operation. Let's add a grace period for messages that may be sent when the system is shutting down. We will put our new spec in a file named recovery-tutorial.speqtr:

behavior "Messages should be received"
    when "The producer sends a message"
        "Producer sending measurement message"@producer AS SentMessage
    end

    nominal case "The consumer receives the message within allowable time"
        SentMessage FOLLOWED BY WITHIN 850us
          "Received measurement message"@consumer AS ReceivedMessage
          AND SentMessage.sample = ReceivedMessage.sample
    end

    recovery case "The pipeline is shutting down, message receipt is not guaranteed"
        SentMessage FOLLOWED BY WITHIN 5s "Shutting down"@producer
    end
end

Now, let's update our specification and evaluate it again:

$ conform spec update tutorial --file recovery-tutorial.speqtr
Updated spec 'tutorial' to version '4ef43db4-4cac-4f5a-9103-e7e66cd133b8'

$ conform spec eval --name tutorial
No explicit workspace provided. Using the default workspace.
evaluation of spec "tutorial"
[ ✘ ] segment "Run 0e60118a-50f0-4326-85b4-ba8eb802fd60"
[ ✘ ]   behavior "Messages should be received"
Failures Detected
Behaviors: [0: Passed] [0: Inconclusive] [1: Failed] (stored as 20701255-a919-4bc8-b921-e5e35acab1fd)

  |
1 | behavior "Messages should be received"
  |
6 |     nominal case "The consumer receives the message within allowable time"
7 |         SentMessage FOLLOWED BY WITHIN 850us "Received measurement message"@consumer AS ReceivedMessage AND
  |                                 ^^^^^^^^^^^^ Did not match
8 |         SentMessage.sample = ReceivedMessage.sample
9 |     end
  |
  = error: When evaluating the behavior 'Messages should be received', no
           expected cases matched. The case 'The consumer receives the message
           within allowable time' partially matched, but an event matching the
           subexpression 'WITHIN 850us' was not found.

Our updated specification still fails. This confirms that the problem was not just system shutdown and that there is in fact a bug in the system.

← Editor Integration config →