SCS Undergraduate Thesis Topics
|Meera Sridhar||The Honeywell Triplex Sensor Voter||Jeannette Wing|
The Honeywell Sensor Voter Project involves formally verifying desired properties of the Triplex Sensor Voter, a real-time flight control device made by Honewell Inc. Honeywell Inc. was interested in verifying certain safety properties of this device. In order to do this, they had previously used random testing and simulation and other traditional verification mechanisms. Although these approaches provide examples of scenarios in which the system's safety properties hold, they do not guarantee that the safety properties hold in a sufficiently comprehensive set of scenarios. In our case study we explore the use of model checking, a formal verification mechanism, to provide this guarantee. Apart from providing such a reliable means of verification, the process of model checking also aided in refining and disambiguating the Triplex Sensor Voter's underlying algorithm. Our case study also demonstrates adapting model checking, a tool built for discrete systems, to verify properties for a real-time system. Although previous work has been done in this area, we are the first to verify these properties using Symbolic Model Verifier and only the model checking structures defined in "Clark, Grumberg, Peled. Model Checking. MIT Press, Cambridge Massachusetts ©2001."