Sphinx is an extensible verification-driven engineering toolkit based on the Eclipse platform. It provides textual and graphical modeling editors to describe the structure, the discrete dynamics, and the continuous dynamics of cyber-physical systems. Sphinx uses KeYmaera as hybrid verification tool.
Sphinx supports four configuration elements: textual modeling, graphical modeling, proof inspection, and simulation. Not all of the third-party plugins are required, depending on the chosen configuration. Those are marked below.
Nowadays, robots interact more frequently with a dynamic environment outside
limited manufacturing sites and in close proximity with humans. Thus, safety of
motion and obstacle avoidance are vital safety features of such robots. We formally
study two safety properties of avoiding both stationary and moving obstacles:
(i) passive safety, which ensures that no collisions can happen while the robot
moves, and (ii) the stronger passive friendly safety in which the robot further
maintains sufficient maneuvering distance for obstacles to avoid collision as
well. We use hybrid system models and theorem proving techniques that describe and
formally verify the robot’s discrete control decisions along with its continuous,
physical motion. Moreover, we formally prove that safety can still be guaranteed
despite location and actuator uncertainty.
[ Paper | Sphinx Project ]
We study how CPS technology can help improve freeway traffic by combining local
car GPS positioning, traffic center control decisions, and communication to
achieve more tightly coupled feedback control in intelligent speed adaptation.
We develop models for an intelligent speed adaptation that respects variable speed
limit control and incident management. We identify safe ranges for crucial design
parameters in these systems and, using the theorem prover KeYmaera, formally
verify safety of the resulting CPS models. Finally, we show how those parameter
ranges can be used to decide trade-offs for practical system implementations even
for design parameters that are not modeled formally.
[ Paper | Sphinx Project ]
KeYmaera X is a theorem prover for specifying and verifying correctness properties of hybrid systems (systems that mix discrete and continuous dynamics). KeYmaera X implements differential dynamic logic and provides a high degree of control over automated proof search. KeYmaera X features a minimal core that isolates soundness-critical axiomatic reasoning. Tactics built on top of this core drive automated proof search, and a modern web-based front-end provides a clean interface for both interactive and automated proving.