| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL P/dml100-186/ Datei vom 4.1.2008 mit Größe 10 kB |
|
Quelle README.txt Sprache: Text |
|||||||||
|
Author: Niels Kirkegaard
This example describes a VDM++ specification of a KLV system. The purpose of the KLV system is to provide a continuous monitoring of the speed of a train. The VDM++ specification is inspired by a KLV description provided to the EP26538 FMERail project as case study by Atelier B. This model shows an example of how an informal description can be translated into a precise model that together with a graphical front-end can be used to ensure that the customer and the developer have a common interpretation of the system under development. The focus of the model is on the logic of the KLV systems when a train meets speed restriction beacons along the tracks, i.e. on events that triggers the KLV system. Issues such as how to determine whether a beacon has been met within a certain distance calculated from speed has been abstracted in away in the current model. They could be issues to extend the model with. Language Version: vdm10 ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28