Fork Algebra as a Formalism to Reason Across Behavioral Specifications

FRIAS, MARCELO FABIÁN; GALEOTTI, JUAN PABLO; LOPEZ POMBO, CARLOS GUSTAVO; ROMAN, MARIO

St. Catharine, Ontario, Canada

Conferencia; 8th. Conference on Relational Methods in Computer Science (RelMiCS) - 3nd. International Workshop on Applications of Kleene Algebra; 2005

Brock University

Describing systems through the specification of different views is a well accepted practice in modern software engineering. In this paper we show how to reason across behavioral specifications within a relational framework. We consider views specifying behavioral information using linear temporal logic or dynamic logic. The main result is that independently generated specifications can be amalgamated within a common relational framework to which different analysis techniques can be applied. The paper also presents a realistic problem for which  behavioral specifications in dyamic logic and linear temporal logic are jointly employed in the proof of a non trivial property.