PNML Compliance

The SEPIA framework is a Java library for security based modelling and reasoning on basis of Petri net based techniques. It comprises a set of traversal, refinement of readability techniques in order to analyse system behaviour in form of Petri nets. For compatibility with other frameworks, the Petri nets can be exported and imported using the PNML and Petrify file formats.

The SEPIA framework provides implementations for various types of Petri nets (T. Stocker & F. Böhr. IF-Net: A Meta-Model for Security-Oriented Process Specification).

Along Place/Transition-nets, it supports Petri nets with distinguishable token colors, so called colored Petri nets (CPN). To support information flow analysis of processes, it defines so-called IF-Nets, tailored for security-oriented workflow modelling which enable users to assign security-levels to transitions, data elements and persons/agents participating in the process execution.

For these net types, Petri net type definitions (PNTD) have been devised, based on the PNML Core Model (Pnml.org – PNML reference site http://www.pnml.org/).

Their availability under http://ifnml.process-security.de/grammar/v1.0/ allows for a syntactical validation of all PNML documents by SEPIA, as long as the Petri net type attribute points to a valid type definition. The type attribute is the URL to the PNTD document without the extension .pntd. The type attribute is valid as long as it exists and the PNTD document it points to exists, too. If the net type attribute is not valid, either the validation fails or the parser tries to parse the PNML document as P/T-net.

Since the net types of SEPIA differ from those of pnml.org, not all PNML documents can be represented in SEPIA’s proprietary format and therefore parsed or serialized (but still validated). All nets that pass the validation but aren’t of one of SEPIA’s net types (P/T-net, CPN, or IF-net) are interpreted as P/T-net. With this convention, we try to keep compatibility with other tools on the cost of some information that gets lost when interpreting nets as P/T-nets.

Since our data structure doesn’t allow for split Petri nets spread over several pages, we limited the number of possible pages per net to one. Note that in case of more pages, SEPIA parsers will only consider the first page.

The SEPIA framework provides all mandatory features in order to be compliant with the PNML guidelines (Pnml.org – Tool construction http://www.pnml.org/tools.php):

  • Create Petri nets according to their type definition and export them in the PNML file format.
  • Parse Petri nets from their PNML file format according to their type definition.
  • The PNML syntax validation is optional.