Bibtex de la publication

@TechReport{ Ga2013.19,
author = {Garnacho, Manuel and Bodeveix, Jean-Paul and Filali, Mamoun},
title = "{Mechanized Semantics of Concurrent Systems with Priorities}",
year = {2013},
month = {juin},
type = {Rapport de recherche},
number = {Report--2013-16--FR},
institution = {IRIT},
address = {Université Paul Sabatier, Toulouse},
language = {anglais},
URL = {},
keywords = {Proof assistant, Mechanized Semantics, Transition Systems, Priority, Concur- rent Systems},
abstract = {Concurrent systems consist of many components which may execute in parallel and are complex to design and to implement. Component-based languages have been introduced to deal with such issues. However concurrency introduces phenomena not present in sequential systems such as deadlock, starvation and fairness. Introducing priorities in those languages is a solution to control such phenomena. In order to prove properties of such languages as well as of behaviors of systems modeled thanks to them, one needs to formalize their semantics. We introduce a formal semantic model based on transitions systems that enables to specify concurrent systems with priority constraints. Then we define an internal composition operator together with priority constraints and establish its compositionality. We have also defined a port hiding function in order to close these models and we have proven its soundness. Another substantial contribution of this paper is that all our definitions and proofs have been mechanized in the COQ proof assistant. Furthermore, our framework provides a very expressive proof environment to deal with problems about both component-based languages and system specifications expressed within those.}