Sphinx Get the user manual

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.

Features

Installation

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.

  1. Install Eclipse Modeling (Kepler)
  2. Start Eclipse
  3. Click Help → Install Modeling Components → Select Xtext and Papyrus and Click Finish
  4. Click Help → Install new Software...
  5. Add the Sphinx update site: http://www.cs.cmu.edu/~smitsch/updates/releases
  6. Add the XSemantics update site: http://master.dl.sourceforge.net/project/xsemantics/updates/releases/1.3
  7. For proof inspection: Add the EMF Compare update site: http://download.eclipse.org/modeling/emf/compare/updates/releases
  8. For simulation: Add the Wolfram Workbench update site: http://workbench.wolfram.com/update/
    Note: Wolfram Workbench requires a valid Mathematica license.
  9. For simulation: Add the Eclipse Indigo compatibility update site: http://download.eclipse.org/releases/indigo
  10. Select Sphinx from the drop-down menu and choose the features to install. If no features are displayed: untick "Group items by category"
  11. Follow the screen instructions to complete the installation

Case Study: Provably Safe Robotic Obstacle Avoidance

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 ]

Case Study: Road Traffic Control

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 Download

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.