Welcome to \(\Psi\)-TaLiRo

\(\Psi\)-TaLiRo is a python toolbox for search-based test generation, typically at the system level. The objective of this library is to make writing and testing requirements for systems fast and easy in order to help facilitate the adoption of formal and semi-formal methods for verifying systems of all kinds. To this end, \(\Psi\)-TaLiRo defines several testing interfaces and multiple ready-to-use implementations so that users can quickly set up tests to ensure no bugs or behavioral violations hide in their systems.

Motivation

Consider that we are designing a simple switching thermostat system described by the following state machine:

Source: An Algebra of Hybrid Systems by Bernhard Moller and Peter Hofner (2009).

When designing a system such as this one, we may be curious if there are any system inputs that cause the system to violate its operating bounds. A naive approach would be to test all possible inputs, but in a continuous input space like ours this approach is infeasible. Furthermore, for more complex systems the input space may be very large, making a brute force approach even more intractable. Therefore, we will instead leverage search techniques to test a subset of inputs, using the results from each test to try and select inputs that will put the system closer to violating its operating bounds. In order to do this, we must first create a representation of our system that we can use to simulate its behavior. One possible representation of this system is the following Python class:

import enum

class Thermostat:
    class Mode(enum.IntEnum):
        HEATING = 1
        COOLING = 2

    def __init__(self, initial_temp: float):
        self.temp = initial_temp
        self.mode = Thermostat.Mode.COOLING

    def step(self, step_size: float):
        if self.mode is Thermostat.Mode.COOLING and self.temp < 19:
            self.mode = Thermostat.Mode.HEATING

        if self.mode is Thermostat.Mode.COOLING and self.temp > 21:
            self.mode = Thermostat.Mode.COOLING

        temp_dot = -0.1 * self.temp

        if self.mode is Thermostat.Mode.HEATING:
            temp_dot = 5 + temp_dot

        self.temp = self.temp + temp_dot * step_size

Using this definition, we can define a model component that is responsible for encapsulating the execution logic of the model given a set of inputs.

from staliro import models

STEP_SIZE = 0.1

@models.model()
def thermostat(inputs: models.Sample) -> models.Trace[list[float]]:
    system = Thermostat(inputs.static["temp"])
    states = {}

    for step in range(100):
        time = step * STEP_SIZE
        states[time] = [system.temp]
        system.step(STEP_SIZE)

    return models.Trace(states)

Then we can represent a requirement of our system (in this case that the temperature of the system stays within the interval \([18.0, 22.0]\)) using Signal Temporal Logic.

from staliro import specifications

req = specifications.RTAMTDense("(always (temp >= 18.0 and temp <= 22.0)", {"temp": 0})

Finally, we can instantiate an optimizer and define the test parameters in order to begin executing tests

from staliro import TestOptions, optimizers, staliro

optimizer = optimizers.UniformRandom()
options = TestOptions(
    runs=1,
    iterations=100,
    static_inputs={
        "temp": (18.0, 22.0),
    }
)

runs = staliro(thermostat, req, optimizer, options)

The optimizer we have chosen to use is the Uniform Random optimizer which will generate samples uniformly across the input space. For our test parameters, we run a single optimization attempt, with a sample budget of 100 samples, and we generate a single system input called \(temp\) which will be within the interval \([18.0, 22.0]\). We execute the test by calling the staliro() function, which returns a set of Run values containing all the samples generated by the optimizer, as well as their associated cost values.

To quickly begin setting up your own tests, please refer to the Quickstart and Examples pages. For more in-depth descriptions of the interfaces and components provided by \(\Psi\)-TaLiRo please refer to the API documentation.

Citing this project

To cite our work, please include a reference to the following paper or include our \(Bib\TeX\) entry in your bibliography file.

PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems

@InProceedings{10.1007/978-3-030-85248-1_15,
    author="Thibeault, Quinn and Anderson, Jacob and Chandratre, Aniruddh and Pedrielli, Giulia and Fainekos, Georgios",
    editor="Lluch Lafuente, Alberto and Mavridou, Anastasia",
    title="PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems",
    booktitle="Formal Methods for Industrial Critical Systems",
    year="2021",
    publisher="Springer International Publishing",
    address="Cham",
    pages="223--231",
    isbn="978-3-030-85248-1"
}