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

• Signal Temporal Logic (STL)
• Requirements
• Mutation testing

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