Local Causal Reasoning of a Safety-Critical Subway System

Translating an informal design intent into a formal specification is an error prone process. A designer may be able to claim that his implementation meets his formal specification. But, in many cases, he cannot confidently claim that his formal specification correctly captures the original design intent. This problem, in our views, is due to global causal reasoning, as we show with LUSTRE for a Subway system. To resolve this lack of confidence, we briefly present our interactive design tool, which forces a designer to reason locally while formally specifying the design intent.