An extended linear tense propositional logic is presented for the
specification and verification of the behavior of very dynamic information
systems. The temporal evolution of a system is described with causal
rules specifying trigger/reaction relationships between events.
Besides the presentation of the language, semantics and axiomatization
of the proposed triggering logic, a practical proof system is outlined
which provides effective tools for proving both safety and liveness
properties of the specified systems. Its usefulness is illustrated
by proving several properties of a system using semaphores. The
relationship between the event structure and the tense structure
of the logic is also discussed. The proposed logic is an important
fragment of the INFOLOG calculus that is being developed for information
systems design.
%0 Journal Article
%1 fiadeiro86
%A Fiadeiro, Jose
%A Sernadas, Amilcar
%D 1986
%J Information Systems
%K logic formal model requirements temporal
%N 1
%P 61--85
%R 10.1016/0306-4379(86)90023-2
%T The INFOLOG linear tense propositional logic of events and transactions
%U http://www.sciencedirect.com/science/article/B6V0G-48TD1TG-99/2/c69c52733788dbb64dd73e7cc147d7fe
%V 11
%X An extended linear tense propositional logic is presented for the
specification and verification of the behavior of very dynamic information
systems. The temporal evolution of a system is described with causal
rules specifying trigger/reaction relationships between events.
Besides the presentation of the language, semantics and axiomatization
of the proposed triggering logic, a practical proof system is outlined
which provides effective tools for proving both safety and liveness
properties of the specified systems. Its usefulness is illustrated
by proving several properties of a system using semaphores. The
relationship between the event structure and the tense structure
of the logic is also discussed. The proposed logic is an important
fragment of the INFOLOG calculus that is being developed for information
systems design.
@article{fiadeiro86,
abstract = {An extended linear tense propositional logic is presented for the
specification and verification of the behavior of very dynamic information
systems. The temporal evolution of a system is described with causal
rules specifying trigger/reaction relationships between events.
Besides the presentation of the language, semantics and axiomatization
of the proposed triggering logic, a practical proof system is outlined
which provides effective tools for proving both safety and liveness
properties of the specified systems. Its usefulness is illustrated
by proving several properties of a system using semaphores. The
relationship between the event structure and the tense structure
of the logic is also discussed. The proposed logic is an important
fragment of the INFOLOG calculus that is being developed for information
systems design.},
added-at = {2006-09-18T06:26:07.000+0200},
author = {Fiadeiro, Jose and Sernadas, Amilcar},
biburl = {https://www.bibsonomy.org/bibtex/2a3661d21391bc3275095b774ba45b85a/neilernst},
citeulike-article-id = {738339},
description = {Not previously uploaded},
doi = {10.1016/0306-4379(86)90023-2},
interhash = {8e4b5751f77faa3ba9eacacae6644177},
intrahash = {a3661d21391bc3275095b774ba45b85a},
journal = {Information Systems},
keywords = {logic formal model requirements temporal},
number = 1,
pages = {61--85},
priority = {2},
timestamp = {2006-09-18T06:26:07.000+0200},
title = {The INFOLOG linear tense propositional logic of events and transactions},
url = {http://www.sciencedirect.com/science/article/B6V0G-48TD1TG-99/2/c69c52733788dbb64dd73e7cc147d7fe},
volume = 11,
year = 1986
}