Using the Vienna Development Method (VDM) to Formalize a Communication Protocol

摘要

The purpose of this document is to serve as an introduction to certain specification techniques and the specification computer language (Meta-IV) of the Vienna Development Method (VDM) and to further extend the use of VDM by applying it within a new domain. VDM has been applied to the specification of a communication protocol. The protocol is one used for the communication between an inertial navigation system (INS) and an external computer (EC). This protocol was chosen because it is a new application area for VDM, and it is an integral part of an existing project at the SEI. The Real-Time Embedded Systems Testbed (REST) Project is implementing the protocol as part of an INS simulator system that is being developed to investigate the use of Ada for embedded systems. Keywords: Inertial navigation, Algorithms, Software. (jes)