Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems

We discuss our experiences in building tools for software verification of autonomic systems developed with the Autonomic System Specification Language (ASSL). ASSL is a software framework that aims to assist developers of autonomic systems by providing a powerful combination of both notation and tools. One of the major objectives of the framework is to assure the correctness of the autonomic systems via inclusion of tools targeting consistency checking, model checking, and automatic test case generation. In this paper, we review our recent work on these tools.

A systematic way of defining variants of a modeling language is useful for adapting the language to domain or project specific needs. Variants can be obtained by adapting the syntax or semantics of the language. In this paper, we take a formal approach to define modeling language variability and show how this helps to reason about language variants, models, and their semantics formally. We introduce the notion of semantic language refinement meaning that one semantics variant is implied by another. Leaving open all variation points that a modeling language offers yields the notion of the inner semantics of that language. Properties of the modeling language which do not depend on the selection of specific variants are called invariant language properties with respect to a variation point. These properties consequently follow from the inner semantics of a model or language.

Design space exploration (DSE) refers to the activity of exploring design alternatives prior to implementation. The power to operate on the space of potential design candidates renders DSE useful for many engineering tasks, including rapid prototyping, optimization, and system integration. The main challenge in DSE arises from the sheer size of the design space that must be explored. Typically, a large system has millions, if not billions, of possibilities, and so enumerating every point in the design space is prohibitive. In this paper, we present a method for systematically exploring the design space in a cost-effective manner. The key idea is that many of the design candidates may be considered equivalent as far as the user is concerned, and so only a small subset of the space needs to be explored. Our approach takes the user-defined notion of equivalence, and generates symmetry breaking predicates to ensure that the underlying exploration engine does not sample multiple equivalent design candidates. We describe how the method is integrated into our DSE framework, FORMULA, which uses an SMT solver to solve a set of global design constraints and search for valid design instances.

This paper presents an approach for incrementally adjusting the timing behavior of legacy real-time software according to explicit timing specifications expressed in the Timing Definition Language (TDL). The main goals of such a migration are ensuring predictability of the timing behavior, and enabling adaptivity of the system. The latter is particularly important for embedded control systems which adapt their computational load in accordance to parameters of the physical environment in which they operate.

Our approach entails a minimal instrumentation of the original code combined with an automatically generated runtime system, which ensures that the executions of designated periodic computations in the legacy software satisfy the logical execution time specifications of the TDL model. The presented approach has been applied to a complex legacy controller system in the automotive domain.

Self-caring systems are systems capable of monitoring and managing their own health and, indirectly, their useful lifetime. Unlike self-healing systems which are reactive to faults and failures, self-caring systems are aware of their health and hence can potentially circumvent and adapt to impending faults, or recover from them quicker and more effectively. Towards a methodology to model and incorporate health management logic and control mechanisms into an Information Technology (IT) system whose health needs to be managed, we propose the following: 1. the use of Petri nets as a discrete event system (DES) graphical model that can also be used for analysis, simulation and execution control, 2. the use of Remaining-Useful-Life (RUL) management and prognosis as a novel way of looking at health management in IT systems 3. the use of a control theoretic framework for RUL management. As a simple illustration of the concept, a controller was built for useful life management in the application execution stage (containing a potential memory exhaustion fault) of an IT system.

Modular and self-reconfigurable robots are a powerful way to design versatile systems that can adapt themselves to different physical environment conditions. Self-reconfiguration is not an easy task since there are numerous possibilities of module organization. Moreover, some module organizations are equivalent one to another.

In this paper, we apply symbolic representation techniques from model checking to provide an optimized representation of all configurations for a modular robot. The proposed approach captures symmetries of the system and avoids storing all the equivalences generated by permuting modules, for a given configuration. From this representation, we can generate a compact symbolic configuration space and use it to efficiently compute the moves required for self-reconfiguration (i.e. going from one configuration to another). A prototype implementation is used to provide some benchmarks showing promising results.

