Specifications of distributed systems in prolog

Abstract

A specification in Prolog coded as a collection of Horn clauses is a system description specifying externally observable system behavior. These system descriptions can be executed for both generating and recognizing possible sequences of valid externally observable system interactions. Thus, they aid in the dynamic analysis of the system functionality captured by subsequent designs and implementations of the specified systems. This paper proposes a comprehensive structure for Prolog-based specifications which supports descriptions of system functionality at various levels of abstraction. The paper also discusses how these executable descriptions are used for validation purposes. © 1990.