This paper presents an approach to analyse the application of tactics in architectural patterns. We define and illustrate the approach using archery, a language for specifying, analysing and verifying architectural patterns. The approach consists of characterising the design principles of an architectural pattern as constraints, expressed in the language, and then, establishing a refinement relation based on their satisfaction. The application of tactics preserving refinement ensures that the original design principles, expressed themselves as constraints, still hold in the resulting architectural pattern. The paper focuses on fault-tolerance tactics, and identifies a set of requirements for a semantic framework characterising them. The application of tactics represented as model transformations is then discussed and illustrated using two case studies.

Spreadsheets are increasingly used as programming languages, in the construction of large and complex systems. The fact is that spreadsheets, being a highly flexible framework, lack important programming language features such as abstraction or encapsulation. This flexibility, however, comes with a price: spreadsheets are populated with significant amounts of errors. One of the approaches that try to overcome this problem advocates the use of model-driven spreadsheet development: a spreadsheet model is defined, from which a concrete spreadsheet is generated. Although this approach has been proved effective in other contexts, still it needs to accommodate for future evolution of both the model and its instance, so that they remain synchronized at all moments. In this paper, we propose a pair of transformation sets, one working at the model level and the other at the instance level, such that each transformation in one set is related to a transformation in the other set. With our approach, we ensure model/data compliance while allowing for model and data evolution.

Notable Byzantine Fault Tolerant protocols have been designed so far. These protocols are often evaluated on simple benchmarks, and few times on NFS systems. On the contrary, studies that addressed the behaviour of BFT on large back-ends, like Directories, are rare. We believe that studying such systems is crucial for practice community due to their popularity. In this paper, we integrate BFT with OpenLDAP Directory. We introduce the design of the integrated system, that we call BFT-LDAP. Then, we study its behaviour accompanied with some useful observations. In addition, we discuss the cost overhead of this integration. Our approach ensures that OpenLDAP legacy code remains completely intact, and that the integration with BFT is straightforward using APIs. Moreover, we convey that the additional performance cost of BFT-LDAP is negligible as compared to that of stand-alone OpenLDAP. We conducted our experiments on Emulab. The experiments indicate that the performance discrepancy of BFT-LDAP is negligible whenever different state-of-the-art BFT protocols are used. Other experiments demonstrate that a little sacrifice in throughput (less than 10%) is needed in order to leverage the resiliency of OpenLDAP against Byzantine faults (i.e., through applying BFT).

Design patterns provide a means to reuse proven solutions during development, but also to identify good practices during analysis. These are particularly relevant in complex and critical software, such as is the case of ubiquitous and pervasive systems. Model Driven Engineering (MDE) presents a solution for this problem, with the usage of high level models. As part of an effort to develop approaches to the migration of applications to mobile contexts, this paper reports on a tool that identifies design patterns in source code. Code is transformed into both platform specific and independent models, and from these design patterns are inferred. MapIt, the tool which implements these functionalities is described.

This paper takes a fresh look at the topic of trace semantics in the theory of coalgebras. The first development of coalgebraic trace semantics used final coalgebras in Kleisli categories, stemming from an initial algebra in the underlying category (see notably~\cite{HasuoJS07}). This approach requires some non-trivial assumptions, like dcpo enrichment, which do not always hold, even in cases where one can reasonably speak of traces (like for weighted automata). More recently, it has been noticed (see~\cite{SBBR10}) that trace semantics can also arise by first performing a determinization construction. In this paper, we develop a systematic approach, in which the two approaches correspond to different orders of composing a functor and a monad, and accordingly, to different distributive laws. The relevant final coalgebra that gives rise to trace semantics does not live in a Kleisli category, but more generally, in a category of Eilenberg-Moore algebras. In order to exploit its finality, we identify an extension operation, that changes the state space of a coalgebra into a free algebra, which abstractly captures determinization of automata. Notably, we show that the two different views on trace semantics are equivalent, in the examples where both approaches are applicable.

In concurrency theory, various semantic equivalences on la- belled transition systems are based on traces enriched or decorated with some additional observations. They are generally referred to as decorated traces, and examples include ready, failure, trace and complete trace equivalence. Using the generalized powerset construction, recently introduced by a subset of the authors (FSTTCS’10), we give a coalgebraic presentation of decorated trace semantics. This yields a uniform notion of canonical, minimal representatives for the various decorated trace equivalences, in terms of final Moore automata. As a consequence, proofs of decorated trace equivalence can be given by coinduction, using different types of (Moore-) bisimulation, which is helpful for automation.