Maria

Maria: Modular reachability analyser for algebraic system nets Maria performs simulation, exhaustive reachability analysis and on-the-fly LTL model checking of high-level Petri nets with fairness constraints. The algebra contains powerful built-in data types and operations. Models can be exported to low-level Petri nets and labelled transition systems. Translator programs allow Maria to analyse transition systems as well as distributed computer programs written in procedural or object-oriented languages, or high-level specifications such as SDL. par Maria has been implemented in portable C and C++, and it is freely available under the conditions of the GNU General Public License.


References in zbMATH (referenced in 17 articles , 1 standard article )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Lakos, Charles: Modelling mobile IP with mobile Petri nets (2009)
  2. Klaudel, Hanna; Pommereau, Franck: M-nets: a survey (2008)
  3. Kryvyy, Sergiy; Matvyeyeva, Lyudmila: Algorithm of translation of MSC-specified system into Petri net (2007)
  4. Comet, Jean-Paul; Klaudel, Hanna; Liauzu, Stéphane: Modeling multi-valued genetic regulatory networks using high-level Petri nets (2005)
  5. Evangelista, Sami: High level Petri nets analysis with Helena (2005)
  6. Kristensen, Lars Michael; Christensen, Søren: Implementing coloured Petri nets using a functional programming language (2004)
  7. Latvala, Timo; Mäkelä, Marko: LTL model checking for modular Petri nets (2004)
  8. Ojala, Leo; Penttinen, Olli-Matti; Parviainen, Elina: Modeling and analysis of Margolus quantum cellular automata using net-theoretical methods (2004)
  9. Thanh, Cécile Bui; Klaudel, Hanna: Object-oriented modelling with high-level modular Petri nets (2004)
  10. Aalto, Annikka; Husberg, Nisse; Varpaaniemi, Kimmo: Automatic formal model generation and analysis of SDL (2003)
  11. Gaeta, R.; Gribaudo, M.; Manini, D.; Sereno, M.: On the use of Petri nets for the computation of completion time distribution for short TCP transfers (2003)
  12. Mäkelä, Marko: Model checking safety properties in modular high-level nets (2003)
  13. Thanh, C.Bui; Klaudel, H.; Pommereau, F.: Petri nets with causal time for system verification (2003)
  14. Klaudel, Hanna; Pommereau, Franck: A class of composable and preemptible high-level Petri nets with an application to multi-tasking systems (2002)
  15. Mäkelä, Marko: Maria: Modular reachability analyser for algebraic system nets (2002)
  16. Mäkelä, Marko: Optimising enabling tests and unfoldings of algebraic system nets (2001)
  17. Mäkelä, Marko: Modular reachability analyzer for high-level Petri nets (2000)