A system-based approach to the formal development of embedded controllers for a railway

摘要

We describe a formal approach to the development of embedded controllers for a railway. The approach Starts with a system-level specification modeling the system under control and the desired control behavior. Correctness-preserving refinement it then used to add more and more implementation detail to the models and to decompose the models into sub-systems to arrive at models of individual controllers. The B Method is used as the formal notation and methodology.