The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Modal I/O automata (MIOs) by Larsen et al. provide a flexible framework for the specification and implementation of interacting systems. They distinguish between "may" transitions and "must" transitions, where the former can be disregarded and the latter must be respected by any correct refinement. Building on the theory of MIOs we introduce a new compatibility notion, called weak modal compatibility, for interacting components. As an important property of behavioural interface theories we prove that weak modal compatibility is preserved under weak modal refinement. Then we extend the notion of weak modal compatibility to loosely coupled systems which interact via buffered FIFO channels. We show that also in this case weak compatibility is preserved by weak modal refinement and that, moreover, local refinements compose to global refinements. Finally, we describe the MIO Workbench, an Eclipse-based editor and verification tool for modal I/O automata.