Mica is an Ocaml library developed by Benoît Caillaud implementing the Modal Interface algebra published in the following paper:

Jean-Baptiste Raclet, Eric Badouel, Albert Benveniste, Benoît Caillaud, Axel Legay, Roberto Passerone: A Modal Interface Theory for Component-based Design. Fundam. Inform. 108(1-2): 119-149 (2011).

The purpose of Modal Interfaces is to provide a formal support to contract based design methods in the field of system engineering. Modal Interfaces enable compositional reasoning methods on I/O reactive systems.

In Mica, systems and interfaces are represented by extension. However, a careful design of the state and event heap enables the definition, composition and analysis of reasonably large systems and interfaces (~106 states). The heap stores states and events in a hash table and ensures structural equality (there is no duplication). Therefore complex data-structures for states and events induce a very low overhead, as checking equality is done in constant time.

Thanks to the Inter module and the mica interactive environment, users can define complex systems and interfaces using Ocaml syntax. It is even possible to define parameterized components as Ocaml functions.

Mica is available as an open-source distribution, under the CeCILL-C Free Software License Agreement, version 1. Users agree to comply with the terms of the license contained in the following document: http://www.cecill.info/licences/Licence_CeCILL-C_V1-en.html

Mica is a testbed for new operators, algorithms and methods with a strong focus on system design. It has been enriched with several new operators and services: abstraction, projection, compatible quotient, weak implication, ... The next step will be the extension of Modal Interfaces to more expressive formalisms, retaining its low computational complexity.