Author: Jasper Nygaard and Rasmus Sørensen


This VDM-RT model was produced as a part of an MSn thesis investigating and analyzing
the possibility of obtaining early stage validation of potential candidate system 
architectures, by means of formal modelling and validation. The goal was to analyze 
recent research extensions of VDM++ for describing and analyzing such distributed 
systems (VDM-RT) and see if the language is suitable to stress test a distributed 
system and validate any architectural benefits. Additionally this thesis discusses
favorable approaches for realizing a case study of a transportation system in Tokyo, 
referred to as CyberRail. Different VDM++ models of candidate architectures for the 
CyberRail system has been developed and validated. This thesis includes 2 Real-Time 
VDM++ models (Backend Responsibility source, Joint Responsibility source), based 
on 2 different architectures. 

Language Version: vdm10
Entry point     : new World("test1_10.txt").run()
Entry point     : new World("test2.txt").run()