Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Selected Presentations

A temporal approach to algebraic specifications

Yulin FengContact Information and Junbo LiuContact Information

(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.

Contact Information Yulin Feng
Email: @feng%informatik.uni-bremen.de

Contact Information Junbo Liu
Email: @liu%informatik.uni-bremen.de
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.111 • Server: mpweb06
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)