Ayleen Schinko and Walter Vogler. Fault-Free Refinements for Interface Automata
A refinement preorder for a model of concurrent systems should be compositional (i.e. a precongruence for parallel composition) and should not introduce faults into a fault-free specification. Arguably, if these are the features of interest, the coarsest such precongruence is the optimal refinement preorder and often, it preserves additional properties.
For the model of interface automata, originally faults are communication errors in the form of unexpected inputs. The respective optimal preorder has been characterized as the inclusion of two trace sets. Here, we extend these characterizations by regarding also quiescence (quiescence and divergence resp.) as faults. The latter preorder is coarser, i.e. better, than an earlier preorder regarding errors, quiescence and divergence. A conjunction operator allows to specify different facets of an overall specification by separate automata and then to combine them. We also present conjunction operators for our settings, avoiding flaws that can be found in the literature.
Bram van der Sanden, Marc Geilen, Michel Reniers and Twan Basten. Partial-Order Reduction for Performance Analysis of Max-Plus Timed Systems
This paper presents a partial-order reduction method for performance analysis of max-plus timed systems. A max-plus timed system is a network of automata, where the timing behavior of deterministic system tasks (events in an automaton) is captured in (max,+) matrices. These tasks can be characterized in various formalisms like synchronous data flow, Petri nets, or real-time calculus. The timing behavior of the system is captured in a (max,+) state space, calculated from the composition of the automata. This state space may exhibit redundant interleaving with respect to performance aspects like throughput or latency. The goal of this work is to obtain a smaller state space to speed up performance analysis. To achieve this, we first formalize state-space equivalence with respect to throughput and latency analysis. Then, we present a way to compute a reduced composition directly from the specification. This yields a smaller equivalent state space. We perform the reduction on-the-fly, without first computing the full composition. Experiments show the effectiveness of the method on a set of realistic manufacturing system models.
Loic Helouet, Hervé Marchand and John Mullins. Concurrent secrets with quantified suspicion
A system is considered as opaque if behaviors that should be kept secret cannot be discovered by any user of the system. Deciding opacity of distributed systems was originally addressed as a boolean question, and then extended to a probabilistic setting.
This paper considers a different quantitative approach that measures the efforts that a malicious user should make to discover a secret. This effort is measured as a distance w.r.t a regular profile specifying a normal behavior. This leads to several notions of quantitative opacity. When attackers are passive, i.e. they only observe the system, quantitative opacity can be brought back to a language inclusion problem, and is PSPACE-complete. When attackers are active, i.e. perform particular actions leading to secret leakage within a finite horizon, quantitative opacity becomes a partial observation quantitative game, where an attacker wins if it has a strategy to learn a secret without deviating too much from its profile. Within this active setting, the complexity of opacity is EXPTIME-complete.
Alexander Schulz-Rosengarten, Steven Smyth, Reinhard von Hanxleden and Michael Mendler. On Reconciling Concurrency, Sequentiality and Determinacy for Reactive Systems – A Sequentially Constructive Circuit Semantics for Esterel
A classic challenge in designing reactive systems is how to reconcile concurrency with determinacy. Synchronous languages, such as Esterel, SyncCharts or SCADE, resolve this by providing a semantics that does not depend on run-time scheduling decisions. Esterel comes with a constructive semantics that is grounded in physics: an Esterel program is considered valid (constructive) iff its corresponding circuit has a well-defined, delay-insensitive behavior. The circuit semantics provides on the one hand a mathematically grounded semantics, based on constructive logic, on the other hand it gives a direct path to a data-flow style software implementation. However, Esterel’s constructive semantics entails a rather restricted regime for handling sequential accesses to shared data. Thus many programs are rejected as being non-constructive, even though they have a very natural, determinate interpretation. We here present a “sequentially constructive circuit semantics” (SCC) that lifts this restriction, by distinguishing sequential and concurrent execution contexts. This permits an imperative style familiar to programmers versed in C, for example, without leaving the sound physical foundation of synchronous programming.
Vincent Bloemen, Jaco van de Pol and Wil van der Aalst. Symbolically Aligning Observed and Modelled Behaviour
Conformance checking is a branch of process mining that aims to assess to what degree a given set of event logs and a corresponding reference model conform to each other. The state-of-the-art approach in conformance checking is based on the concept of alignments. Alignments express the observed behaviour in terms of the reference model while minimizing the number of mismatches between the event data and the model. The currently known best algorithm for constructing alignments applies the A* shortest path algorithm for each trace of event data.
In this work, we apply insights from the field of model checking to aid conformance checking. We investigate whether alignments can be computed efficiently via symbolic reachability with decision diagrams. We designed a symbolic algorithm for computing shortest-paths on graphs restricted to 0- and 1-cost edges (which is typical for alignments).
We have implemented our approach in the LTSmin model checking toolset and compare its performance with the A* implementation supported by ProM. We generated more than 4000 experiments (Petri net model and log trace combinations) by setting various parameters, and analysed performance and related these to structural properties.
Our empirical study shows that the symbolic technique is in general better suited for computing alignments on large models than the A* approach. Our approach is better performing in cases where the size of the state-space tends to blow up. Based on our experiments we conclude that the techniques are complementary, since there is a significant number of cases where A* outperforms the symbolic technique and vice versa.
Bowen Li, Maciej Koutny, Brian Randell, Anirban Bhattacharyya and Talal Alharbi. SONCraft: A Tool for Construction, Simulation and Analysis of Structured Occurrence Nets
This paper presents SONCraft – an open source tool for editing, simulating, and analysing Structured Occurrence Nets (SONs), which is a Petri net-based formalism for portraying the behaviour of complex evolving systems. The tool is implemented as a Java plug-in within the Workcraft platform, which is a flexible framework for the development and analysis of Interpreted Graph Models. SONCraft provides an easy to use graphical interface that facilitates model entry, supports interactive visual simulation, and allows the use of a set of analytical tools. We give an overview of SONCraft functionality and architecture.
Fatma Jebali and Dumitru Potop-Butucaru. Ensuring consistency between cycle-accurate and instruction set simulators
The xMAS micro-architecture modeling language has been introduced by Intel to facilitate the formal representation and functional analysis of on-chip interconnect fabrics. In this paper, we introduce xMAStime, a new domain-specific language inspired by xMAS. xMAStime allows the modeling of full micro-architectures comprising certain classes of CPU pipelines, caches, and RAM, to achieve timing analysis of real-time software. Given an in-order pipeline model in xMAStime, we automatically generate both a Cycle-Accurate, Bit-Accurate (CABA) hardware simulator and an instruction set simulator where time is accounted with safe upper bounds, as in Worst-Case Execution Time (WCET) analysis. The approach relies on the theory of endochronous systems, which ensures semantics consistency between the two generated simulators, using a delay-insensitivity argument. xMAStime is implemented over Lucid Synchrone – a synchronous data-flow language featuring higher order types. We apply the proposed approach to model and simulate a full-fledged MIPS32-based architecture.
Markus Anders, Anoop Bhagyanath and Klaus Schneider. On Memory Optimal Code Generation for Exposed Datapath Architectures with Buffered Processing Units
One reason for the limited use of instruction level parallelism (ILP) by conventional processors is their use of registers. Therefore, some recent processor architectures expose their datapaths to the compiler so that the compiler can move values directly between processing units to bypass the registers. In particular, the Synchronous Control Asynchronous Dataflow (SCAD) machine is an exposed datapath architecture that uses buffers at input and output ports of its processing units. Code generation techniques inspired by classic queue machines can completely eliminate the use of registers in SCAD. However, bounded buffer sizes still make spill code necessary to store values temporarily in main memory. Since memory access is expensive, it is desirable to minimize them for improving the performance of SCAD. Memory optimal code generation problems have been extensively studied in the case of register machines and were proven to be NP-complete. These results are however not directly applicable to SCAD since SCAD code bypasses register usage.
In this paper, we prove that memory optimal code generation for SCAD is also NP-complete by presenting a polynomial time transformation from memory optimal register code to memory optimal SCAD code. In particular, we present a one to one correspondence between the registers in register machines and the entries of buffers in SCAD machines which suggests that these architectures are closer to each other than expected. However, the size of circuit implementations of buffers scales much better compared to register files so that more space is available on SCAD machines. Second, the instruction set of SCAD does not depend on a given number of registers or buffers. Finally, we present experimental results to demonstrate the improvement of the performance of memory optimal SCAD code compared to memory optimal code that is based on register allocation.
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig, Marco Montali and Othmane Rezine. Complexity of Reachability for Data-aware Dynamic Systems
A formal model called database manipulating systems was introduced to model data-aware dynamic systems. Its semantics is given by an infinite labelled transition systems where a label can be an unbounded relational database. Reachability problem is undecidable over schemas consisting of either a binary relation or two unary relations. We study the reachability problem under schema restrictions and restrictions on the query language. We provide tight complexity bounds for different combinations of schema and query language, by reductions to/from standard formalism of infinite state systems such as Petri nets and counter systems. Our reductions throw light into the connection between two seemingly unrelated models.
Hanifa Boucheneb, Didier Lime, Olivier H. Roux and Charlotte Seidner. Optimal-cost reachability analysis based on time Petri nets
This paper investigates the optimal-cost reachability problem in the context of time Petri nets, where a rate cost is associated with each place. This problem consists in deciding whether or not there exists a sequence of transitions reaching, with minimal cost, a given goal marking. This paper shows that for some subclasses of cost time Petri nets, the optimal- cost reachability problem can be solved more efficiently using a method based on the state classes, without resorting to linear programming or splitting state classes.
Étienne André, Didier Lime and Mathias Ramparison. Timed automata with parametric resets
Timed automata (TAs) represent a powerful formalism to model and verify systems where concurrency is intricated with hard timing constraints. However, they can seem limited when dealing with uncertain or unknown timing constants. Several parametric extensions were proposed in the literature, and the vast majority of them leads to the undecidability of the EF-emptiness problem: “is the set of valuations reaching a given location empty?” Here, we study an extension of TAs where clocks can be reset to a parameter. While the EF-emptiness problem is undecidable for rational-valued parameters, it becomes PSPACE-complete for integer-valued parameters. In addition, exact synthesis of the parameter valuations set can be achieved.
Benjamin Smith and Gianfranco Ciardo. SOUPS: A Variable Ordering Metric for the Saturation Algorithm
Multivalued decision diagrams are an excellent technique to study the behavior of discrete-state systems such as Petri nets, but their variable order (mapping places to MDD levels) greatly affects efficiency, and finding an optimal order even just to encode a given set is NP-hard. In state-space generation, the situation is even worse, since the set of markings to be encoded keeps evolving and is known only at the end.
Previous heuristics to improve the efficiency of the saturation algorithm often used in state-space generation seek a variable order minimizing a simple function of the Petri net, such as the sum over each transition of the top variable position (SOT) or variable span (SOS). This, too, is NP-hard, so we cannot compute orders that minimize SOT or SOS in most cases but, even if we could, this would have limited effectiveness. For example, SOT and SOS can be led astray by multiple copies of a transition (giving more weight to it), or transitions with equal inputs and outputs (giving weight to transitions that should be ignored).
These anomalies inspired us to define SOUPS, a new heuristic that only takes into account the unique and productive portion of each transition. The SOUPS metric can be easily computed, allowing us to use it in standard search techniques like simulated annealing to find good orders. Experiments show that SOUPS is a much better proxy for the quantities we really hope to improve, the memory and time for MDD manipulation during state-space generation.
Dennis Schmitz, Daniel Moldt, Michael Haustermann, David Mosteller and Christian Röder. Team Coordination Based on Causal Nets with Synchronous Channels
Projects consist of a partially ordered set of tasks that need to be performed to reach the projects’ goals. Ordering the tasks and coordinating the individual actors are prerequisites for the success of a project.
The sub-teams (groups) may be distributed in terms of space, time or organization. Hence, they naturally focus on planning their local (intra-group) tasks. In order to deliver a consistent result the groups additionally have to cooperate. Thus, modeling local task orders and coordinating inter-group tasks while avoid- ing global deadlocks is necessary. Today, centralized approaches with a single diagram are used to model the global task order and calculate its critical path.
We propose that each group separately models their intra- and inter-group tasks. Causal nets represent the precedences in an ideal way. Inter-group tasks require a special treatment that we provide by extending causal nets with synchronous channels. Based on reference nets, an additional system net facilitates the synchronization of the extended causal nets. Our special kind of reference nets can be executed within our RENEW IDE. We map those causal nets to Network Planning Technique (NPT) diagrams to consider time aspects. Supported by a RENEW plugin we aggregate the separated groups’ diagrams to a global NPT diagram to calculate the projects’ critical path.
Beside the tool support for general project management, we present and discuss the support for agile and distributed soft- ware development projects. Our extensions preserve the efficient checking for consistent, partially ordered global project plans.