|
Electronic
Systems Design Seminar
|
|
Component-Based Construction of Deadlock-Free Systems
|
We propose a
framework for building deadlock-free systems from deadlock-free
components. The framework is based on a methodology for the layered
construction of systems by superposing three layers. A layer of
components, an
interaction model and a restriction layer. The interaction model
specifies the
possible interactions between components. The restriction layer
restricts the
behavior of the two lower layers by a global constraint. Layered
structuring
allows separating three orthogonal aspects in system construction.
Apart from
its methodological interest it makes technically possible the
definition of a unique and very powerful associative composition
operator.
We study sufficient
deadlock-freedom conditions for systems built from
deadlock-free components and given interaction model and
restriction. We also
provide a sufficient condition for individual deadlock-freedom of the
components of such systems.
Joseph Sifakis is a
CNRS Researcher and Director of the Verimag laboratory, Grenoble,
France. He worked on both theoretical and practical aspects
of concurrent systems specification and verification. He contributed to
the development of verification methods and tools by model-checking for
untimed and timed systems. His current research work aims at developing
methods for modeling real-time systems with emphasis on composability
and compositionality techniques.