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.
This work addresses the problem of detecting and
resolving conflicts due to timing constraints imposed by features
in real-time systems. We consider systems composed of a base
system with multiple "features" or "controllers",
each of which independently advises the system on how to react to
input events so as to conform to their individual
specifications. We propose a methodology for developing such
systems in a modular manner based on the notion of
"conflict-tolerant" features that are designed to continue
offering advice even when their advice has been overridden in the
past. We give a simple priority-based scheme for composing such
features, which guarantees the "maximal" use of each
feature. We provide a formal framework for specifying such
features, and a compositional technique for verifying systems
developed in this framework.
This is joint work with Madhu Gopinathan, Prahlad Sampath, and
S. Ramesh.