FLOW*

FLOW

Description: A Cyber-Physical System (CPS) can be viewed as a computer program that interacts with a physical environment. Such a system can be formalized by a hybrid automaton which equipped with finitely many discrete states and continuous variables. A state of a hybrid automaton can be denoted by a discrete state along with a valuation of the variables.

The reachability problem on hybrid automata can be defined as follows. Given a hybrid automaton A , an initial set X_0 and a state x , is x reachable in A from X_0 ? Reachability plays a key role in the verification of hybrid automata. For example, in safety verification, we want to check whether an unsafe state is reachable by the system.

The tool FLOW* focuses on reachability-based verification of hybrid automata. Since the reachability problem on hybrid automata is not decidable, the tool computes an over-approximation for a reachable state set. If a given state is not included then it is absolutely unreachable. The over-approximation set is represented as a finite set of Taylor models.

VO Integration: No

Active: Yes

Available Benchmarks: Yes

Website: https://flowstar.org/

Download: Link

Documentation: There is sparse documentation. There are some short usage examples as well as an examples of a model on the tool website. Links to relevant publications are here.

Contact: Link to list of contributors.

Graphic and excerpt from: https://flowstar.org/