Welcome to the IFx-OMEGA tool webpage

IFx-OMEGA is a compiler / simulator / model-checker for a rich subset of UML 2.2 / SysML 1.1, based on the IF model checker from VERIMAG.

IFx-OMEGA originated in the European project IST OMEGA, and was further developed with support from other projects including IST ASSERT, ESA Activity 3-12639 and ESA FullMDE.

IFx-OMEGA may be used to validate and verify asynchronous timed system models with complex dynamics. It is based on a rigorous semantics, especially suited for critical real-time embedded systems.

IFx-OMEGA supports a rich subset of UML 2.2 / SysML 1.1, including:

  • most elements of class/block diagrams : interfaces, classes with properties and operations, signals, association and generalization relations, composite structures with ports, connectors, etc.
  • most elements of state machines : transitions with discrete/timed guards, trigger and effect, composite states, parallel regions, etc.
  • actions : a concrete textual language for actions, compatible with the UML 2.2 action metamodel and including actions for : object creation and destruction, operation calls, expression evaluation, variable assignment, signal output, operation return, as well as control flow structuring statements (conditionals and loops, which are realized by the activity metamodel in UML).