The railway modeling work has produced modeling methods powerful enough to prove safety of the conventional block control system. We hope to apply it to newer systems for which safety is more problematic.
The VFRAME++ work centers around correctness of translation from graphical representations of circuits to hardware implementing them. Work so far carried out consists of design verification of a translation algorithm in PVS. Currently planned is an a posteriori checker to show that a particular translation has been done correctly. Such a checker would have the advantage of being simple and stand-alone, hence easy to demonstrate to be correct.