Testing the correctness of tasking supervisors with TSL specifications

ABSTRACT

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. We have tested a distributed tasking supervisor for the Ada programming language by monitoring the execution behavior of Ada tasking programs that have been compiled and linked with the supervisor. This behavior is checked for consistency with an event-based formalization of the Ada tasking semantics expressed in the TSL specification language. The TSL Runtime System automatically performs all monitoring and consistency checking at runtime. Our approach improves upon other approaches to testing tasking supervisors, particularly the Ada Compiler Validation Capability (ACVC), and also an approach described by Klarund. In contrast with these other approaches, in our approach (1) we test only the behavior of the tasking supervisor, not the behavior of the test programs; and (2) any Ada tasking program may be employed as test data, because the TSL specifications we construct describe the semantics of Ada language statements, not the semantics of application programs.

REFERENCES

• Ada83: US Department of Defense, US Government Printing Office. The Ada Programming Language Reference Manual, February 1983. ANSI/MIL-STD-1815A-1983.
• Ada87: Ada Joint Program Office. Ada validation procedures and guidelines. Ada Letters, 7(2):29-57, March-April 1987.
• HL83: D. Helmbold , David C. Luckham, Runtime and description of deadness errors in ADA tasking, Stanford University, Stanford, CA, 1983
• HL85a: David P. Helmbold and David C. Luckham. Debugging Ada tasking programs. IEEE Software, 2(2):47-57, March 1985.
• HL85b: David Helmbold , David Luckham, TSL: task sequencing language, Proceedings of the 1985 annual ACM SIGAda international conference on Ada, p.255-274, May 14-16, 1985, Paris, France
• Kla85: Nils Klarund. Formal concepts for specification and automatic testing of Ada tasks. Technical report, DDC International A/S, 1985.
• LHM+87: David C. Luckham , D. P. Helmbold , S. Meldal , D. L. Bryan , M. A. Haberler, Task sequencing language for specifying distributed Ada systems, Proc. of the CRAI Workshop on Software Factories and Ada on System development and Ada, p.249-305, January 1987, Capri, Italy
• Ros85: David S. Rosenblum. A methodology for the design of Ada transformation tools in a DI- ANA environment. IEEE Software, 2(2):24- 33, March 1985.
• Ros87: David S. Rosenblum. An efficient communication kernel for distributed Ada runtime tasking supervisors. Ada Letters, 7(2):102- 117, March-April 1987.
• Ros88: David Samuel Rosenblum , David C. Luckham, Design and verification of distributed tasking supervisors for concurrent programming languages, 1988

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Debugging aids
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Ada

General Terms:
Languages, Verification