PV1 STLInspectoraids the creation of signal temporal logic specs

Tool for the systematic validation of Signal Temporal Logic (STL) specifications against informal textual requirements.

Application domain/field

Type of tool

Debug/testing tool for STL specifications

Expected input

STL formula

Format:

Own textual format

Expected output

User is presented with test signals for which needs to be decided whether or not the signal satisfies the informal requirement. If an error was found, the user can change the STL candidate and continue inspection.

Internals

STLInspector tries to identify typical faults that occur in the process of formalizing requirements by mutating a candidate STL specification. The requirements engineer is used as an oracle. Uses ANTLR, Z3.

Comments

License: Apache License 2.0
STL

Links

Repository: https://github.com/STLInspector/STLInspector

Last commit date

30 September 2019

Related papers

https://doi.org/10.1007/978-3-319-63387-9_11 (CAV '17)

Last publication date

13 July 2017

Related tools

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.