Invariant Refinement Method (IRM)

IRM is a method and a corresponding model that allows for designing software-intensive Cyber-Physical Systems (siCPS) with a focus on dependability aspects. IRM is tailored for systems consisting of ensembles of components (e.g. DEECo-based systems), and provides a way to refine high-level system invariants into low-level system obligations, or equivalently to trace low-level system obligations to their rationale at the requirements space.

A good starting point to learn about (different types of) invariant refinements in ensemble-based systems is this paper.

IRM for Self-Adaptation (IRM-SA)

IRM-SA is an extension to IRM that allows for introducing alternative decompositions in the design. Each branch in an alternative decomposition corresponds to a different situation in the environment (captured by one or more assumptions) that dictates a different design in order for the parent invariant to be preserved.

IRM-SA design tool

The IRM-SA design tool is part of the IRM-SA toolchain and can be used to create IRM-SA models (e.g. like this one). It relies on Eclipse's EMF and GMF technologies and on Epsilon modeling languages for the tasks of model manipulation and model tranformation.

The source code of the tool (prototype version) is available at

IRM-SA-based adaptation plugin for DEECo

IRM-SA models can also be used at runtime to guide architectural reconfigurations in a DEECo-based system. The idea is to translate the IRM-SA graph into an analytical model (e.g. a predicate logic formula) and reason on this model at runtime.

A proof-of-concept implementation of the above idea as a jDEECo plugin is available at

IRM-SA experimental evaluation with jDEECo

In order to experiment with the application of IRM-SA self-adaptation in decentralized settings, we performed multi-node simulations with jDEECo. The simulation code and parameters are available on GitHub. The raw results and the IRM-SA model of the experiments (accompanying our submission to the JSS special issue on adaptive and reconfigurable software systems and architectures) are available in this experiment kit.

IRM-SA empirical evaluation

The material and results of the empirical study we performed to evaluate IRM-SA (accompanying our submission to the JSS special issue on adaptive and reconfigurable software systems and architectures) are available here.

Case studies

Firefighter Tactical Decision System

IRM-SA has been used so far to model a Firefighter Tactical Decision System, an inherently dynamic, real-world, real-scale distributed system.

Publications & Technical Reports

[PDF] Keznikl J., Bureš T., Plášil F., Gerostathopoulos I., Hnětynka P., Nicklas Hoch: Design of Ensemble-Based Component Systems by Invariant Refinement,
In Proceedings of CBSE 2013, Vancouver, Canada, June 2013.

[PDF] Bureš T., Gerostathopoulos I., Keznikl J., Plášil F.: Formalization of Invariant Patterns for the Invariant Refinement Method,
Tech. Report No. D3S-TR-2013-04, Dep. of Distributed and Dependable Systems, Charles University in Prague, February 2014.

[PDF] Gerostathopoulos I., Bureš T., Hnětynka P.: Position Paper: Towards a Requirements-Driven Design of Ensemble-Based Component Systems,
In Proceedings of International Workshop on Hot Topics in Cloud Services, ICPE '13, Prague, Czech Republic, March 2013.

[PDF] Bureš T., Gerostathopoulos I., Hnětynka P., Keznikl J., Kit M., Plášil F., Noel Plouzeau: Adaptation in Cyber-Physical Systems: from System Goals to Architecture Configurations,
Tech. Report No. D3S-TR-2014-01, Dep. of Distributed and Dependable Systems, Charles University in Prague, January 2014.

[PDF] Gerostathopoulos I.: Model-Driven Design of Ensemble-Based Component Systems,
In Joint Proceedings of MODELS' 14 Poster Session and ACM Student Research Competition, Valencia, Spain, CEUR, September 2014.


Your questions, opinions, and comments are welcome. For proposing impovements and reporting bugs, please consider using the issues tool on GitHub/GitLab.

Ilias Gerostathopoulos
Jaroslav Keznikl
Michal Kit
Tomáš Bureš
Petr Hnětynka
František Plášil
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>
  • How to find us?
Modified on 2017-02-27