Search

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.

Lists the reviewers who contributed to this publication in 2023.

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.

System specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where they are able to provide yes/no answers to queries regarding their temporal properties. Probabilistic modelling and checking aim at enriching this binary, qualitative information with quantitative information, more suitable to approaches such as reliability engineering. Compositional construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour to then analyse the composite system behaviour. Compositional construction also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. These component models are smaller and thus easier to validate. Compositional construction poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular the behaviour of other system components. Thus, the validity of compositionally constructed system specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support specification of non-deterministic and probabilistic component behaviour which, when observed through logics such as pCTL, is preserved in the composite system. In this paper we present a probabilistic extension to Interface Automata which preserves pCTL properties under probabilistic fairness by ensuring a probabilistic branching simulation between component and composite automata. The extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, that supports delayed synchronisation that may be required because of internal component behaviour. These results are equally applicable as an extension to non-probabilistic Interface Automata.

Fluent model checking is an automated technique for verifying that an event-based operational model satisfies some state-based declarative properties. The link between the event-based and state-based formalisms is defined through "fluents" which are state predicates whose value are determined by the occurrences of initiating and terminating events that make the fluents values become true or false, respectively.The existing fluent temporal logic is convenient for reasoning about untimed event-based models but difficult to use for timed models. The paper extends fluent temporal logic with temporal operators for modelling timed properties of discrete-time event-based models. It presents two approaches that differ on whether the properties model the system state after the occurrence of each event or at a fixed time rate. Model checking of timed properties is made possible by translating them into the existing untimed framework.

As a popular means for capturing behavioural requirements, scenarios show how components interact to provide system-level functionality. If component reliability information is available, scenarios can be used to perform early system reliability assessment. In previous work we presented an automated approach for predicting software system reliability that extends a scenario specification to model (1) the probability of component failure, and (2) scenario transition probabilities. Probabilistic behaviour models of the system are then synthesized from the extended scenario specification. From the system behaviour model, reliability prediction can be computed. This paper complements our previous work and presents a sensitivity analysis that supports reasoning about how component reliability and usage profiles impact on the overall system reliability. For this purpose, we present how the system reliability varies as a function of the components reliabilities and the scenario transition probabilities. Taking into account the concurrent nature of component-based software systems, we also analyse the effect of implied scenarios prevention into the sensitivity analysis of our reliability prediction technique.

Constructing rigorous models for analysing the behaviour of concurrent and distributed systems is a complex task. Our aim is to facilitate model construction. Scenarios provide simple, intuitive, example based descriptions of the behaviour of component instances in the context of a simplified architecture instance. The specific architecture instance is generally chosen to provide sufficient context to indicate the expected behaviour of particular instances of component types to be used in the real system. Existing synthesis techniques provide mechanisms for building behaviour models for these simplified and specific architectural settings. However, the behaviour models required are those for the full generality of the system architecture, and not the simplified architecture used for scenarios. In this paper we exploit architectural information in the context of behaviour model synthesis from scenarios. Software architecture descriptions give the necessary contextual information so that component instance behaviour can be generalised to component type behaviour. Furthermore, architecture description languages can be used to describe the complex architectures in which the generalised behaviours need to be instantiated. Thus, architectural information used in conjunction with scenario-based model synthesis can support both model construction and elaboration, where the behaviour derived from simple architecture fragments can be instantiated in more complex ones.

Constructing comprehensive operational models of intended system behaviour is a complex and costly task. Consequently, practitioners have adopted techniques that support incremental elaboration of partial behaviour descriptions. A noteworthy example is the wide adoption of scenario-based notations such as message sequence charts. Scenario-based specifications are partial descriptions that can be incrementally elaborated to cover the system behaviour that is of interest. However, how should partial behavioural models described by different stakeholders with different viewpoints covering different aspects of behaviour be composed? How should partial models of component instances of the same type be put together. In this paper, we propose model merging as a general solution to these questions. We formally define model merging based on observational refinement and show that merging consistent models is a process that should result in a minimal common refinement. Because minimal common refinements are not guaranteed to be unique, we argue that the modeller should participate in the process of elaborating such a model. We also discuss the role of the least common refinement and the greatest lower bound of all minimal common refinements in this elaboration process. In addition, we provide algorithms for i) checking consistency between two models; ii) constructing their least common refinement if one exists; iii) supporting the construction of a minimal common refinement if there is no least common refinement.

Scenario-based specifications such as Message Sequence Charts (MSCs) are popular for requirement elicitation and specification. MSCs describe two distinct aspects of a system: on the one hand they provide examples of intended system behaviour and on the other they outline the system architecture. A mismatch between architecture and behaviour may give rise to implied scenarios. Implied scenarios occur because a component's local view of the system state is insufficient to enforce specified system behaviour. An implied scenario indicates a gap in the MSC specification that needs to be clarified. It may simply mean that an acceptable scenario has been overlooked and should be added to the scenario specification. Alternatively, it may represent an unacceptable behaviour which should be documented and avoided in the final implementation. Thus implied scenarios can be used to iteratively drive requirements elicitation. However, in order to do so, tools for coping with rejected implied scenarios are needed. The contributions of this paper are twofold. Firstly, we define a language for describing negative scenarios. Secondly, we complement existing implied scenario detection methods with techniques for accommodating negative scenarios.

Scenario-based specifications describe how independent components interact to provide system level behaviour. The specified system decomposition and system behaviour can give rise to implied scenarios, which are the result of specifying the global behaviour of a system that will be implemented component-wise. The existence of implied scenarios is an indication that further validation with stakeholders must be done. An implied scenario can be accepted or rejected by stakeholders indicating that the implied scenario is acceptable system behaviour or a situation that should be avoided. In consequence, implied scenarios can be used to iteratively drive requirement elicitation. However, in order to do so, we must be capable of detecting implied scenarios in the presence of rejected implied scenarios, in other words in the presence of behaviour constraints. The contribution of this paper is a technique for detecting implied scenarios in message sequence chart (MSC) specifications that can be used in conjunction with behaviour constraints. The technique is based on building a Coordinator component that forces system components to follow the same sequence of basic MSCs as they go through a high-level MSC. The result is a model that behaves as specified in the MSC but does not comply with the MSC architecture. The resulting model is not a proposed implementation, rather a precise model of specified behaviour that can be used in combination with constrained implementation models to detect further implied scenarios. [Copyright &y& Elsevier]

Scenario-based specifications such as Message Sequence Charts (MSCs) are becoming increasingly popular as part of a requirements specification. Scenario describe how system components, the environment and users work concurrently and interact in order to provide system level functionality. Each scenario is a partial story which, when combined with other scenarios, should conform to provide a complete system description. However, although it is possible to build a set of components such that each component behaves in accordance with the set of scenarios, their composition may not provide the required system behaviour. Implied scenarios may appear as a result of unexpected component interaction. In this paper, we present an algorithm that builds a labelled transition system (LTS) behaviour model that describes the closest possible implementation for a specification based on basic and high-level MSCs. We also present a technique for detecting and providing feedback on the existence of implied scenarios. We have integrated these procedures into the Labelled Transition System Analyser (LTSA), which allows for model checking and animation of the behaviour model.

We report here on the First PhD and Young Researchers Warm Up Symposium for the International Conference on Software Engineering 2017 that will be held in Buenos Aires, Argentina.