Abstract Interface theories based on Interface Automata (IA) are formalisms for the component-based specification of concurrent systems. Extensions of their basic synchronization mechanism permit the modelling of data, but are studied in more complex settings involving modal transition systems or do not abstract from internal computation. In this article, we show how de Alfaro and Henzinger’s original IA theory can be conservatively extended by shared memory data, without sacrificing simplicity or imposing restrictions. Our extension IA for shared Memory (IAM) decorates transitions with pre- and post-conditions over algebraic expressions on shared variables, which are taken into account by IA’s notion of component compatibility. Simplicity is preserved as IAM can be embedded into IA and, thus, accurately lifts IA’s compatibility concept to shared memory. We also provide a ground semantics for IAM that demonstrates that our abstract handling of data within IA’s open systems view is faithful to the standard treatment of data in closed systems.

Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based on recognizing the terminal strong components of the reduced state space and, if necessary, expanding the stubborn sets used in their roots. In an earlier study it was pointed out that if the system may execute a cycle consisting of only invisible actions and that cycle is concurrent with the rest of the system in a non-obvious way, then the method may be fooled to construct all states of the full parallel composition. This problem is solved in this study by a method that “freezes” the actions in the cycle. The new method also preserves fair testing equivalence, making it usable for the verification of many progress properties.

Abstract Over the past two decades, de Alfaro and Henzinger’s interface automata (IA) have become a popular formal framework for the component-based specification of concurrent systems. IA’s parallel composition assumes that a component may wait on inputs but never on outputs, implying that an output must be consumed immediately or a communication error occurs. By now, the literature contains a number of semantics for IA: linear-time semantics based on traces observing communication errors , quiescence and/or divergence , as well as branching-time semantics based on alternating simulation . This article surveys these semantics from Rob van Glabbeek’s linear-time branching-time perspective, which does not consider settings with communication errors. We shed light onto the subtleties implied by IA’s pruning of all behaviour that might lead a component to autonomously enter an error state, and investigate when exactly de Alfaro and Henzinger’s restriction of input-determinism is needed. In addition, we introduce several new semantics for IA, in particular the linear-time ready semantics and the branching-time ready simulation .

Testing preorders on component specifications ensure that replacing a specification by a refined one does not introduce unwanted behavior in an overall system. Considering deadlocks as unwanted, the preorder can be characterized by a failure semantics on Labeled Transition Systems (LTSs). In previous work, we have generalized this to Modal Transition Systems (MTSs) with a new, MTS-specific testing idea. In the present article, we generalize this idea further to DMTS, a subclass of disjunctive MTSs. On the one hand, the testing preorder can be characterized by the same failure semantics, and dMTS have no additional expressivity in our setting. On the other hand, the technical treatment is significantly harder and, surprisingly, the preorder is not compositional. Furthermore, we regard deadlocks and divergence (infinite unobservable runs) as unwanted and characterize the testing preorder with an unusual failure-divergence semantics. This preorder is already on LTSs strictly coarser—and hence arguably better—than the traditional failure-divergence preorder. It is a precongruence on dMTS, also for hiding, and much easier to handle than the deadlock-based preorder. It arises as well from a new variant of De Nicola’s and Hennessy’s must-testing.

With the aim to preserve deadlock freedom, we define a new refinement preorder for modal transition systems (MTSs), using an MTS-specific variant of testing inspired by De Nicola and Hennessy. We characterize this refinement with a kind of failure semantics and show that it “supports itself,” for example, in the sense of thoroughness—in contrast to standard modal refinements. We present a conjunction operator with respect to our new refinement, which is quite different from existing ones. It always returns an MTS—again in contrast to the case of modal refinement. Finally, we also consider De Nicola’s and Hennessy’s may- and must-testing, where the latter leads to a semantics that is also compositional for hiding.

The ninth International Conference on the Application of Concurrency to System Design (ACSD) was held in July 2009 in Augsburg, Germany.Following a tradition, Fundamenta Informaticae publishes a special issue with revised and extended versions of a selection of the best papers from ACSD.The current issue is the eighth special issue devoted to ACSD.ACSD serves as a forum for disseminating theoretical results with application potential and advanced methods and tools for the design of complex concurrent systems.The conference aims at cross-fertilizing both theoretical and applied research on the following topics:• design methods, tools and techniques based on models of computation and concurrency (dataflow models, communicating automata, Petri nets, process algebras, state charts, MSCs, etc.), (performance) analysis, verification, testing and synthesis;• hardware / software co-design, platform-based design, component-based design, refinement techniques, hardware / software abstractions, co-simulation and verification;

Resynthesis of handshake specifications obtained e.g. from BALSA or TANGRAM with speed-independent logic synthesis from STGs is a promising approach. To deal with state-space explosion,we suggested STG decomposition; a problemis that decomposition can lead to irreducible CSC conflicts. Here, we present a new approach to solve such conflicts by introducing internal communication between the components. We give some first, very encouraging results for very large STGs concerning synthesis time and circuit area.

More than a decade ago, Moller and Tofts published their seminal work on relating processes that are annotated with lower time bounds, with respect to speed. Their paper has left open many questions concerning the semantic theory for their suggested bisimulation–based faster–than preorder, the MT–preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, and a convincing intuitive justification of the MT–preorder. This paper solves these difficulties by developing and employing novel tools for reasoning in discrete–time process algebra, in particular a general commutation lemma relating the sequencing of action and clock transitions. Most importantly, it is proved that the MT–preorder is fully–abstract with respect to a natural amortized preorder that uses a simple bookkeeping mechanism for deciding whether one process is faster than another. Together these results reveal the intuitive roots of the MT–preorder as a faster–than relation, while testifying to its semantic elegance. This lifts some of the barriers that have so far hampered progress in semantic theories for comparing the speed of processes. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.