Interfaces have emerged as an essential concept for component-based system
engineering. Industrial needs, and requirements applicable to interface
theories in the context of embedded system design have been studied in
details. Thanks to its rich composition algebra, the modal interface theory
[1], developped by INRIA  matches these requirements, enabling both modularity
in design, an assume-guarantee style of reasoning and a better separation of
concerns and responsabilities between design teams. It is actually a
unification of the Assume/Guarantee and of the Interface Automata theory,
therefore allowing to express requirements using any of these two styles.
modal interfaces meet methodological requirements Modal interfaces have been
extended to finite data types and the full power of a synchronous interaction
semantics. This is implemented, in part, in the InterSMV modal interface
verifier. This tool is capable of computing compositions of interfaces
(conjunction, product and quotient) and can decide satisfaction and refinement
relations.

[1] J-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay, R.
Passerone. Modal Interfaces: Unifying Interface Automata and Modal
Specifications. To appear in Fundamenta Informaticae (2010).