SRI Matlab Project

Motivation

• Traditional control methodologies apply to individual controllers
• Traditional formal methods just looks at the discrete logic
• Control methodologies do not handle complex logic so do not provide satisfactory performance
• Formal verification of safety cannot be done independent of continuous mathematics

Goal

• Given a hybrid system (above) and a safety property (rigorously expressed)
• mathematically explore entire state-space (discrete × continuous) and show safety property is true

Approach

• Automatically apply hybrid abstraction
  • find points where functions of continuous variables change signs
  • partitions continuous n-space into finite number of regions with similar behavior
  • model check combination of discrete logic and the partitioned continuous space
• Avoid hard quantifier elimination problems
• Go beyond decidability limits
• Guarantee soundness
• Keep techniques compositional

Papers

• Gregoire Hamon, John Rushby, An Operational Semantics for Stateflow
• Ashish Tiwari, N. Shankar, and John Rushby, Invisible Formal Methods for EmbeddedControl Systems

Note: The tag identifies links that are outside of the NASA domain.