Specifying Objects of Concurrent Systems

Formal specification can play an important role in the design, development, and maintenance of concurrent systems. However, existing languages for specifying concurrent systems lack the same maturity as those for sequential programs. In this dissertation, we define a formal language, the Generic Concurrent Interface Language (GCIL), that supports modularization and abstraction in the specification of a class of concurrent systems. Our goal is to define a language that is useful to designers and programmers, who may have limited experience with formal methods. A striking feature of GCIL is its focus on data rather than processes. A GCIL specification describes the objects with which the concurrent processes interact, rather than the processes themselves. Each object specification is independent and can be considered individually. GCIL is an extension of one of the languages of Larch, a family of languages for specifying the modules, including abstract data types, that constitute a seque..