Unified Maude model-checking tool

The unified Maude model‑checking utility umaudemc is a uniform command‑line, graphical, and programming interface to different model checkers operating on Maude specifications. On both standard and strategy‑controlled Maude specifications, umaudemc can be used for

• checking LTL, CTL, CTL*, and μ‑calculus properties (see Standard model checking),

• applying probabilistic model‑checking methods (see Probabilistic model checking),

• estimating quantitative properties by statistical model checking (see Statistical model checking), and

• exporting the rewrite graphs in different formats and more (see Other tools).

This utility can be installed with

$ pip install umaudemc

or downloaded from its git repository. It requires Python 3.9 or newer and the maude Python library, which is automatically installed by the previous pip command. Some external backends are optional for standard and required for probabilistic model checking, while installing SciPy is advisable for statistical model checking. Follow the corresponding links for installation instructions.

See also

Maude website · Maude 3.5.1 manual · Source code

Using the tool

The command‑line interface is organized in subcommands: check, pcheck, scheck, graph, and gui Their syntax and options are listed by passing the --help flag. Almost every command starts with the following arguments:

$ umaudemc ⟨subcommand⟩ ⟨Maude filename⟩ ⟨initial term⟩

Some more options are generally available for a more precise selection of the input Maude model:

--module ⟨name⟩, -m ⟨name⟩

Selects the module specifying the system to be model checked. By default, as in the Maude interpreter, the last module will be used unless a module is explicitly selected with a select command in the file.

--metamodule ⟨term⟩, -M ⟨term⟩

Selects the meta‑module described by its argument as the module where to model check. The term will be reduced in the module indicated by the module option or selected by default.

Moreover, the following arguments may be inserted between umaudemc and the subcommand:

--verbose, -v

Select the verbose mode so that more information is printed by the tool.

--no-advise

Suppress debug advisories from Maude, like the -no-advise option of the Maude interpreter.

--version

Show the current version of the tool and the optional dependencies that have been detected to be available or missing.

Moreover, umuademc can be used as a Python library (see API reference).

Table of contents

• Introduction
  • Standard Maude models
  • Strategy-controlled models
  • Probabilistic models
• Standard model checking
  • Syntax of formulas
  • Strategy-aware model checking
  • Examples
  • External model checkers and their installation
• Probabilistic model checking
  • Examples
  • External backends and their installation
• Statistical model checking
  • QuaTEx
  • Examples
  • Distributed model checking
  • Particularities of some probability assignment methods
• Other tools
  • Graph generation
  • A graphical interface
  • Batch checking
• Bibliography
  • References
• API reference
  • MaudeModel