Proving specifications of tasking systems using Ada/TL
James Francis Peters, William J. Hankley · 1990
ADA/TL is a language for specification of the behavior of systems of communicating tasks. It merges concepts of the specification part of ADA, VDM specification of packages, and temporal logic specification of task behavior. The TL part consists of constructive specification of behaviors of individual tasks and a system specification of the properties of the interaction of tasks. A proof of a system specification consists of showing that the system property holds over all possible interleavings of the task behaviors.