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.