Specification-Based Testing of a Concurrent Software System: An Experience Report

Future systems for analyzing, debugging and testing concurrent programs will rely heavily on automated reasoning processes such as automatic runtime consistency checking. This paper reports experience with the use of high-level, event-based formal specifications and automatic runtime consistency checking to test the correctness of a large concurrent software system, a Distributed Tasking Supervisor for the Ada programming language. The Supervisor is a virtually complete implementation of Ada tasking that executes Ada programs in parallel on a shared memory multiprocessor.