Model based testing with F#, C# and JTorX

Model based testing can be applied to rigorously test software modules. The basic concept is that there is some specification (a model) and an implementation (can be a model or a piece of software). The implementation is regarded as a black box, also known as system under test (SUT). In this post, I'll give a very simple example of a situation where this technique can be applied. I'll be using JTorX as a tool for testing.

Consider a simple coffee machine. Fill it up with some water, fill the pod with some coffee beans, press a button and enjoy a cup of coffee.

It is possible to model such a process with a mealy machine. The following model could be an accurate description of a coffee machine:

According to the model, the machine has at least the following properties:

  • Pressing the coffee button before inserting both water and coffee beans will result in failure.
  • When the coffee machine has failed, the only way to reset it is to clean it.

We model the coffee machine as a set of states (the circles in the picture), where each state resembles some possible state of the coffee machine. We consider a to be the initial state. The machine can transition to another state because of user input (e.g. a user pressed a button). Each input also triggers an output: the coffee machine is capable of reporting "Ok", "Fail" and it should be able to output some coffee. Each edge in the graph is of the form "input / output". The idea is that this model is a specification of the behaviour we expect from a system that is considered to be a coffee machine. It's possible to use this specification for testing. We will use the ioco (input-output conformance) relation defined on labelled transition systems to make this happen. I will not go deeply into this theory, everything is explained in detail in the paper "Model Based Testing With Labelled Transition Systems" by Tretmans.

In order to use ioco, we need to convert the mealy machine to a labelled transition system (LTS). In essence, the main difference is that each transition (edge) of a LTS describes precisely one output or input. The mealy machine describes both an input and output for each transition. We can easily convert each transition from the mealy machine to a LTS using this conversion tactic:

Unfortunately, the resulting LTS model is not quite as readable:

Now that we have a LTS, we can use the ioco relation to test implementations for conformance. This is done by testing each "trace" of the specification (the LTS) with the implementation to see if the output conforms with the output that is allowed by the specification. A trace is a path from one state p in the graph to another state q:  p \xrightarrow{a} q, where a is some output or input. It can be empty (\epsilon) or it can be quiescent, but we will not go in detail about that here.  p \xrightarrow{a . b} q is shorthand for  p \xrightarrow{a} q' \xrightarrow{b} q . An example trace of the LTS model is  a \xrightarrow{?water . !ok . ?pod . !ok . ?button } h. ioco requires that all possible outputs of the implementation after a trace are foreseen by the specification. Formally, this is defined by  \forall s \in \text{Straces}(\text{spec}). \ out(\text{impl} \ \textbf{after} \ s) \subseteq out(\text{spec} \ \textbf{after} \ s) . We have that out(spec \ \textbf{after} \ \text{?water . !ok . ?pod . !ok . ?button}) = \{ \text{!coffee} \}, if a = \ \text{spec}. This means that an implementation cannot output tea after we press the button on the coffee machine. However, if the trace is not defined by the specification, the implementation can define any behaviour it desires for that particular trace. This means that the trace is underspecified. For more information about ioco, please take a look at the paper I referenced earlier.

Now let's define a simple implementation of a coffee machine in F#:


module Machine

type States  = A | B | C | D | E | F

type Inputs  = Pod | Clean | Water | Button

type Outputs = Fail | Ok | Coffee

type State   = States

let transitionFunc = dict [
                            (A, Clean),  (A, Ok);
                            (A, Pod),    (B, Ok);
                            (A, Button), (F, Fail);
                            (A, Water),  (C, Ok);
                            (B, Pod),    (B, Ok);
                            (B, Clean),  (A, Ok);
                            (B, Button), (F, Fail);
                            (B, Water),  (D, Ok);
                            (C, Pod),    (D, Ok);
                            (C, Clean),  (A, Ok);
                            (C, Water),  (C, Ok);
                            (C, Button), (F, Fail);
                            (D, Pod),    (D, Ok);
                            (D, Clean),  (A, Ok);
                            (D, Water),  (D, Ok);
                            (D, Button), (E, Coffee);
                            (E, Clean),  (A, Ok);
                            (E, Button), (F, Fail);
                            (E, Water),  (F, Fail);
                            (E, Pod),    (F, Fail);
                            (F, Clean),  (A, Ok);
                            (F, Button), (F, Fail);
                            (F, Water),  (F, Fail);
                            (F, Pod),    (F, Fail);
                          ]

