The Modular Reachability Analyzer

Maria (Modular Reachability Analyzer) is a four-year research project being carried out at the Laboratory for Theoretical Computer Science of Helsinki University of Technology. The focus is on applications and on making the power of formal analysis methods available for the software industry.

Goals

The main product of the project is a pack of software tools that perform reachability analysis and check safety and liveness properties of distributed system models. The models can be constructed either by hand or automatically from other formalisms, such as the CCITT Specification and Description Language (SDL).

One of the most important goals in the project is to be able to analyze telecommunications protocols specified in SDL. The SDL must be translated to an efficient but yet accurate model, and the properties to be verified must be given in a language simple enough for the average engineer. Finally, the counterexamples found in the analysis must be translated back to execution paths and states in the original formalism.

Previous Work

Translating SDL specifications to Petri Net models is not a new idea. Implementations exist for SDL-like languages (Emma for TNSDL) and for subsets of SDL. The lesson learned in the Emma project was that the reachability analyzer must support sophisticated data types in order to allow for effective, compact and readable translations from specifications written in a high-level language such as SDL.

There are many reachability analysis tools for different classes of Petri Nets, but in our opinion, there is no match for the tool developed in the Maria project, when it comes to the flexibility of the data type system and to the expressive power of the expressions.