PV3 ⊧ ForeSee: Formula Exploitation by Sequence Tree for falsificationgenerates an input that triggers a violation of the user-specified property

Application domain/field

• Falsification
• Cyber-physical systems
• Hybrid systems
• Temporal logic
• Optimization-based falsification
• Signal temporal logic (STL)

Expected input

• Simulink model
• STL specification

Format:

Simulink model

Expected output

Input that triggers the violation of the specification?

Internals

Falsification: Given a desired temporal specification, try to find an input of violation instead of a proof guarantee.

Comments

License: GPL-3.0