Product-Based Safety Verification Using Formal Methods
Sofia K. Georgiadis · 2014
How could the safety of a system be proven? Is it possible to apply the rigor of mathematical proofs to large, complex software systems? This paper addresses these questions through a presentation of the use of the Event-B [1] language to prove the safety of the New York City Transit (NYCT) Communications-Based Train Control (CBTC) systems.