Local Specification of Distributed Families of Sequential Objects

TitleLocal Specification of Distributed Families of Sequential Objects
Publication TypeConference Paper
Year of Publication1995
AuthorsEhrich, H. - D., and A. Sernadas
Conference NameRecent Trends in Data Types Specification, Proc1 10th Workshop on Specification of Abstract Data Types joint with the 5th COMPASS Workshop, S.Margherita, Italy, May/June 1994, Selected papers
PublisherSpringer, Berlin, LNCS 906

Fully concurrent models of distributed object systems are specified using linear temporal logic that does not per se cope with concurrency. This is achieved by employing the principle of local sequentiality: we specify from local viewpoints assuming that there is no intra-object concurrency but full inter-object concurrency. Local formulae are labelled by identity terms. For interaction, objects may refer to actions of other objects, e.g., calling them to happen synchronously. A locality predicate allows for making local statements about other objects.

1995LocSpecDistr.pdf350.23 KB