In order to manage evolving organisational practice and maintain compliance with changes in policies and regulations, businesses must be capable of dynamically reconfiguring their business processes. However, such dynamic reconfiguration is a complex, human-intensive and error prone task. Not only must new business process rules be devised but also, crucially, the transition between the old and new rules must be managed. In this paper we present a fully automated technique based on formal specifications and discrete event controller synthesis to produce correct-by-construction reconfiguration strategies. These strategies satisfy user-specified transition requirements, be they domain independent - such as delayed and immediate change - or domain specific. To achieve this, we provide a discrete-event control theoretic approach to operationalise declarative business process specifications, and show how this can be extended to resolve reconfiguration problems. In this way, given the old and the new business process rules described as Dynamic Condition Response Graphs, and given the transition requirements described with linear temporal logic, the technique produces a control strategy that guides the organisation through a business process reconfiguration ensuring that all transition requirements and process rules are satisfied. The technique outputs a reconfiguration DCR whose traces reproduce the controller’s reconfiguration strategy. We illustrate and validate the approach using realistic cases and examples from the BPM Academic Initiative.

An important ability of self-adaptive systems is to be able to autonomously understand the environment in which they operate and use this knowledge to control the environment behaviour in such a way that system goals are achieved. How can this be achieved when the environment is unknown? Two phase solutions that require a full discovery of environment behaviour before computing a strategy that can guarantee the goals or report the non-existence of such a strategy (i.e., unrealisability) are impractical as the environment may exhibit adversarial behaviour to avoid full discovery. In this paper we formalise a control and discovery problem for reactive system environments. In our approach a strategy must be produced that will, for every environment, guarantee that unrealisablity will be correctly concluded or system goals will be achieved by controlling the environment behaviour. We present a solution applicable to environments characterisable as labeled transition systems (LTS). We use modal transition systems (MTS) to represent partial knowledge of environment behaviour, and rely on MTS controller synthesis to make exploration decisions. Each decision either contributes more knowledge about the environment's behaviour or contributes to achieving the system goals. We present an implementation restricted to GR(1) goals and show its viability.

Discrete event controllers are at the heart of many software systems that require continuous operation. Changing these controllers at runtime to cope with changes in its execution environment or system requirements change is a challenging open problem. In this paper we address the problem of dynamic update of controllers in reactive systems. We present a general approach to specifying correctness criteria for dynamic update and a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur and in which the underlying system architecture can reconfigure. Our solution uses discrete event controller synthesis to automatically build a controller that guarantees both progress towards update and safe update.

We contribute to recent efforts in relating two approaches to automatic synthesis, namely, automated planning and discrete reactive synthesis. First, we develop a declarative characterization of the standard "fairness" assumption on environments in non-deterministic planning, and show that strong-cyclic plans are correct solution concepts for fair environments. This complements, and arguably completes, the existing foundational work on non-deterministic planning, which focuses on characterizing (and computing) plans enjoying special "structural" properties, namely loopy but closed policy structures. Second, we provide an encoding suitable for reactive synthesis that avoids the naive exponential state space blowup. To do so, special care has to be taken to specify the fairness assumption on the environment in a succinct manner.

In this paper we present CLTSA (Counting Fluents Labelled Transition System Analyser), an extension of LTSA (Labelled Transition System Analyser) that incorporates counting fluents, a useful mechanism to capture properties related to counting events. Counting fluent temporal logic is a formalism for specifying properties of event-based systems, which complements the notion of fluent by the related concept of counting fluent. While fluents allow us to capture boolean properties of the behaviour of a reactive system, counting fluents are numerical values, that enumerate event occurrences.

The pervasiveness and growing complexity of software systems are challenging software engineering to design systems that can adapt their behavior to withstand unpredictable, uncertain, and continuously changing execution environments. Control theoretical adaptation mechanisms have received growing interest from the software engineering community in the last few years for their mathematical grounding, allowing formal guarantees on the behavior of the controlled systems. However, most of these mechanisms are tailored to specific applications and can hardly be generalized into broadly applicable software design and development processes. This article discusses a reference control design process, from goal identification to the verification and validation of the controlled system. A taxonomy of the main control strategies is introduced, analyzing their applicability to software adaptation for both functional and nonfunctional goals. A brief extract on how to deal with uncertainty complements the discussion. Finally, the article highlights a set of open challenges, both for the software engineering and the control theory research communities.

The problem of automatically constructing a software component such that when executed in a given environment satisfies a goal, is recurrent in software engineering. Controller synthesis is a field which fits into this vision. In this paper we study controller synthesis for partially observable LTS models. We exploit the link between partially observable control and non-determinism and show that, unlike fully observable LTS or Kripke structure control problems, in this setting the existence of a solution depends on the interaction model between the controller-to-be and its environment. We identify two interaction models, namely Interface Automata and Weak Interface Automata, define appropriate control problems and describe synthesis algorithms for each of them.

