Simple Railroad Controller: A Case Study in Real-Time Specification Using MOSCA

摘要

MOSCA is an experimental language that extends the Vienna Development Method(VDM) specification language VDM-SL to be applicable in the area of developing distributed, parallel and real-time systems. As is generally known, plain VDM is not adequate for these application area's since it lacks facilities to specify multiple threads of control and it does not allow the use of time within specifications. MOSCA is designed to overcome these restrictions. This report presents an overview of some of the process specification capabilities of MOSCA. It demonstrates these capabilities in particular by application in a real case project, the specification of a simple railroad controller.