* Model checking, using Petri Net `Tina <http://projects.laas.fr/tina//>`_, and `LNT <http://cadp.inria.fr>`_
* Constraint analysis, using the REAL annex language
It can be integrated with the `AADLib <https://github.com/OpenAADL/AADLib>`_ library of AADL components, and through a `OSATE2 plugin <https://github.com/OpenAADL/osate2-ocarina>`_
It can be integrated with the `AADLib <https://github.com/OpenAADL/AADLib>`_ library of AADL components.
It can also be embedded in AADL editors: in `OSATE <http://osate.org>`_ using the `OSATE2 plugin <https://github.com/OpenAADL/osate2-ocarina>`_, and `AADL Inspector <http://www.ellidiss.fr/public/wiki/wiki/inspector>`_
