This library contains an operational embedding of differential dynamic logic for the formal verification of hybrid systems. Hybrid systems contain continuously evolving and discretely evolving components, and arise in many safety- and mission-critical applications. Differential dynamic logic (dL) is a framework for formally specifying and reasoning about hybrid programs, where the specification allows modeling of hybrid systems, and its proof calculus allows for reasoning about such potentially complex programs. This embedding of dL is operational, meaning that it leverages the internal logic of PVS, resulting in a version of dL whose proof calculus is not only formally verified, but is also executable within PVS itself. The result is a Properly Assured Implementation of Differential Dynamic Logic for Hybrid Program Verification and Specification, Plaidypvs.
| Theory Name | Description |
|---|---|
hp_def |
Preliminary definitions for hybrid programs |
HP |
Datatype denoting hybrid programs |
NQBool |
Datatype for non-quantified boolean hybrid program expressions |
hp_expr |
More basics of hybrid programs including input/output semantics |
bounded_star_semantics |
Defines bounded star hybrid program and shows equivalence to star hybrid program |
bound_variables_def |
Defined bound variables for an HP |
bool_expr |
Defines boolean expressions and normalizeed nonquantifeid boolean expressions |
hp_props |
Example of reasoning about HP at the semantic definition level |
substitution |
Defines subsitution with properties for common real and boolean expressions |
ODEs_equiv |
Connects ODE library to ODEs |
differentiation |
Establishes rules of differentation |
chain_rule_re |
Proves chain rule for real expressions from chain rule in mv_analysis library |
diff_re_props |
Standard properties of differentiable real expressions |
continuity_re_def |
Define continuity of real expressions |
continuity_props |
Continuity properties for real expressions and environments |
continuity_re_props |
Standard arithmetic properties of continuous real expressions |
fresh_props |
Established properties of fresh variables |
bound_variables_def |
Define bound variables |
dynamic_logic |
Rules and rewrites of differential dynamic logic |
dl_solution |
Dl solve rule with examples |
sem_rel_diff_star |
Added rule to dL that was required for this development. The rules removes a STAR operator from Differential program |
dL_examples/ |
Directory of examples of using dL in PVS |
- J Tanner Slagel, NASA, USA
- Mariano Moscato, National Institute of Aerospace, USA
- Lauren White, NASA, USA
- César Muñoz, NASA, USA
- Swee Balachandran, National Institute of Aerospace, USA
- Aaron Dutle, NASA, USA
- J Tanner Slagel, NASA, USA, [email protected]