We give two different notions of deadlock for systems based on active objects and futures. One is based on blocked objects and conforms with the classical definition of deadlock by Coffman, Jr. et al. The other one is an extended notion of deadlock based on blocked processes which is more general than the classical one. We introduce a technique to prove deadlock freedom of systems of active objects. To check deadlock freedom an abstract version of the program is translated into Petri nets. Extended deadlocks, and then also classical deadlock, can be detected via checking reachability of a distinct marking. Absence of deadlocks in the Petri net constitutes deadlock freedom of the concrete system.

We investigate deadlock detection for a modeling language based on active objects. To detect deadlock in an Actor-like subset of Creol we focus on the communication between the active objects. For the analysis of the model we translate a Creol configuration to a process algebra featuring the Linda coordination primitives. The translation preserves the deadlock behaviour of the model and allows us to apply a formalism introduced by Busi et al. (2000) [3] to detect global deadlocks in the process algebra.

This paper is an extended version of the Credo Methodology [16]. Credo offers tools and techniques to model and analyze highly reconfigurable distributed systems. In a previous version we presented an integrated methodology to use the Credo tool suite. Following a compositional, component–based approach to model and analyze distributed systems, we presented a separation of the system into components and the network. A high–level, abstract representation of the dataflow level on the network was given in terms of behavioral interface automata and a detailed model of the components in terms of Creol models. Here we extend the methodology with a detailed model of the network connecting these components. The Vereofy tool set is used to model and analyze the dataflow of the network in detail. The behavioral automata connect the detailed model of the network and the detailed model of the components. We apply the extended methodology to our running example, a peer-to-peer file-sharing system.

In this paper we investigate the synchronization of multithreaded call graphs with reentrance similar to call graphs in Java programs. We model the individual threads as Visibly Pushdown Automata (VPA) and analyse the reachability of a state in the product automaton by means of a Context Free Language (CFL) which captures the synchronized interleaving of threads. We apply this CFL-reachability analysis to detect deadlock.

We propose and explore a formal approach for black-box testing asynchronously communicating components in open environments. Asynchronicity poses a challenge for validating and testing components. We use Creol, a high-level, object-oriented language for distributed systems and present an interface specification language to specify components in terms of traces of observable behavior. The language enables a concise description of a component’s behavior, it is executable in rewriting logic and we use it to give test specifications for Creol components. In a specification, a clean separation between interaction under control of the component or coming from the environment is central, which leads to an assumption-commitment style description of a component’s behavior. The assumptions schedule the inputs, whereas the outputs as commitments are tested for conformance with the specification. The asynchronous nature of communication in Creol is respected by testing only up-to a notion of observability. The existing Creol interpreter is combined with our implementation of the specification language to obtain a specification-driven interpreter for testing.

This paper is an extended version of the Credo Methodology [16]. Credo offers tools and techniques to model and analyze highly reconfigurable distributed systems. In a previous version we presented an integrated methodology to use the Credo tool suite. Following a compositional, component based approach to model and analyze distributed systems, we presented a separation of the system into components and the network. A high level, abstract representation of the dataflow level on the network was given in terms of behavioral interface automata and a detailed model of the components in terms of Creol models. Here we extend the methodology with a detailed model of the network connecting these components. The Vereofy tool set is used to model and analyze the dataflow of the network in detail. The behavioral automata connect the detailed model of the network and the detailed model of the components. We apply the extended methodology to our running example, a peer-to-peer file-sharing system.

Credo offers tools and techniques to model and analyze highly reconfigurable distributed systems. In this paper, we present an integrated methodology to use the Credo tool suite. In this methodology, we advertise the use of top-down design, component-based modeling and compositional analysis to address the complexity of highly reconfigurable distributed systems. As a running example, we model a peer-to-peer file-sharing system and show how and when to apply the different modeling and analysis techniques of Credo.

We present a static technique for deadlock detection for active objects. To do so, we introduce a novel kind of automata (visibly multiset automata, VMAs for short) to describe in an approximative manner the behaviour of one active object resp. a deadlock scenario. In this setting deadlock detection is checking the intersection of the VMAs for emptiness. We illustrate our technique in terms of the Creol language.

This paper formalizes the observable interface behavior of a concurrent, object-oriented language with futures and promises. The calculus captures the core of Creol, a language, featuring in particular asynchronous method calls and, since recently, first-class futures.The focus of the paper are open systems and we formally characterize their behavior in terms of interactions at the interface between the program and its environment. The behavior is given by transitions between typing judgments, where the absent environment is represented abstractly by an assumption context. A particular challenge is the safe treatment of promises: the erroneous situation that a promise is fulfilled twice, i.e., bound to code twice, is prevented by a resource aware type system, enforcing linear use of the write-permission to a promise. We show subject reduction and the soundness of the abstract interface description. (C) 2009 Elsevier Inc. All rights reserved.

In this paper we give a representation of a weakest precondition calculus for abstract object creation in dynamic logic, the logic underlying the KeY theorem prover. This representation allows to both specify and verify properties of objects at the abstraction level of the (object-oriented) programming language. Objects which are not (yet) created never play any role, neither in the specification nor in the verification of properties. Further, we show how to symbolically execute abstract object creation.

Thread pools are often used as a pattern to increase the throughput and responsiveness of software systems. Implementations of thread pools may differ considerably from each other, which urges the need to analyze these differences in a formal manner. We use an object-oriented paradigm to model different thread pools in the context of the ASK system, an industrial communication platform. We use behavioral interfaces , high-level behavioral specifications for the objects, as a starting-point for analysis. Based on these behavioral interfaces, functional aspects are modeled in Creol, a high-level modeling language for concurrent objects. We use Uppaal to create real-time models and to perform schedulability analysis with respect to the behavioral interfaces. We finally check conformance between the real-time and Creol models using test-cases generated from the behavioral interfaces.

Since usually no scheduler is given at the programming or modeling language level, abstract models together with a refinement notion are necessary to model concurrent systems adequately. Deterministic transition systems are an appropriate model for implementations of (concurrent) reactive programs based on synchronous communication. In this paper, we develop a suitable setting for modeling and reasoning about deterministic transition systems. In particular, we (i) develop a class of abstract models together with a refinement notion; (ii) define parallel composition guaranteeing fairness; and (iii) develop a 3-valued logic with a satisfaction relation that is preserved under refinement.