Refinement and verification applied to an in-flight Data acquisition unit
Wan J. Fokkink, Natalia Ioustinova, E. Kesseler, Jaco van de Pol, Yaroslav S. Usenko, Yuri Yushtein · 2002
In order to optimise maintenance and increase safety, the Royal Netherlands Navy initiated the development of a multi-channel on-board data acquisition system for its Lynx helicopters. This AIDA (Automatic In-ight Data Acquisition) system records usage and loads data on main rotor, engines and airframe. We used refinement in combination with model checking to arrive at a formally verified prototype implementation of the AIDA system, starting from the functional requirements.