Petri Nets 2012 & ACSD 2012
Hamburg, Germany, June 25–29, 2012
Note: Detailed information about all events is also collected in the programme booklet.
The operators of concurrent programming include sequential composition, choice, synchrony, and concurrent composition. These operators are subject to algebraic laws as familiar and elegant as the laws governing the arithmetic operators which we learnt at school. The only unfamiliar law is that which relates sequential and concurrent composition: it is similar to the interchange law of category theory. The power of the algebra of concurrent programming is such as to permit purely algebraic proof of familiar programming calculi, like Hoare logic and separation logic and Jones rely/guarantee. Furthermore, the algebra can also prove the transitions of an operational semantics, like Milner's process calculus CCS.
But do the laws apply to specifications and designs of programs that run concurrently on today's multi-processor computer systems? To give an affirmative answer to this question, we define a realistic mathematical model of concurrent programming, and prove that it satisfies the laws. A program is modelled as the set of all its possible executions, in all possible environments. Choice is modelled as union of sets (only one operand is executed). Synchrony is intersection (both operands are executed, and behave the same), and refinement between programs is set inclusion (so the refined program is more deterministic).
An execution is modelled as an occurrence net, whose nodes are events that have occurred in and around the executing computer, and whose arrows represent a dependency between pairs of the events. Concurrent composition of executions is just their disjoint union: every event is evoked by exactly one of the concurrent operands. Sequential composition is similar, subject to the proviso that no event of the first operand can depend on any event of the second operand. These composition operators are lifted point-wise to sets.
by Alain Finkel
Well-structured transition systems (WSTS) are a general class of infinite-state systems where termination, boundedness and coverability are decidable, using simple algorithms that work forwards and backwards. These algorithms cannot decide more complex problems like the place-boundedness problem and the computation of the cover (the downward closer of the reachability set).
To achieve this goal, we consider complete WSTS where the set of states is a complete well ordering (with other technical but realistic hypotheses).
We will then describe a simple, conceptual forward analysis procedure for infinite-complete WSTS. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set of X. We show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets.
We will first provide a survey about the theory of WSTS and then we will focus on complete WSTS.
by Bart Jacobs
Typical of the area of computer security is the presence of a malicious attacker who is deliberately trying to undermine your system. This makes computer very hard, because the behaviour of the attacker is hard to predict. Formal approaches to security thus mainly serve to make your assumptions about your system and the attacker explicit. Via a number of case studies in computer security this point will be elaborated.
This talk considers interactive Markov chains (IMCs), a natural generalization of transition systems and continuous-time Markov chains (CTMCs). We show how they can be used to provide a truly simple semantics of Generalized Stochastic Petri Nets (GSPNs). In fact, any GSPN. No restrictions on the concurrent/conflicting enabledness of immediate transitions are imposed. This contrasts with classical solutions for GSPNs which use weights. (A simple extension of IMCs also covers weights.)
We will present novel analysis algorithms for expected time and long-run average time objectives of IMCs, i.e., GSPNs. Two case studies indicate the feasibility of these analyses and show that a classical reliability analysis for confused GSPNs may lead to significant over-estimations of the true probabilities.
My key slogan will be: treat nondeterminism as is! This yields both a simple GSPN semantics and trustworthy analysis results.
Finally we show that IMCs naturally cover engineering notations like dynamic fault trees and the SAE-standardized Architecture Analysis & Design Language (AADL).
by Jens Sparsø
Over the last decade, the network-on-chip concept has evolved from an academic research topic towards industrial take-up. Many of today's chip multi-processors (used in general purpose computing) and many of today's multi-processor system-on-chip platforms (used in application-specific embedded systems) are built around some form of intra-chip packet-switched interconnection-network. Designing a network-on-chip poses challenges in several very different areas: At the hardware level designers are concerned with issues like area, speed and power consumption of the routers and links in the network, as well as timing organization of the whole platform (synchronous, mesochronous, globally-asynchronous, locally-synchronous and asynchronous). At the system level designers are concerned with issues like programming model, memory hierarchy and perhaps guaranteeing of real-time requirements. The talk will review some of our past work in the field of networks-on-chip and the lessons learned, and discuss ongoing research specifically targeting networks-on-chip for real-time multi-processor systems.
