Temporal specification of Ada tasks

The authors report work on a language called Ada/TL for the specification of the temporal behavior of interacting Ada tasks in both concurrent and distributed systems. Ada/TL is an extension of the task-specification declarations required by Ada. The extensions include temporal assertions about rendezvous and other events of external interactions and nontemporal in and out assertions about parameters and other data items that flow between tasks. Linear-time operators are used to specify the sequential behavior of individual tasks and branching-time operators to specify global properties about the interaction of tasks. It is intended that task specifications follow the style of Ada declarations and be constructive inasmuch as they lead directly to the design of task-rendezvous behavior. The authors describe the representation of an externally viewable state of an Ada task and define operators to specify a task behavior as a sequence of state conditions. Specifications are illustrated for examples of tasks using shared resources and interaction using both synchronous and asynchronous communication. Specification of timing constraints and analysis of gloval correctness of specifications are discussed