Maria

Overview

Tool homepage: http://www.tcs.hut.fi/Software/maria/

Tool availability: Free of charge

Tool Features

• High-level Petri Nets
• Place/Transition Nets
• Modular high-level nets
• Labelled state transition systems

• Token Game Animation
• Fast Simulation
• State Spaces
• Modular state spaces
  LTL model checker with fairness assumptions
  Very high-level data types and operations

Environments

• Sun, SunOS 5.7 and 5.8 (32-bit and 64-bit)
• Digital, UNIX 4.0
• Silicon Graphics, IRIX 6.5 (32-bit and 64-bit)
• HP-UX 11.22
• NetBSD, FreeBSD, OpenBSD
• PC, Linux
• PC, MS Windows 95 and later
• Apple, Mac OS X 10.1
• Any system that supports C++

Tool Description

Maria is a reachability analyzer and a model checker whose modelling formalism is based on Algebraic System Nets, capable of handling tens of millions of reachable states and enabled transitions.

Maria includes a distributed algorithm for checking safety properties. The algorithm can be executed on multi-processor computers as well as on workstations in TCP/IP networks.

Optionally, nets can be unfolded or translated to transition systems.

Thanks to its modular design and open source license (GPL), Maria can easily be extended with new algorithms.

Contact Information

Marko M„kel„
Timo Latvala
Laboratory for Theoretical Computer Science
P.O.Box 5400
02015 Helsinki University of Technology
Finland

Phone:  +358 - 9 - 451 2895
Fax:    +358 - 9 - 451 3369
E-mail: maria@tcs.hut.fi

Other Remarks

Maria is efficient both in interactive use and in exhaustive reachability analysis, as it can both interpret models directly and compile them to fast C code.

The graphical user interface of Maria is based on GraphViz.