Skip to main content

About this book

These Transactions publish archival papers in the broad area of Petri nets and other models of concurrency, ranging from theoretical work to tool support and industrial applications. ToPNoC issues are published as LNCS volumes, and hence are widely distributed and indexed. This Journal has its own Editorial Board which selects papers based on a rigorous two-stage refereeing process. ToPNoC contains:
- Revised versions of a selection of the best papers from workshops and tutorials at the annual Petri net conferences- Special sections/issues within particular subareas (similar to those published in the Advances in Petri Nets series)- Other papers invited for publication in ToPNoC- Papers submitted directly to ToPNoC by their authors
The 10th volume of ToPNoC contains revised and extended versions of a selection of the best workshop papers presented at the 35th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2014, and the 14th International Conference on Application of Concurrency to System Design, ACSD 2014. It also contains one paper submitted directly to ToPNoC.The 8 papers cover a diverse range of topics including model checking and system verification, refinement, and synthesis; foundational work on specific classes of Petri nets; and innovative applications of Petri nets and other models of concurrency.

Table of Contents


Verification of Logs - Revealing Faulty Processes of a Medical Laboratory

If there is suspicion of Lyme disease, a doctor sends a blood sample of the patient to a medical laboratory. The laboratory performs a number of different blood examinations, testing for antibodies against the Lyme disease bacteria. The total number of performed examinations depends on the intermediate results of the blood count. Of course, the number of performed examinations is important since the cost of each examination needs to be covered by the health insurance companies. In order to control and restrict the number of performed examinations, the health insurance companies provide a so called charges regulation document. If some health insurance company disagrees with the charges of a laboratory, it is the job of the public prosecution service to validate the charges according to this document.
In this paper we present a case study showing a systematic approach to revealing faulty processes in a medical laboratory. Different files produced by the information system of the respective laboratory are analyzed, consolidated, and stored in a database. An excerpt of this data is translated into an event log, providing a list of all events performed by the information system. This list is further compressed and translated into the language of the information system. Compared to the size of the data and the size of the event log, the size of the language is small. With the help of the regulation document this language can be split in two sets - the set of valid and the set of faulty words. In a next step, we build a colored Petri net model corresponding to the set of valid words in a sense that only the valid words are executable in the Petri net model. In a last step we translate the colored Petri net into a PL/SQL-program. This program can automatically reveal all faulty processes stored in the database.
Robin Bergenthum, Joachim Schick

An Everlasting Secure Non-interactive Timestamping Scheme in the Bounded Storage Model

Digital timestamping is a cryptographic technique allowing to affix a reliable date to a digital document in order to prove that it exists and its integrity is kept since this date. However, there is a good chance that a lot of current timestamping systems will not be secure in the coming years. In fact, the security of most of the existing timestamping systems is based on the security of the used cryptographic techniques as hash functions. However, a hash function has a limited lifetime. In this context, we provide a non-interactive timestamping scheme in the bounded storage model (BSM). In this model, we assume that an adversary has a limited memory but his computing power can be unlimited. Thus, the security of our timestamping scheme does not depend on the lifetime of any cryptographic technique. We prove, in fact, that our timestamping scheme is eternally secure even against an adversary with unlimited computing power.
Assia Ben Shil, Kaouther Blibech Sinaoui

Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets

In this paper, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behavior of bounded Time Petri Nets (TPN) with strong time semantics. The main feature of this abstract representation compared to existing approaches is the used criterion to encapsulate the elapsing of time within each node of the TAG (called aggregate), and how to maintain the relative differences between the firing times of enabled transitions. We prove that the TAG preserves timed traces and reachable states of the corresponding TPN. Another interesting and novel feature of the TAGs is the possibility of extracting an explicit run from any of its traces. Thus, we supply an algorithm that maps an abstract run of the TAG to an explicit timed trace (involving a relative elapsed time before each fired transition) of the corresponding TPN. Moreover, the fact that the TAG preserves the timed behavior of the corresponding TPN makes it directly usable in order to check both event- and state-based timed properties as well as the Zenoness property. Zenoness is a pathological behavior which violate a fundamental progress requirement for timed systems stating that it should be possible for time to diverge. A TPN is said to be Zeno when it admits a run where an infinity of transitions are fired in a finite amount of time. We give an algorithm allowing to detect the Zenoness of bounded TPNs and compare the size of the TAG to two well known approaches namely the state class graph and the zone-based graph methods.
Kais Klai

