psy-taliro 1.0.0

Description:

psytaliro 1.0.0

Ψ-TaLiRo
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.
Models
Ψ-TaLiRo represents the cyber-physical system under test as a model.
Conceptually, a model is a function that maps a set of system inputs to a
timed series of states called a Trace. Ψ-TaLiRo provides two ways to
construct a model: the Blackbox and Ode models. The Blackbox model
makes no assumptions about the underlying system it represents. The Ode
model expects the underlying model to be represented using ordinary
differential equations.
Specifications
Ψ-TaLiRo tests are system requirements expressed in metric temporal logic
(MTL). Evaluation of the system requirement depends on a monitor, and
Ψ-TaLiRo supports several options. All specific implementations are
available in the 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



Optimizers
Ψ-TaLiRo generates inputs for the system under test by using an optimizer.
The optimizers provided by the toolbox are the UniformRandom and
DualAnnealing optimizers in the 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.
Type hints
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:

MyPy
Pyright
Pyre
Pytype

The easiest way to get started is to install
VSCode with the
python extension
which includes the pyright type checker.
Installation
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:

Pipenv
Poetry
Venv

(Anaconda)[https://www.anaconda.com] can also be used to create separate python
environments, and may be easier to set up on some systems.
Example
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)

Documentation
For additional details about the toolbox components, or example scripts, refer
to the documentation site.
Citing this project
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}
}