Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Model-Checking Kit: Modelling a system


The Kit offers several languages for modelling a system. These languages can be divided into so-called net languages and those languages abstracting from net details. The following languages can be used for modelling a system:

  • Languages abstracting from net details

  • These languages abstract from structural net concepts like places, transitions and arcs.

    • B(PN)2 (Basic Petri Net Programming Notation)
      This is a structured parallel programming language, offering among others loops, blocks and procedures.

    • CFA (Communicating Finite Automata)

    • This is a language for the description of finite automata communicating via shared variables or channels of finite length. CFA offer very flexible communication mechanisms. They are one of the modelling languages of the PEP tool.

    • IF (Interchange Format)

    • This is a language proposed in order to model asynchronous communicating real-time systems.

  • Net languages

  • In these languages one has to define places, transitions and arcs explicitely.

    • APNN (Abstract Petri Net Notation)

    • This is a language for the description of different classes of Petri nets. Keywords are similar to LaTeX commands.

    • PEP (Low level PEP notation)

    • This is a low level language, to be used by machines. It is included in this list only because some tools can export models in this language.

    • SENIL (Simple Extensible Net Input Language)

    • This is another language for the description of 1-safe Place/Transition Petri nets. It is suitable for small nets with at most a few dozens of nodes, but not for larger projects. It is designed to be used by students.

Next chapter: Describing properties