pHL-SV/3.16 — Hybrid Language (Safety Verification)¶
| Type: | package |
|---|---|
| State: | under development and/or testing |
| Servers: | vm3, vm2, vm1 |
About¶
pHL-SV is an improvement of the software dReal/dReach [2]. It is one of the middle level components of the pHL set of packages and it is a tool for safety verification of hybrid systems. It answers questions of the type: Can a hybrid system run into an unsafe region of its state space? This question can be encoded to SMT formulas and answered by the SMT solver pHL-RT. This package is able to handle general hybrid systems with nonlinear differential equations and complex discrete mode-changes. Since pHL-RT implements a delta-complete decision procedure, pHL-SV performs “bounded delta-complete reachability analysis”.
sDL structure¶
Follows the standard sDL structure:
//%SCOPE description text
#include "somefile"
BEGIN-CODE [ pHL-SV/3.16 | {package options} ]
{package commands}
END-CODE
Commented lines, in the CODE body text, start with “##”.
Namespaces and commands¶
The standard “core” namespace is available.
Folders¶
(information will be added later by the package administrator)