Momba

Momba provides a Python framework for constructing, validating, and analyzing quantitative models using the JANI-model interchange format.

Key Features:

• JANI-model support: Reads and writes the JANI-model interchange format, which represents systems with concurrency, probabilistic elements, real-time dynamics, and continuous behaviors.
• Pythonic interface: Exposes a Python-based, syntax-aware macro language for programmatic model construction, validation, and analysis.
• Modular model construction: Supplies convenience functions to build models modularly for reuse and composability.
• Model validation and analysis: Implements functions for validating model structure and performing analysis on quantitative models.
• Exploration engine: Includes an exploration engine for rapid prototyping of interactive model exploration and visualization and for integration into testing frameworks.
• Interoperability: Ensures compatibility with state-of-the-art model checkers and other analytical tools via the JANI-model format.

Scientific Applications:

• Quantitative model checking: Enables exchange and analysis of models with model checkers for quantitative verification studies.
• Modeling concurrent and stochastic systems: Supports construction and analysis of systems exhibiting concurrency, probabilistic behavior, real-time dynamics, and continuous dynamics.
• Tool prototyping and testing: Facilitates rapid prototyping of interactive exploration and visualization tools and their integration into testing workflows.

Methodology:

Implements a Pythonic, syntax-aware macro language and convenience functions for modular model construction; reads and writes the JANI-model interchange format; provides an exploration engine; and offers model validation, analysis, and interoperability with external model checkers and analytical tools.