Abstract:
We consider the question of composition in system design, a
fundamental issue in engineering. More precisely, we are interested
in deducing system properties from components properties and
vice-versa. This requires system and component specifications to be
"compositional" in some sense. Depending on what systems
are and how they are composed, this problem is satisfactorily solved
(e.g., sequential composition of terminating programs) or remains a
hot research topic (e.g., concurrent composition of reactive systems).
In this paper, we aim at providing a logical framework in which
composition issues can be reasoned about independently from the kind of
systems and the laws of composition under consideration. We show that
many composition related statements can be expressed in terms of
predicate transformers in a way that presents interesting similarities
with program semantics descriptions based on weakest precondition
calculus.
Michel Charpentier <
>
Last modified: Mon May 5 17:22:04 EDT 2003