Applying Model Checking to Large Software Specifications
Embedded systems
Problems
Reactive systems
Key question
Symbolic model checking
Software model checking
Why might model checking fail?
Our approach—try it!
Outline
PPT Slide
Sample transitions
Events
Properties to check: examples
TCAS
TCAS specification
TCAS—high-level structure
Model checking
Binary decision diagrams (BDDs)
Using SMV
Iterative process
Use of non-determinism
Translating RSML to SMV
State encoding
Synchrony hypothesis
Transitions
Non-deterministic transitions
Checking properties
Property checking
Disclaimer
Deterministic transitions
Tradeoffs
Function consistency
Display_Model_Goal
Output agreement
Output agreement check
Where may formulae come from?
Performance results
Discussion
Model checking software
Email: notkin@cs.washington.edu
Home Page: http://www.cs.washington.edu/homes/notkin