Fluent linear temporal logic is a formalism for specifying properties of event-based systems, based on propositions called fluents, defined in terms of activating and deactivating events. In this paper, we propose complementing the notion of fluent by the related concept of counting fluent. As opposed to the boolean nature of fluents, counting fluents are numerical values, that enumerate event occurrences, and allow us to specify naturally some properties of reactive systems. Although by extending fluent linear temporal logic with counting fluents we obtain an undecidable, strictly more expressive formalism, we develop a sound (but incomplete) model checking approach for the logic, that reduces to traditional temporal logic model checking, and allows us to automatically analyse properties involving counting fluents, on finite event-based systems. Our experiments, based on relevant models taken from the literature, show that: (i) counting fluent temporal logic is better suited than traditional temporal logic for expressing properties in which the number of occurrences of certain events is relevant, and (ii) our model checking approach on counting fluent specifications has an efficiency that is comparable to that of model checking equivalent fluent temporal logic specifications, while our approach scales better.

Most approaches for adaptive systems rely on models, particularly behaviour or architecture models, which describe the system and the environment in which it operates. One of the difficulties in creating such models is uncertainty about the accuracy and completeness of the models. Engineers therefore make assumptions which may prove to be invalid at runtime. In this paper we introduce a rigorous, tiered framework for combining behaviour models, each with different associated assumptions and risks. These models are used to generate operational strategies, through techniques such controller synthesis, which are then executed concurrently at runtime. We show that our framework can be used to adapt the functional behaviour of the system: through graceful degradation when the assumptions of a higher level model are broken, and through progressive enhancement when those assumptions are satisfied or restored.

Controller synthesis provides an automated means to produce architecture-level behaviour models that are enacted by a composition of lower-level software components, ensuring correct behaviour. Such controllers ensure that goals are satisfied for any model-consistent environment behaviour. This paper presents a tool for developing environment models, synthesising controllers efficiently, and enacting those controllers using a composition of existing third-party components. Video: www.youtube.com/watch?v=RnetgVihpV4.

We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behavior models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from environment assumptions. We show that assumptions must be modeled carefully in order to avoid synthesizing anomalous behavior models. We characterize nonanomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.

Existing software engineering techniques for automatic synthesis of event-based controllers have various limitations. In the context of the world/machine approach such limitations can be seen as restrictions in the expressiveness of the controller goals and domain model specifications or in the relation between the controllable and monitorable actions. In this thesis we aim to provide techniques that overcome such limitations, e.g. supporting more expressive goal specifications, distinguishing controllable from monitorable actions or guaranteeing achievement of the desired goals, among others. Hence, improving the state of the art in the synthesis of event-based controllers. Moreover, we plan to provide efficient tools supporting the developed techniques and evaluate them by modelling known case studies from the software engineering literature. Ultimately, showing that by allowing more expressiveness of controller goals and domain model specifications, and explicitly distinguishing controllable and monitorable actions such case studies can be more accurately modelled and solutions guaranteeing satisfaction of the goals can be achieved.

Constructing comprehensive operational models of intended system behavior is a complex and costly task, which can be mitigated by the construction of partial behavior models, providing early feedback and subsequently elaborating them iteratively. However, how should partial behavior models with different viewpoints covering different aspects of behavior be composed? How should partial models of component instances of the same type be put together? In this article, we propose model merging of modal transition systems (MTSs) as a solution to these questions. MTS models are a natural extension of labelled transition systems that support explicit modeling of what is currently unknown about system behavior. We formally define model merging based on weak alphabet refinement, which guarantees property preservation, and show that merging consistent models is a process that should result in a minimal common weak alphabet refinement (MCR). In this article, we provide theoretical results and algorithms that support such a process. Finally, because in practice MTS merging is likely to be combined with other operations over MTSs such as parallel composition, we also study the algebraic properties of merging and apply these, together with the algorithms that support MTS merging, in a case study.

We revisit synthesis of live controllers for event-based operational models. We remove one aspect of an idealised problem domain by allowing to integrate failures of controller actions in the environment model. Classical treatment of failures through strong fairness leads to a very high computational complexity and may be insufficient for many interesting cases. We identify a realistic stronger fairness condition on the behaviour of failures. We show how to construct controllers satisfying liveness specifications under these fairness conditions. The resulting controllers exhibit the only possible behaviour in face of the given topology of failures: they keep retrying and never give up. We then identify some well-structure conditions on the environment. These conditions ensure that the resulting controller will be eager to satisfy its goals. Furthermore, for environments that satisfy these conditions and have an underlying probabilistic behaviour, the measure of traces that satisfy our fairness condition is 1, giving a characterisation of the kind of domains in which the approach is applicable.

We present a novel technique for synthesising behaviour models that works for an expressive subset of liveness properties and conforms to the foundational requirements engineering World/Machine model, dealing explicitly with assumptions on environment behaviour and distinguishing controlled and monitored actions. This is the first technique that conforms to what is considered best practice in requirements specifications: distinguishing prescriptive and descriptive assertions. Most previous attempts at using synthesis of behavioural models were restricted to handling only safety properties. Those that did support liveness were inadequate for synthesis of operational event based models as they did not include the bespoke distinction between system goals and environment assumptions.

Modal transition systems (MTS) are operational models that distinguish between required and proscribed behaviour of the system to be and behaviour which it is not yet known whether the system should exhibit. MTS, in contrast with traditional behaviour models, support reasoning about the intended system behaviour in the presence of incomplete knowledge. In this paper, we present MTSA a tool that supports the construction, analysis and elaboration of Modal Transition Systems (MTS).