A REFINEMENT BASED APPROACH TO CALCULATING A FAULT-TOLERANT RAILWAY SIGNAL DEVICE

摘要

In this extended abstract, we present a technique whereby a new, fail-safe and fault-tolerant architecture for an existing device is calculated, and verified, from an existing abstract specification. The inspiration for the architecture draws from the Byzantine Generals problem. The model is presented in Hoare's CSP, safety properties are proved using the model checker FDR, and development is guided by the laws of Circus. The case study is Montigel's Dwarf Signal.