Skip past navigation NASA Langley Formal Methods


home

welcome

quick page

philosophy

team

research

quote

links

new?
  home > research > contract work

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

Note: The link to external site tag identifies links that are outside of the NASA domain.

 

  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 11 January 2002 (10:21:43)