Testing the Correctness of Tasking Supervisors with TSL Specifications

This paper describes the application of behavior specifications to the testing of tasking supervisors, an important component of an implementation of a concurrent programming language. The goal of such testing is to determine whether or not a tasking supervisor correctly implements the semantics of its associated language. In particular, we test our distributed tasking supervisor for the Ada programming language by monitoring the execution behavior of Ada tasking programs that have been compiled to execute with the supervisor. The behavior is checked for consistency with an event-based formalization of the Ada tasking semantics expressed in the TSL (Task Sequencing Language) specification language; the TSL Runtime System automatically performs the execution monitoring and consistency checking. Our approach improves upon other approaches to testing and validating tasking supervisors, particularly the Ada Compiler Validation Capability (ACVC) and an approach described by Klarund.