Task sequencing language for specifying distributed Ada systems TSL-1

Abstract

TSL-1 is a language for specifying sequences of tasking events occuring in the execution of distributed Ada1 programs. TSL-1 specifications are included in an Ada program as formal comments. They express constraints to be satisfied by the sequences of actual tasking events that can occur. An Ada program is consistent with its TSL-1 specifications if its runtime behavior satisfies them. This paper presents an overview of TSL-1. The features of the language are described informally, and examples illustrating the use of TSL-1, both for debugging and for specification of tasking programs, are given. Some important constructs, as well as topics related to uncertainty of observation of distributed programs, are dealt with in other papers. In the future, constructs for defining abstract units will be added to TSL-1, forming a new language TSL-2 for the specification of distributed systems prior to their implementation in any programming language.