Selected Presentations
A temporal approach to algebraic specifications
Yulin Feng1
and Junbo Liu1 
| (1) |
FB3 Mathematik und Informatik, Universität Bremen, Postfach 330 440, D-2800 Bremen 33, FR Germany |
Abstract
This paper is contributed to make connections between models for algebraic and temporal specifications. It brings a different viewpoint for classical algebras and algebraic specifications. Every algebra we concern here is finitely generated and associated with an implicit transition structure. The operators in the algebra may be partially defined. The class of algebras could be used as Kripke semantic models to interpret the temporals, so that we can do temporal reasoning about system behaviours such as safety and liveness properties. The unification of notions in algebraic and temporal specifications has many advantages for system developments. We may use a formal temporal deduction system to verify some dynamic properties from premises of algebraic specifications; or a temporal requirement specification may be used to develop systems in the style of top-down refinements. The notion of C-algebras has been crucial all along this work. In this paper we present the concepts, definitions and some basic theorems on C-algebras. Moreover, there exists a minimally defined algebra which is the initial one for each partially defined specification. The example of a lift controller is finally used to illustrate how to reason about the temporal behaviours of an algebraic specification.
This work is partly supported by the Commission of the European Communities under the ESPRIT Programme, Contract #390, PROSPECTRA Project.
On leave from University of Science & Technology of China, Hefei, Anhui 230026, China.
References secured to subscribers.