SAT-based model checking of train control systems
Markus Roggenbach · 2009
Formal verification of railway control software has been identified to be one of the “grand challenges” [7] of Computer Science. Various formal methods have been applied to this area, including algebraic specification, e.g. [3], process algebraic modelling and verification, e.g. [14], and also model oriented specification, where e.g. the B method has been used in order to verify part of the Paris Metro railway [4]. In partnership with Invensys, an internationally established company specialised in railway control systems, we explore various verification approaches based on SAT solving [2].