Specifying concurrent systems with TSL

Author

Rosenblum, David S.

Author_Institution

AT&T Bell Lab., Murray Hill, NJ, USA

Volume

8

Issue

3

fYear

1991

fDate

5/1/1991 12:00:00 AM

Firstpage

52

Lastpage

61

Abstract

The Task Sequencing Language (TSL), which lets programmers specify constraints on the behavior of concurrent programs, is described. The constraints, specified by high-level annotations to Ada programs, are monitored at runtime; when a violation is detected, control is returned to the user, along with information about the nature of the violation. It is argued that such a tool is a necessary crutch for human reasoning capabilities when dealing with the complexities of concurrent process interaction. The first large-scale application of TSL, the specification and validation of a distributed tasking supervisor for Ada, is described.<>

Keywords

Ada; parallel programming; program verification; specification languages; system recovery; Ada programs; TSL; Task Sequencing Language; concurrent process interaction; concurrent programs; distributed tasking supervisor; high-level annotations; human reasoning capabilities; large-scale application; specification; validation; violation; Animation; Computer errors; Concurrent computing; Debugging; Humans; Information analysis; Instruments; Software tools; System recovery;

fLanguage

English

Journal_Title

Software, IEEE

Publisher

ieee

ISSN

0740-7459

Type

jour

DOI

10.1109/52.88944

Filename

88944