Heuristics, simulation, artificial intelligence techniques and combinations thereof have all been employed in the attempt to make computer systems adaptive, context-aware, reconfigurable and self-managing. This paper complements such efforts by exploring the possibility to achieve runtime adaptiveness using mathematically-based techniques from the area of formal methods. It is argued that formal methods @ runtime represents a feasible approach, and promising preliminary results are summarised to support this viewpoint. The survey of existing approaches to employing formal methods at runtime is accompanied by a discussion of their challenges and of the future research required to overcome them.

Verification of complex systems specification often encounters the so-called state space explosion problem, which prevents exhaustive model-checking in many practical cases. Many techniques have been developed to counter this problem by reducing the state space, either by retaining a smaller number of relevant states, or by using a smart representation. Among the latter, modular state spaces [CP00, LP04] have turned out to be an efficient analysis technique in many cases [Pet05]. When the system uses a priority mechanism (e.g. timed systems [LP07]), there is increased coupling between the modules — preemption between modules can occur, thus disabling local events. This paper shows that the approach is still applicable even when considering dynamic priorities, i.e. priorities depending both on the transition and the current marking.

The problem frame approach allows to precisely pin the software development problems before starting to work on them, thus avoiding to solve the wrong problems. Furthermore, the problem frames allow to develop tailored methods and schematic solutions to handle the tasks required to solve the corresponding problems. In this paper we adopt this approach to study the problem of developing a large class of software systems able to translate in different ways some inputs in outputs (e.g., hybrid mail or big brothers filtering digital communications for suspicious words). Our interest in this kind of systems has been prompted by a cooperation with a big company producing systems of this kind and by their search of techniques and approaches to handle predictable and unpredictable changes. We want to investigate how and if the problem frame based approach will help to master the aspects relative to predictable and unpredictable changes in the context, in the domain and in the requirements. We thus present the Multi-Translation Frame.

This paper describes a framework currently under development for modelling, simulation, and verification of relay interlocking systems as used by the Danish railways. The framework is centred around a domain-specific language (DSL) for describing such systems, and provides (1) a graphical editor for creating DSL descriptions, (2) a data validator for checking that DSL descriptions follow the structural rules of the domain, (3) a graphical simulator for simulating the dynamic behaviour of relay interlocking systems, and (4) verification support for deriving and verifying safety properties of relay interlocking systems.

Adaptation brings with it challenges related to trust. Mission critical and safety related systems usually require very predictable and repeatable behavior in order to be deployed. However, adaptation can satisfy many of the newer requirements of these systems. Service oriented architectures that adapt can enhance robustness, yet they bring the issue of choosing which of several services to trust for a particular need. Some adaptive systems require human interaction or must observe their human users in order to effect the adaptation. Users must develop trust for these systems so that they feel their time and energy are not wasted and that the system will in fact yield increased efficiency and effectiveness. This paper discusses these challenges and suggests some solutions for ensuring trust in adaptive systems.

Safety cases have become popular, even mandated, in a number of jurisdictions that develop products that have to be safe. Prior to their use in software certification, safety cases were already in use in domains like aviation, military applications, and the nuclear industry. Argument based methodologies/approaches have recently become the cornerstone for structuring justification and evidence to support safety claims. We believe that the safety case methodology is useful for the software certification domain, but needs to be tailored, more clearly defined, and more appropriately structured in analogy with regulatory regimes in classical engineering disciplines. This paper presents a number of reasons as to why current approaches to safety cases do not satisfy essential attributes for an effective software certification process and proposes improvements based on lessons learned from other engineering disciplines. In particular, the safety case approach lacks the highly prescriptive and domain specific nature that can be seen in other engineering specialities, in terms of engineering and analysis methods to be applied in generating the relevant evidence. Safety case approaches and corresponding methods should aim to achieve the levels of precision and effectiveness of engineering methods underpinning regulatory regimes in other engineering disciplines.

This paper addresses improved principles for verification and validation to establish confidence in robustness of adaptive software systems, to include uncertainty with respect to cyber environment and dynamics of internal system configuration. It applies to component based systems with probabilistic decision making at multiple levels and bridges the gap between checking the correctness of a single component and validating systems composed of many components.