An extensible Python toolbox for search-based test generation for cyber-physical systems. This work is based of the MATLAB toolbox S-TaLiRo, which is available here.
staliro.specifications
module. To use a specification, you
will need to ensure that the monitor library is installed. Additional
information is available in the table below:
Monitor | Installation | Link |
---|---|---|
RTAMT | pip install rtamt |
homepage |
TLTK (*Linux only) | pip install tltk_mtl |
homepage |
Py-TaLiRo | pip install pytaliro |
homepage |
staliro.optimizers
module.
For other optimizer options, see the PartX repository. There you will find additional implementations that give extra guarantees about the system input space.
This toolbox provides PEP484 type hints to help ensure correct usage. To use the type hints, you will need to install one of the several type hint checkers available for python. A non-exhaustive list is:
The easiest way to get started is to install VSCode with the python extension which includes the pyright type checker.
To install this toolbox, run the command pip install psy_taliro
. To avoid
installing python packages globally, you can use a virtual environment to
keep the packages in a project-specific directory. Some of the tools for
managing virtual environments are:
(Anaconda)[https://www.anaconda.com] can also be used to create separate python environments, and may be easier to set up on some systems.
from math import pi
from staliro import models, optimizers, specifications
from staliro.options import Options
from staliro.staliro import staliro
@models.blackbox()
def aircraft_model(X, T, U):
"""Blackbox model that represents the dynamics of an aircraft.
Arguments:
X: The static (initial) inputs to the system. A four-element vector of
the form [roll, pitch, yaw, thrust].
T: Interpolation times for the input signals
U: Interpolated values of the time-varying input signals
Returns:
trace: A set of timed state values representing the altitude of the
aircraft over time
"""
...
optimizer = optimizers.UniformRandom()
requirement = "[] (alt > 0.0)" # Requirement that the aircraft does not crash
specification = specifications.RTAMTDense(requirements, {"alt": 0}) # The altitude value is in the first column of the aircraft trace states
options = Options(
runs=10, # 10 independent optimization attempts
iterations=100, # Generate 100 samples per optimization attempt
interval=(0.0, 2.0), # Simulation interval is from 0 to 2 seconds
static_parameters=[
(-pi / 4, pi / 4), # Roll
(-pi / 4, pi / 4), # Pitch
(-pi / 4, pi / 4), # Yaw
(0, 100), # Thrust
]
)
result = staliro(aircraft_model, specification, optimizer, options)
For additional details about the toolbox components, or example scripts, refer to the documentation site.
If you use this toolbox in your research, include this citation in your bibliography
@misc{psy-taliro,
doi = {10.48550/ARXIV.2106.02200},
url = {https://arxiv.org/abs/2106.02200},
author = {Thibeault, Quinn and Anderson, Jacob and Chandratre, Aniruddh and Pedrielli, Giulia and Fainekos, Georgios},
keywords = {Software Engineering (cs.SE), Systems and Control (eess.SY), FOS: Computer and information sciences, FOS: Computer and information sciences, FOS: Electrical engineering, electronic engineering, information engineering, FOS: Electrical engineering, electronic engineering, information engineering},
title = {PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems},
publisher = {arXiv},
year = {2021},
copyright = {arXiv.org perpetual, non-exclusive license}
}