AIDA (Automatic In-Flight Data Acquisition) System.

Organisation:	National Aerospace Laboratory and CWI (THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language)
Tools used:	B-Toolkit muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Systems.
Period:	2002
Size:	approximately 250,000 states and 900,000 transitions
Description:	AIDA (Automatic In-flight Data Acquisition) is a multi-channel on-board data acquisition system developed by the Royal Netherlands Navy in order to facilitate the maintenance and increase the safety of its Lynx helicopters. The AIDA system records usage and loads data on main rotor, engines, and airframe. It gathers input data from 15 analog and 2 discrete signals produced by several measurement and control devices. The system runs 39 different tasks responsible for data storage, conditioning and processing, and performs several logging tasks simultaneously (e.g., writing data acquisition files, producing audio and video signals, etc.). There are four different groups of tasks: data reduction tasks, which monitor and process signals using standard algorithms, with subsequent storage of data into memory; level crossing detection tasks, which monitor signals to check whether a predefined level is crossed upwards or downwards; event count and event duration tasks, which provide signal monitoring, count the number of times that a signal reaches a certain predefined level, and determine the time span that the signal is at this predefined level; system integrity tasks, which verify the status of the AIDA recorder and check whether a predefined malfunctioning condition is met. In a project funded by the Royal Netherlands Navy, the National Aerospace Laboratory (NRL) in collaboration with CWI developed a formally verified implementation of the AIDA system starting from the functional requirements. The approach used was a combination of refinement and model-checking methods. Refinement was carried out using the B method and the B-Toolkit. Verification of progress properties (which cannot be shown only by refinement) was carried out by model-checking using the CADP and muCRL toolsets. To perform refinement, an abstract B model of the AIDA system was developed starting from the AIDA functional requirements, and was validated using the B-Toolkit by animation and proof of internal consistency obligations. Several selected components of the system were further refined and proved to be correct w.r.t. the abstract model. At the end, executable specifications (implementations) were obtained and tested against a general environment which produces chaotic combinations of input signals. To verify progress properties, different components of the AIDA system (tasks, sensors, buttons, data acquisition file, output channels, and environment) were specified in muCRL. This allowed to detect and correct several specification errors. The state space of the muCRL description was generated using the muCRL toolset and checked to be deadlock free (using the muCRL toolset) and livelock free (using the CADP toolset). For each task, two correctness requirements were formulated in regular alternation-free mu-calculus and verified using the EVALUATOR 3.0 model-checker of CADP. This allowed to detect and correct a spurious logging error due to an ambiguity in the informal requirements of the AIDA system.
Conclusions:	This case-study demonstrated that the combination of refinement methods (such as the B method and B-Toolkit) and verification methods (such as muCRL and the CADP toolbox) can be successfully applied in the development of naval equipment. Also, the joint use of the muCRL and CADP toolsets turns out to be very effective for a completely automated verification of functional properties.
Publications:	[Fokkink-Ioustinova-Kesseler-vdPol-Usenko-Yushtein-02] Wan Fokkink, Natalia Ioustinova, Ernst Kesseler, Jaco van de Pol, Yaroslav S. Usenko, and Yuri A. Yushtein. "Refinement and Verification Applied to an In-Flight Data Acquisition Unit". Proceedings of the 13th Conference on Concurrency Theory CONCUR'2002 (Brno, Czech Republic), Lecture Notes in Computer Science vol. 2421, pp. 1-23, August 2002. Available on-line at: http://www.cwi.nl/~wan/WJFmore/ktvfm.ps.gz or from the CADP Web site in PDF or PostScript
Contact:	Dr. Wan Fokkink CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam, The Netherlands Room: M342 Tel: +31 20 592 4104 Fax: +31 20 592 4199 E-mail: wan@cwi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page