Our approach—try it!
Applied model checking to the specification of TCAS II
- Traffic Alert and Collision Avoidance system
- In use on U.S. commercial aircraft
- FAA adopted specification
- Initial design and development by Leveson
Translation process (RSML to SMV)
Model checking (dealing with BDD’s)
Analyzing TCAS properties