let coffeeMachine input state = 
        let success, result = transitionFunc.TryGetValue((state, input))
        if success then Some(result) else None
    
let initialState = A

The main definition in the code above is the function transitionFunc : State \times Input \rightarrow State \times Output, which is modeled as a set. Given some state and input, it will return the associated next state and output if present. We would like to test this implementation using the specification defined earlier. In order to do this, we need some way to communicate with the above program (system under test). Therefore, we construct a simple C# application that is able to communicate through sockets:


using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Net.Sockets;
using System.Text;
using System.Net;
using Microsoft.FSharp.Core;

namespace CoffeeMachine
{
    class Program
    {
        static void Main(string[] args)
        {
            StartServer(5000);
        }

        static void StartServer(int port)
        {
            var server = new TcpListener(IPAddress.Any, port);

            server.Start();

            while ( true )
            {
                var client = server.AcceptTcpClient();

                HandleClient(client);

                client.Close();
            }
        }

        static void HandleClient(TcpClient client)
        {
            var networkStream = client.GetStream();
            var state = Machine.initialState;
            var outputs = new Dictionary<Machine.Outputs, string>()
            {{Machine.Outputs.Coffee, "!coffee"}, {Machine.Outputs.Fail, "!fail"}, {Machine.Outputs.Ok, "!ok"}};

            var inputs = new Dictionary<string, Machine.Inputs>() {
                {"?button", Machine.Inputs.Button},
                {"?pod", Machine.Inputs.Pod},
                {"?clean", Machine.Inputs.Clean},
                {"?water", Machine.Inputs.Water},
            };

            var states = new Dictionary<Machine.States, string>() {
                {Machine.States.A, "A"},
                {Machine.States.B, "B"},
                {Machine.States.C, "C"},
                {Machine.States.D, "D"},
                {Machine.States.E, "E"},
                {Machine.States.F, "F"},
            };

            using (StreamWriter writer = new StreamWriter(networkStream))
            {
                using (StreamReader reader = new StreamReader(networkStream))
                {
                    string inputStr = string.Empty;
                    while ((inputStr = reader.ReadLine()) != null)
                    {
                        Machine.Inputs input = null;
                        if (inputs.TryGetValue(inputStr, out input))
                        {
                            var output = Machine.coffeeMachine(input, state);
                            
                            if (FSharpOption<Tuple<Machine.States, Machine.Outputs>>.get_IsSome(output))
                            {
                                Console.WriteLine("read {0}, output: {1}. new state: {2}", inputStr,
                                    outputs[output.Value.Item2], states[output.Value.Item1]);

                                state = output.Value.Item1;
                                writer.WriteLine(outputs[output.Value.Item2]);
                                writer.Flush();
                            }
                        }
                        else
                        {
                            Console.WriteLine("do not understand {0}", inputStr);
                        }
                    }
                }
            }
        }
    }
}

The above program accepts connections and routes inputs to the coffee machine we've defined in F#. Now we can use JTorX to test the implementation:

Configure JTorX such that it will communicate with our SUT using sockets (select the proper option for "implementation"). Then enter "localhost!5000" to configure the endpoint. Now that it is configured, it is possible to let JTorX test the implementation. Press the start button on the "Test" tab. Then press "Auto". JTorX will happily traverse the LTS model and test each path with the implementation. When each path is covered, you can stop the test process by clicking the "Stop" button. A message sequence chart and coverage analysis is maintained during testing.

Of course, the coffee machine is an extremely trivial example. More complex examples include protocol specifications or parts of larger systems that can be expressed with state machines.

Comments are closed.