object ModelPlex extends ModelPlexTrait with Logging
ModelPlex: Verified runtime validation of verified cyber-physical system models.
- See also
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyber-physical system models. Formal Methods in System Design, 42 pp. 2016. Special issue for selected papers from RV'14.
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyber-physical system models. In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of LNCS, pages 199-214. Springer, 2014.
- Alphabetic
- By Inheritance
- ModelPlex
- Logging
- LazyLogging
- LoggerHolder
- ModelPlexTrait
- Function2
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
val
INDEXED_POST_VAR: (Variable) ⇒ Variable
Returns the post variable of
v
identified by index increase.Returns the post variable of
v
identified by index increase.- Definition Classes
- ModelPlexTrait
-
val
NAMED_POST_VAR: (Variable) ⇒ Variable
Returns the post variable of
v
identified by name postfixpost
.Returns the post variable of
v
identified by name postfixpost
.- Definition Classes
- ModelPlexTrait
-
def
apply(vars: List[Variable], kind: Symbol, checkProvable: Option[(ProvableSig) ⇒ Unit]): (Formula) ⇒ Formula
Synthesize the ModelPlex (Controller) Monitor for the given formula for monitoring the given variable.
Synthesize the ModelPlex (Controller) Monitor for the given formula for monitoring the given variable. @ param kind The kind of monitor, either 'ctrl or 'model.
- checkProvable
true to check the Provable proof certificates (recommended).
- Definition Classes
- ModelPlex → ModelPlexTrait
-
def
apply(formula: Formula, kind: Symbol, checkProvable: Option[(ProvableSig) ⇒ Unit] = Some(_ => ()), unobservable: ListMap[_ <: NamedSymbol, Option[Formula]] = ListMap.empty): Formula
Synthesize the ModelPlex (Controller) Monitor for the given formula for monitoring the given variable.
Synthesize the ModelPlex (Controller) Monitor for the given formula for monitoring the given variable.
- Definition Classes
- ModelPlex → ModelPlexTrait
-
def
apply(vars: List[Variable], kind: Symbol): (Formula) ⇒ Formula
- Definition Classes
- ModelPlexTrait → Function2
-
def
applyAtAllODEs(t: DependentPositionTactic): DependentPositionTactic
Applies tatic
t
at all ODEs underneath this tactic's position. -
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
lazy val
chaseEulerAssignments: DependentPositionTactic
Chases remaining assignments.
- def chaseToTests(combineTests: Boolean): BuiltInPositionTactic
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
controllerMonitorByChase: BuiltInPositionTactic
Returns a tactic to derive a controller monitor in axiomatic style using forward chase.
Returns a tactic to derive a controller monitor in axiomatic style using forward chase. The tactic is designed to operate on input produced by createMonitorSpecificationConjecture.
- returns
The tactic.
- Definition Classes
- ModelPlex → ModelPlexTrait
|- xpost=1 ------------------------------controllerMonitorByChase(1) |- <{x:=1; {x'=2}}*>xpost=x
In order to produce the result above, the tactic performs intermediate steps as follows.
, |- xpost=1 ------------------------------true& |- (true & xpost=1) ------------------------------<:=> assign |- <x:=1;>(true & xpost=x) ------------------------------DX diamond differential skip |- <x:=1; {x'=2}>xpost=x ------------------------------<*> approx |- <{x:=1; {x'=2}}*>xpost=x
- See also
Examples: -
def
controllerMonitorT: DependentPositionTactic
Returns a backward tactic for deriving controller monitors.
Returns a backward tactic for deriving controller monitors.
- Definition Classes
- ModelPlex → ModelPlexTrait
-
def
createMonitorCorrectnessConjecture(vars: List[Variable], kind: Symbol, checkProvable: Option[(ProvableSig) ⇒ Unit], unobservable: ListMap[_ <: NamedSymbol, Option[Formula]]): (Formula) ⇒ Formula
Conjecture for double-checking a monitor formula for correctness: assumptions -> (monitor -> < prg; >Upsilon).
-
def
createMonitorSpecificationConjecture(fml: Formula, vars: List[Variable], unobservable: ListMap[_ <: NamedSymbol, Option[Formula]], postVar: (Variable) ⇒ Variable = NAMED_POST_VAR): ModelPlexConjecture
Construct ModelPlex monitor specification conjecture corresponding to given formula.
Construct ModelPlex monitor specification conjecture corresponding to given formula.
- fml
A formula of the form p -> [a]q, which was proven correct.
- vars
A list of variables V, superset of BV(a).
- unobservable
Unobservable variables/parameters and their optional estimation (e.g., from a sensor), keys subset of vars ++ any fns.
- returns
A tuple of monitor conjecture and assumptions
- Definition Classes
- ModelPlex → ModelPlexTrait
- See also
Mitsch, Platzer: ModelPlex (Definition 3, Lemma 4, Corollary 1).
-
def
createNonlinearModelApprox(name: String, tactic: BelleExpr, defs: Declaration): (Expression) ⇒ (Formula, BelleExpr)
Creates a model with the ODE approximated by the evolution domain and diff.
Creates a model with the ODE approximated by the evolution domain and diff. invariants from the
tactic
. Returns the adapted model and a tactic to proof safety from the original proof. -
def
createSandbox(name: String, tactic: BelleExpr, fallback: Option[Program], kind: Symbol, checkProvable: Option[(ProvableSig) ⇒ Unit], synthesizeProofs: Boolean, defs: Declaration, postVar: (Variable) ⇒ Variable = NAMED_POST_VAR): (Formula) ⇒ ((Formula, BelleExpr), List[(String, Formula, BelleExpr)])
Creates a sandbox safety conjecture from a formula of the shape init->[?bounds;{ctrl;plant}*]safe.
Creates a sandbox safety conjecture from a formula of the shape init->[?bounds;{ctrl;plant}*]safe. The sandbox embeds an (unverified) external controller in monitor checks of
kind
. It approximates the external controller behavior with nondeterministic values for each of the bound variables inctrl
. Input to the external controller is measured with nondeterministic values for each of the bound variables inplant
, but restricted to those satisfying the evolution domain constraints and invariants of the plant. If the monitor is satisfied, the external controller's decision are actuated. Otherwise (monitor unsatisfied)fallback
(if specified, ctrl by default) is executed.- tactic
The tactic used to prove safety of the original model.
- fallback
The fallback controller to embed in the sandbox,
ctrl
by default.- kind
The kind of monitor to derive (controller or model monitor).
- checkProvable
Whether or not to check the ModelPlex provable.
- returns
The sandbox formula with a tactic to prove it, and a list of lemmas used in the proof.
-
def
createSlidingMonitorSpec(fml: Formula, vars: List[Variable], unobservable: ListMap[_ <: NamedSymbol, Option[Formula]], windowSize: Int): (Formula, List[Formula])
Construct ModelPlex monitor specification conjecture corresponding to given formula for parameter estimation over a sliding window.
Construct ModelPlex monitor specification conjecture corresponding to given formula for parameter estimation over a sliding window.
- fml
A formula of the form p -> [a]q, which was proven correct.
- vars
A list of variables V, superset of BV(a).
- unobservable
Unobservable variables/parameters and their optional estimation (e.g., from a sensor), keys subset of vars, any fns.
- windowSize
Size of sliding window for parameter estimation.
- returns
A tuple of monitor conjecture and assumptions
-
def
curried: (List[Variable]) ⇒ (Symbol) ⇒ (Formula) ⇒ Formula
- Definition Classes
- Function2
- Annotations
- @unspecialized()
-
def
diamondDiffSolve2DT: DependentPositionTactic
Returns a tactic to solve two-dimensional differential equations.
Returns a tactic to solve two-dimensional differential equations. Introduces constant function symbols for variables that do not change in the ODE, before it hands over to the actual diff. solution tactic.
- returns
The tactic.
- Definition Classes
- ModelPlex → ModelPlexTrait
-
def
diamondTestRetainConditionT: DependentPositionTactic
Returns a modified test tactic for axiom <?H>p <-> H & (H->p)
Returns a modified test tactic for axiom <?H>p <-> H & (H->p)
- returns
The tactic.
- Definition Classes
- ModelPlex → ModelPlexTrait
|- x>0 & (x>0 -> [x'=x]x>0) ---------------------------diamondTestRetainCondition |- <?x>0>[x'=x]x>0
- Note
Unused so far, for deriving prediction monitors where DI is going to rely on knowledge from prior tests.
Example: -
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
eulerAllIn: DependentPositionTactic
Euler-approximates all atomic ODEs somewhere underneath pos
-
def
eulerSystemAllIn: DependentPositionTactic
Euler-approximates all ODEs somewhere underneath pos.
Euler-approximates all ODEs somewhere underneath pos. Systematic tactic, but not a proof.
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
flipUniversalEulerQuantifiers(fml: Formula): Formula
Unsound approximation step
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
locateT(tactics: List[AtPosition[_ <: BelleExpr]]): DependentPositionTactic
Performs a tactic from the list of tactics that is applicable somewhere underneath position p in sequent s, taking the outermost such sub-position of p.
Performs a tactic from the list of tactics that is applicable somewhere underneath position p in sequent s, taking the outermost such sub-position of p. Formulas only.
- tactics
The list of tactics.
- returns
The tactic.
- Definition Classes
- ModelPlex → ModelPlexTrait
|- a=1 & (<x:=2;>x+y>0 & <y:=3;>x+y>0) ---------------------------------------locateT(diamondSeqT :: diamondChoiceT :: Nil)(1) |- a=1 & <x:=2; ++ y:=3;>x+y>0
Example: -
lazy val
logger: Logger
- Attributes
- protected
- Definition Classes
- LazyLogging → LoggerHolder
-
final
val
loggerName: String
- Attributes
- protected
- Definition Classes
- LoggerHolder
- def modelMonitorByChase(ode: DependentPositionTactic): DependentPositionTactic
-
lazy val
modelMonitorByChase: DependentPositionTactic
Returns a tactic to derive a model monitor in axiomatic style using forward chase + diffSolve.
Returns a tactic to derive a model monitor in axiomatic style using forward chase + diffSolve. The tactic is designed to operate on input produced by createMonitorSpecificationConjecture.
- returns
The tactic.
-
def
modelMonitorT: DependentPositionTactic
Returns a backward tactic for deriving model monitors.
Returns a backward tactic for deriving model monitors.
- Definition Classes
- ModelPlex → ModelPlexTrait
-
def
modelplexAxiomaticStyle(unprog: DependentPositionTactic): DependentPositionTactic
ModelPlex backward proof tactic for axiomatic-style monitor synthesis, i.e., avoids proof branching as occuring in the sequent-style synthesis technique.
ModelPlex backward proof tactic for axiomatic-style monitor synthesis, i.e., avoids proof branching as occuring in the sequent-style synthesis technique. The tactic 'unprog' determines what kind of monitor (controller monitor, model monitor) to synthesize. Operates on monitor specification conjectures.
- unprog
A tactic for a specific monitor type (either controller monitor or model monitor).
- Definition Classes
- ModelPlex → ModelPlexTrait
- See also
-
def
modelplexSequentStyle: DependentPositionTactic
ModelPlex sequent-style synthesis technique, i.e., with branching so that the tactic can operate on top-level operators.
ModelPlex sequent-style synthesis technique, i.e., with branching so that the tactic can operate on top-level operators. Operates on monitor specification conjectures.
- returns
The tactic.
- Definition Classes
- ModelPlex → ModelPlexTrait
-
def
mxAbbreviateFunctions(fml: Formula, defs: Declaration): (Formula, USubst)
Abbreviates functions to nullary function symbols if all their arguments are free in
fml
, expand according todefs
the functions that have at least one if their arguments bound.Abbreviates functions to nullary function symbols if all their arguments are free in
fml
, expand according todefs
the functions that have at least one if their arguments bound. Returns the formula with abbreviated/expanded functions, and the substitutions telling which functions were expanded/abbreviated how. - def mxAutoInstantiate(assumptions: List[Formula], unobservable: List[_ <: NamedSymbol], simplifier: Option[BuiltInPositionTactic]): InputTactic
-
def
mxAutoInstantiate(assumptions: List[Formula]): InputTactic
- Annotations
- @Tactic( x$14 , x$15 , x$13 , x$16 , x$17 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )
-
def
mxFormatShape(shape: String): InputTactic
- Annotations
- @Tactic( x$26 , x$27 , x$25 , x$28 , x$29 , x$30 , x$31 , x$32 , x$33 , x$34 , x$35 , x$36 )
- def mxPartialQE(fmlAlts: List[Formula], defs: Declaration, tool: QETacticTool, verified: Boolean = true): ProvableSig
-
def
mxPartialQE(fml: Formula, defs: Declaration, tool: QETacticTool): ProvableSig
Partial QE on a formula that first expands/abbreviates all uninterpreted symbols and then substitutes back in on the result.
-
lazy val
mxSimplify: BuiltInPositionTactic
Simplifies reflexive comparisons and implications/conjunctions/disjunctions with true.
-
def
mxSynthesize(kind: String): InputTactic
- Annotations
- @Tactic( x$2 , x$3 , x$1 , x$4 , x$5 , x$6 , x$7 , x$8 , x$9 , x$10 , x$11 , x$12 )
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
normalizeInputFormula(f: Formula): Formula
Normalizes formula
f
into the shape A -> [a;]S. -
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
optimizationOneWithSearch(tool: Option[SimplificationTool], assumptions: List[Formula], unobservable: List[_ <: NamedSymbol], simplifier: Option[BuiltInPositionTactic], postVar: (Variable) ⇒ Variable = NAMED_POST_VAR): DependentPositionTactic
Opt.
Opt. 1 from Mitsch, Platzer: ModelPlex, i.e., instantiates existential quantifiers with an equal term phrased somewhere in the quantified formula.
- Definition Classes
- ModelPlex → ModelPlexTrait
|- xpost>0 & xpost=xpost ------------------------------optimizationOneWithSearch |- \exists x x>0 & xpost=x
Example: -
def
partitionUnobservable(unobservable: ListMap[_ <: NamedSymbol, Option[Formula]]): (ListMap[Variable, Option[Formula]], ListMap[(Function, Variable), Option[Formula]], ListMap[(Function, Variable), Option[Formula]])
Partitions the unobservable symbols into unobservable state variables and unknown model parameters.
- lazy val simplForall1: Lemma
- lazy val simplForall2: Lemma
-
def
stepwisePartialQE(fml: Formula, assumptions: List[Formula], defs: Declaration, tool: QETacticTool with SimplificationTool, preQE: (Formula, Int) ⇒ Unit = (_, _) => {}, postQE: (Formula, Int) ⇒ Unit = (_, _) => {}): ProvableSig
Splits into separate partial QE calls and merges results.
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toMetric(fml: Formula): Formula
Turns the formula
fml
into a single inequality. -
def
toString(): String
- Definition Classes
- Function2 → AnyRef → Any
-
def
tupled: ((List[Variable], Symbol)) ⇒ (Formula) ⇒ Formula
- Definition Classes
- Function2
- Annotations
- @unspecialized()
-
def
unrollLoop(n: Int): DependentPositionTactic
Unrolls diamond loops
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core
- KeYmaera X kernel, proof certificates, main data structuresExpression
- Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (one-pass) uniform substitutions and renaming.StaticSemantics
- Static semantics with free and bound variable analysisKeYmaeraXParser
.edu.cmu.cs.ls.keymaerax.parser
- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter
- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser
- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser
- Parser reading KeYmaera X model and proof archive.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.cmu.cs.ls.keymaerax.infrastruct
- Prover infrastructure outside the kernelUnificationMatch
- Unification algorithmRenUSubst
- Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context
- Representation for contexts of formulas in which they occur.Augmentors
- Augmenting formula and expression data structures with additional functionalityExpressionTraversal
- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon
- Bellerophon tactic language and tactic interpreterBelleExpr
- Tactic language expressionsSequentialInterpreter
- Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics
- Bellerophon tactic library for conducting proofs.TactixLibrary
- Main KeYmaera X tactic library including many proof tactics.HilbertCalculus
- Hilbert Calculus for differential dynamic logicSequentCalculus
- Sequent Calculus for propositional and first-order logicHybridProgramCalculus
- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
- Unification-based uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]
- Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma
- Lemma mechanismLemma
- Lemmas are Provables stored under a name, e.g., in files.LemmaDB
- Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe
- Real arithmetic back-end solversMathematicaQETool
- Mathematica interface for real arithmetic.Z3QETool
- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
- Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica
- Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3
- Z3 interface for real arithmetic including simplifiers.Entry Points
Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX
- Command-line launcher for KeYmaera X supports command-line argument-help
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.AxIndex
- Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex
- Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax
- Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos