 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| • |
Applied
model checking to the specification of TCAS II
|
|
|
|
– |
Traffic
Alert and Collision Avoidance System
|
|
|
|
• |
In
use on U.S. commercial aircraft
|
|
|
|
• |
http://www.faa.gov/and/and600/and620/newtcas.htm
|
|
|
|
– |
FAA
adopted specification
|
|
|
|
– |
Initial
design and development by Leveson et al.
|
|
|
| • |
Later
applied it to a statecharts description of an electrical
|
|
power
distribution system model of the B777
|
|
|
| • |
The
vast bulk of this work was due to William Chan
|
|
|
|
– |
Along
with Mike Ernst won honorable mention in the 2000 ACM
|
|
Dissertation
Award competition
|
|
|
|
– |
Died
in a tragic automobile accident a week after defending his
|
|
|
dissertation
|
|