|Title||A Linear Temporal Logic Approach to Objects with Transactions|
|Publication Type||Conference Proceedings|
|Year of Conference||1997|
|Authors||Denker, G., J. Ramos, C. Caleiro, and A. Sernadas|
|Conference Name||Sixth Int1 Conf1 on Algebraic Methodology and Software Technology, AMAST'97, 13-17 December 1997, Sydney, Australia|
Our concern is the high level specification of reactive software systems such as information systems. We adopt an object oriented, temporal logic based approach to specification. The notion of transaction incorporates various application domains, for instance transactions as abstractions from processes as known from refinement theory, transactions as abstractions from business processes as known in business process modelling or database transactions. In this paper we investigate object specifications with transactions. We illustrate the use of transactions by examples given in an object oriented style and introduce a linear temporal logic with transactions (\tosl) which serves as denotional model for such object specifications with transactions. We explain how \tos1 is semantically defined in terms of life cycles and illustrate by example the translation of object specifications to \tosl. Using \tos1 for system specification results in sets of formulae which are independent from the level of granularity.