SMT-Based Abstract Parametric Temporal Planning

Planics is a tool for solving the web service composition problem. It uses a uniform semantic description of the services and the service types as a part of the ontology which contains also the objects processed by the services. The user query is expressed in a fully declarative language defined over terms from the ontology by describing two object sets, called the initial and the expected world. The task of Planics consists in finding a sequence of services transforming the initial world into a superset of the expected one using service types available in the ontology and matching them later with real-world services. An abstract planning is the first phase of the task in which Planics composes service types. The paper extends this phase with a theory and a module for parametric temporal planning, by extending the user query with object variables and a PLTLX formula specifying temporal aspects of world transformations in a plan. Our solution comes together with an example, an implementation, and experimental results.
Artur Niewiadomski, Wojciech Penczek

Kleene Theorems for Synchronous Products with Matching

In earlier work [LMP11], we showed that a graph-theoretic condition called “structural cyclicity” enables us to extract syntax from a conflict-equivalent product system of automata. In this paper we have a “pairing” property in our syntax which allows us to connect to a broader class of synchronous product systems [Arn94] with a “matching” property, where the conflict-equivalence is not statically fixed. These systems have been related to labelled free choice nets.
Ramchandra Phawade, Kamal Lodaya

Symbolic Model Checking of Security Protocols for Ad hoc Networks on any Topologies

Petri nets have proved their effectiveness in modeling and formal verification of a large number of applications: control systems, communication protocols, application workflows, hardware design, etc. In the present days, one important focus of computer science is on security and secure communications. The use of Petri nets for verifying security properties is not a mature field due to a lack of convenient modeling and verification capabilities. So far, in the Petri Net field there is only CPN Tools that is mature enough for modeling, using the colored Petri nets formalism. Nevertheless such verifications cannot be performed on large systems as CPN Tools is based on an exhaustive way of computing the semantics of a model. In this paper we present the use of AlPiNA, another candidate for this task. AlPiNA is a symbolic model checker that uses the formalism of algebraic Petri nets. We have used it successfully for modeling ad hoc networks and for verifying security protocols designed for this type of networks. As a case study and benchmark we have chosen the ARAN secure routing protocol. We managed to find all the attacks that were already reported for this protocol. To our knowledge this work is also the first successful attempt to use Petri nets for model checking the security properties of ad hoc networks protocols.
Mihai Lica Pura, Didier Buchs

Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling

The early detection of potential threats during the modelling and design phase of a Secure Information System is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during system execution. This paper deals with internal attacks which can be made by people inside the organization. Such attacks are difficult to detect because insiders have authorized system access and also may be familiar with system policies and procedures. We are interested in finding attacks which conform to the access control policy, but lead to unwanted states. These attacks are favoured by policies involving authorization constraints, which grant or deny access depending on the evolution of the functional Information System state. In this context, we propose to model functional requirements and their Role Based Access Control (RBAC) policies using B machines and then to formally reason on both models. In order to extract insider attack scenarios from these B specifications, our approach first investigates symbolic behaviours. Then, the use of a model-checking tool allows to exhibit, from a symbolic behaviour, an observable concrete sequence of operations that can be followed by an attacker. In this paper, we show how this combination of symbolic analysis and model-checking allows to find out such insider attack scenarios.
Amira Radhouani, Akram Idani, Yves Ledru, Narjes Ben Rajeb

Modelling and Analysis Mobile Systems Using $$\pi $$ -calculus (EFCP)

Reference passing systems, like mobile and reconfigurable systems are common nowadays. The common feature of such systems is the possibility to form dynamic logical connections between the individual modules. However, such systems are very difficult to verify, as their logical structure is dynamic. Traditionally, decidable fragments of \(\pi \)-calculus, e.g. the well-known Finite Control Processes (FCP), are used for formal modelling of reference passing systems. Unfortunately, FCPs allow only ‘global’ concurrency between processes, and thus cannot naturally express scenarios involving ‘local’ concurrency inside a process, such as multicast. In this paper we propose Extended Finite Control Processes (EFCP), which are more convenient for practical modelling. Moreover, an almost linear translation of EFCPs to FCPs is developed, which enables efficient model checking of EFCPs.
Victor Khomenko, Vasileios Germanos


Additional information

Premium Partner

    Image Credits