Seal

Work in progress. Seal is under active development; interfaces, representations, and results may change without notice, and some templates are known to be incomplete or unreliable on larger problems (see the notes in examples/run_examples.ml).

Seal is an OCaml library for the analysis of dynamical systems (linear, piecewise-linear, and polynomial) via invariant synthesis, built on sum-of-squares (SOS) programming and semidefinite programming solvers through OSDP.

It provides:

• A representation layer for linear, piecewise-linear and polynomial discrete-time dynamical systems, with guarded modes and casts between linear and polynomial forms (Seal.Dynsys).
• Quadratic invariant templates (round / shape / affine) for linear systems.
• k-inductive piecewise-quadratic invariant synthesis for piecewise-linear systems.
• Property-directed SOS Lyapunov-style invariant synthesis and per-variable reachable-set bounds for polynomial systems.
• A reachability invariant synthesis method based on Liouville's equation for polynomial systems.

Building

Seal uses dune and depends on osdp and num.

Seal currently needs osdp features not yet in a released version (the latest release on the official opam repository is 1.1.1). Until a new osdp release is published there, seal.opam pins osdp to the dev branch via pin-depends, so a plain opam install . from a clone of this repo resolves it automatically. Seal is not yet published on the official opam repository (packages there cannot use pin-depends), so opam install seal will not work until that osdp release lands.

git clone https://github.com/Embedded-SW-VnV/seal.git
cd seal
opam install . --deps-only
dune build
dune runtest

Usage

See examples/ for sample dynamical systems and examples/run_examples.ml for a smoke-test driver exercising the library end-to-end (representation casts, quadratic templates, piecewise-quadratic invariants, property-driven SOS templates, and reachability bounds).

dune exec examples/run_examples.exe

References

Seal implements methods described in the following publications:

• Pierre-Loïc Garoche. Formal Verification of Control System Software. Princeton University Press, 2019.
• Victor Magron, Pierre-Loïc Garoche, Didier Henrion, Xavier Thirioux. Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems. SIAM J. Control Optim. 57(4): 2799-2820 (2019).
• Assalé Adjé, Pierre-Loïc Garoche. Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs. Comput. Lang. Syst. Struct. 47: 44-61 (2017).
• Assalé Adjé, Pierre-Loïc Garoche, Victor Magron. Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization. SAS 2015: 235-251.
• Assalé Adjé, Pierre-Loïc Garoche. Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. VMCAI 2015: 99-116.
• Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche, Eric Feron. A generic ellipsoid abstract domain for linear time invariant systems. HSCC 2012: 105-114.

License

Seal is distributed under the GNU Lesser General Public License, version 3 or later (LGPL-3.0-or-later). See LICENSE for the full text.

Authors

Pierre-Loïc Garoche (ENAC) — pierre-loic.garoche@enac.fr