Formal verification methods are making headway into required safety verification policies for transportation. However, they often fail to account for the fact that controllers, whether digital or human, have imperfect knowledge of the world. Without addressing this shortcoming, we risk never bridging the gap between theoretical and practical safety.
In this talk, we discuss the sometimes fatal consequences of these shortcomings, and describe a new logic with belief as a first-class citizen, allowing us to model, think and verify belief-aware cyber physical systems.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.