PaperlayerView exact revision on arXiv

Source-linked AI summary

Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases

Radu Calinescu, Danny Weyns, Simos Gerasimou, M. Usman Iftikhar, Ibrahim Habli, Tim Kelly

arXiv:1703.06350v2cs.SE

TL;DR

Self-adaptive software must operate under uncertainty while satisfying strict requirements, yet existing assurance research often addresses only individual aspects rather than complete assurance cases. The paper introduces ENTRUST, which combines design-time and runtime modelling and verification with industry-adopted assurance arguments. Its tool-supported evaluation shows applicability across different domains and support for dynamic assurance-case generation, while the evaluation remains bounded by two systems and author-led research groups.

  • Problem

    Self-adaptive systems need assurance of correct operation under uncertainty and strict requirements, but research has often provided evidence only for individual aspects rather than complete assurance cases.

  • Method

    ENTRUST combines design-time and runtime modelling and verification with industry-adopted assurance processes to engineer self-adaptive systems and their assurance cases.

  • Results

    ENTRUST supports engineering trustworthy self-adaptive solutions across two different application settings and generating their dynamic assurance cases.

  • Takeaways & Limitations

    The methodology provides an end-to-end basis for developing verifiable controllers, design-time and runtime assurance evidence, and runtime assurance-argument instantiations.

  • Takeaways & Limitations

    The evaluation uses only two systems and was conducted by the authors’ three research groups.

Abstract

from arXiv · show

Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance. To address this need, we introduce a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware (ENTRUST). ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop trustworthy self-adaptive software and assurance cases arguing the suitability of the software for its intended application. To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop proof-of-concept self-adaptive software for embedded and service-based systems from the oceanic monitoring and e-finance domains, respectively. The experimental results show that ENTRUST can be used to engineer self-adaptive software systems in different application domains and to generate dynamic assurance cases for these systems.

1 INTRODUCTION

Self-adaptive software uses closed-loop control to respond to uncertainty, but applications with strict requirements need assurance that adaptations remain correct. ENTRUST addresses this gap through end-to-end engineering, verification, and dynamic assurance cases.

  • Motivation: Self-adaptive software monitors environmental and internal changes, then selects and applies revised architectures or parameters.Examples include workload variation, throughput changes, and component failures.
  • Motivation: Strict functional and non-functional requirements make assurance challenging in domains such as telehealth, manufacturing, and oceanic monitoring.The paper highlights the need to demonstrate correct operation under uncertain scenarios.
  • Research gap: Existing research often supplies evidence for individual self-adaptive components rather than complete assurance cases linking evidence to system-level claims.ENTRUST targets this discrepancy between research practice and established assurance processes.
  • ENTRUST: ENTRUST combines design-time and runtime modelling and verification with industry-adopted formalisation of assurance arguments.Design-time activities support controller enactment and partial assurance cases, while runtime activities address adaptation evidence.
  • Contributions: The methodology provides an end-to-end process for engineering self-adaptive software with assurance evidence and constructing assurance cases that integrate it.Its contributions include a self-adaptive-system assurance argument pattern expressed in GSN.
  • Evaluation: ENTRUST is instantiated with UPPAAL and PRISM and evaluated through two case studies from different application domains.The evaluation concerns proof-of-concept systems and reports effective engineering and assurance-case generation across the two settings.

2 PRELIMINARIES

Assurance cases connect structured arguments to evidence about system requirements, while GSN provides the notation for organising those relationships. The paper extends this approach with a reusable assurance argument pattern for self-adaptive software.

  • 2.1 Assurance Cases: An assurance case reports and supports a specific claim about a system’s requirements using evidence and structured arguments.The argument can connect evidence to the claim through intermediate claims.
  • 2.1 Assurance Cases: Assurance cases are developed throughout the system life cycle, with runtime evidence updating them during maintenance.For self-adaptive systems, existing evidence must be combined continuously with new adaptation evidence.
  • 2.2 Goal Structuring Notation: GSN represents claims as goals that are decomposed through strategies and sub-goals until supported by solutions containing assurance evidence.The notation also expresses contextual and evidential relationships among argument elements.
  • 2.2 Goal Structuring Notation: GSN arguments can organise complex assurance structures into modules and mark elements as uninstantiated or undeveloped pending concrete development.These markers distinguish reusable placeholders from argument content requiring further refinement.
  • 2.3 Assurance Argument Patterns: Assurance argument patterns reduce development effort by reusing generic GSN elements for a class of systems and scenarios.Pattern-specific entities are instantiated for each concrete assurance argument.
  • 2.3 Assurance Argument Patterns: The paper devises a new GSN assurance argument pattern applicable to self-adaptive software systems.The pattern extends the reusable-structure approach to this system class.

3 SELF-ADAPTIVE SYSTEM EXAMPLES

The paper presents two self-adaptive systems: an embedded UUV for ocean monitoring and a service-based FX trading system. Both dynamically adjust configurations to satisfy reliability, performance, safety, or optimisation requirements under changing conditions.

  • Systems: The examples comprise a self-adaptive UUV embedded system for oceanographic missions and a service-based FX system used by a European foreign exchange brokerage.The UUV adapts to operating-environment changes, while FX implements a workflow of market, analysis, alarm, and order services.
  • UUV system: The UUV cost function combines sensor energy use and speed through weights representing the relative importance of reduced battery usage and faster mission completion.The requirements use the cost function after throughput and resource-usage constraints are satisfied.
  • UUV system: If the UUV cannot identify a suitable configuration within 2 seconds after a sensor-rate change, it reduces speed to 0m/s until a configuration or new instructions become available.This safety requirement prevents the vehicle from advancing without appropriate measurements.
  • FX system: If FX cannot identify a configuration satisfying its first three requirements within 2s after service characteristics change, it bypasses the Order service.This prevents trades based on incorrect or stale data; the requirements differ qualitatively from those of the UUV system.

4 THE ENTRUST METHODOLOGY

ENTRUST systematically engineers and assures self-adaptive systems based on MAPE control loops. It relies on model-driven engineering and reuse of application-independent software and assurance artefacts to support trustworthy adaptation.

  • Scope: ENTRUST supports systematic engineering and assurance for self-adaptive systems based on monitor-analyse-plan-execute control loops.The methodology does not support systems based on essentially different control techniques, such as the cited control-theoretical paradigm.
  • Principles: Model-driven engineering underpins both design-time and runtime stages, with modelling, simulation, testing, and formal verification providing major sources of assurance evidence.Models describe the structure and behaviour of functional components, controlled systems, environments, and controllers.
  • Principles: Reusing application-independent software and assurance artefacts reduces the effort and expertise required to develop trustworthy self-adaptive systems.The methodology specifically reuses controller components and templates for developing application-specific artefacts.

4.1 Design-time ENTRUST Stages

The design-time ENTRUST stages develop verifiable models, establish controller assurance evidence, instantiate a partial assurance argument, assemble the controller, and prepare the deployed system. They combine application-specific modelling with reusable controller and assurance artefacts.

  • Stage 1: Stage 1 develops verifiable models for the controller, the relevant controlled software, and the environment.Structural and behavioural models may be selected according to the evidence needed for the assurance case, and can be checked through methods such as model checking or simulation.
  • Stage 1: ENTRUST reuses application-independent MAPE controller model templates containing placeholders for application-specific controller elements.Application-specific models require domain knowledge and are based on controlled-system specifications and system requirements.
  • Stage 1: Because self-adaptive systems contain uncertainty, design-time system and environment models may include unknown or estimated parameters, nondeterminism, or missing parts.These incomplete models support later runtime analysis as uncertainty is resolved.
  • Stage 2: Stage 2 verifies generic controller requirements and may also establish application-specific properties such as reachability of failsafe operating modes.Evidence can be generated through formal verification, theorem proving, or simulation, depending on the models and requirements.
  • Stage 3: Stage 3 uses controller evidence to partially instantiate a generic assurance argument, leaving runtime-dependent evidence placeholders unresolved.Design-time evidence can cover deadlock freedom and failsafe requirements, whereas other requirements may require runtime information.
  • Stages 4–5: The controller is assembled by integrating a verified controller platform with application-specific elements, sensors, and effectors, using trusted model-driven engineering.A model compiler or trusted virtual machine can generate or execute controller representations; the latter avoids generating controller code and additional assurances for it.
  • Stage 6: The final design-time stage installs, preconfigures, and activates the integrated system with deployment-specific parameters and architectural aspects.For the UUV, preconfiguration includes selecting the initial speed and active sensor set.

4.2 Runtime ENTRUST Stages

At runtime, ENTRUST uses a MAPE loop to resolve model uncertainties, analyse reconfiguration options, and produce adaptation assurance evidence. That evidence completes a dynamic assurance case for each active configuration and supports auditing and human oversight.

  • Runtime adaptation: The deployed system dynamically adjusts parameters and architecture as the MAPE loop monitors internal and environmental changes.Runtime observations resolve unknowns in incomplete system and environment models, enabling analysis of compliance with requirements.
  • Runtime assurance: Each reconfiguration produces adaptation assurance evidence about the correctness of the analysis results and the reconfiguration plan.Runtime verification, simulation, and runtime model checking may generate this evidence as a byproduct of analysis and planning.
  • Dynamic assurance case: The final runtime stage fills the partial assurance argument's remaining placeholders and creates a complete assurance case for the reconfigured system.The resulting case captures both the full assurance argument and the evidence justifying the active configuration.
  • Dynamic assurance case: Assurance-case versions for every reconfiguration let decision makers and auditors assess current and past cases and let human operators endorse major reconfiguration plans.This supports human-supervised self-adaptive systems in domains where supervision mitigates risk or may be required by regulation.

5 TOOL-SUPPORTED INSTANCE OF ENTRUST

This section introduces a tool-supported ENTRUST instance and uses the UUV system as a running example for describing its stages.

  • The section presents a tool-supported instance of ENTRUST and uses the UUV self-adaptive system throughout its stage descriptions.

5.1 Overview

The tool-supported ENTRUST instance combines reusable controller infrastructure with probabilistic verification, staged assurance development, runtime adaptation, and dynamic assurance-case synthesis.

  • The ENTRUST instance combines a Trusted Virtual Machine with a Probabilistic Verification Engine for executing controller models and verifying stochastic system models.
  • The Trusted Virtual Machine avoids model-to-text transformation, reducing a complex and error-prone operation while retaining assurance needs for the virtual machine.
  • The instance supports stochastic finite-state models including DTMCs, CTMCs, MDPs, and probabilistic automata, with unknown parameters resolved at runtime.
  • The methodology applies broadly because its modelling, verification, and evidence-generation methods are not prescriptive, and it targets systems with stochastic behaviour and non-functional requirements expressible in supported logics.
  • ENTRUST proceeds through controller modelling, UPPAAL verification, partial GSN assurance instantiation, controller enactment, deployment, runtime adaptation, and dynamic assurance synthesis.
  • During adaptation, monitoring updates stochastic models, analysis searches for compliant configurations, planning creates reconfiguration steps, and execution applies them or selects a failsafe.

5.2 Stage Descriptions

The stage descriptions specialise reusable MAPE templates and stochastic models, verify controller behaviour, and evolve assurance arguments as runtime adaptations produce new evidence.

  • 5.2.1 Development of Verifiable Models: ENTRUST provides event-triggered and time-triggered MAPE controller templates, with event-triggered monitors activated by sensor signals announcing system or environmental changes.
  • 5.2.1 Development of Verifiable Models: System specialisation replaces signal placeholders, defines guard and action functions, and implements application-specific automaton regions.
  • 5.2.1 Development of Verifiable Models: The UUV instantiation monitors new measurement rates, invokes runtime verification when analysis is required, and selects a minimum-cost configuration satisfying R1 and R2.
  • 5.2.1 Development of Verifiable Models: The UUV stochastic model composes sensor models in parallel, represents measurement and energy events, and specifies QoS requirements using CSL.
  • 5.2.2 Verification of Controller Models: UPPAAL verification does not use compositional checking because application-specific automaton elements are larger and would add assumption complexity without noticeable verification-time reduction.
  • 5.2.3 Partial Instantiation of Assurance Argument Pattern: ENTRUST dynamically evolves GSN assurance arguments because adaptation changes design features, code elements, claims, and evidence during runtime.
  • 5.2.6 Self-Adaptation: For the UUV, configuration (x1, x2, x3, sp) = (1, 1, 0, 3.2) is selected and runtime verification evidence fully instantiates the assurance argument for R1–R3.

5.3 Self-Adaptive Service-Based System

The FX case applies ENTRUST to a service-based workflow whose implementations vary in reliability, response time, and price, enabling runtime reconfiguration and updated assurance arguments.

  • Development and enactment: The FX system specialises ENTRUST’s event-triggered MAPE templates and implements FX-specific planner, executor, sensor, effector, and verification-engine components.
  • Runtime modelling: Its parametric DTMC models workflow branches with fixed probabilities and service outcomes with runtime-dependent probabilities, prices, and response times.
  • UUV comparison: For the UUV case, 147 alternative configurations are evaluated across seven sensor combinations and 21 speeds, with requirement violations shown as shaded regions.
  • Requirements and verification: The FX requirements use rewards-augmented PCTL for R1–R3 and CTL for the failsafe requirement R4.
  • Deployment: The prototype selects among two functionally equivalent implementations for each of six services, yielding 12 web services with differing characteristics.
  • Self-adaptation and assurance: When service characteristics change, the controller re-verifies configurations, selects the feasible lowest-cost option, plans reconfiguration, and updates the assurance argument with new runtime evidence.

6 EVALUATION

The evaluation examines ENTRUST’s correctness, efficiency, and generality using two self-adaptive systems and finds that it makes appropriate adaptation decisions, generates valid dynamic assurance cases, and supports different application domains. Runtime verification overhead is acceptable for the evaluated systems, although scalability and external validity remain bounded.

  • Evaluation methodology: The evaluation engineers two self-adaptive systems with ENTRUST controllers and partially instantiated assurance arguments, then assesses correctness, efficiency, and generality.The evaluation uses systems from different domains and examines whether adaptation decisions and assurance cases are valid, whether overhead is acceptable, and whether the approach generalizes.
  • RQ1 Correctness: A fixed UUV configuration violates throughput requirements during sensor degradation, including intervals with only 13, 15, or 7 measurements per 10m instead of 20.The result illustrates why adaptation is needed when environmental or component conditions change.
  • RQ1 Correctness: A fixed FX configuration can violate reliability for extended periods, while switching to a more expensive service can instead violate the cost requirement.The example shows the trade-off between meeting reliability and cost requirements under service degradation.
  • RQ1 Correctness: ENTRUST’s assurance cases support requirements through active configurations or reconfiguration while maintaining a failsafe mechanism.The cases are assessed using formal design-time and runtime evidence, with runtime monitoring and continuous verification challenging their validity using operational data.
  • RQ1 Correctness: The experiments provide strong empirical evidence that ENTRUST makes the right adaptation decisions and generates valid assurance cases.The conclusion is explicitly qualified by the limitations described in the evaluation.
  • RQ2 Efficiency: Runtime verification overheads remain below 10ms for UUV configurations and below 30ms for FX configurations, with failsafe configurations available during reverification.The corresponding runtime probabilistic model-checking values are below 1.5s and 2s for the two systems.
  • RQ2 Efficiency: Runtime CPU time increases exponentially with system size and the number of alternative configurations, making the current implementation suitable for systems with up to hundreds of configurations.The authors identify compositional, incremental, caching-lookahead, distributed, and metaheuristic approaches as possible routes to larger configuration spaces.
  • RQ3 Generality: Evidence for the two systems combines testing, model checking, and probabilistic model checking, indicating applicability across application domains.The evaluation covers an embedded UUV system and a service-based FX system, but additional areas require evaluation.

7 RELATED WORK

Existing assurance approaches for self-adaptive systems typically provide evidence for particular components or adaptation properties, while ENTRUST integrates such evidence into an end-to-end methodology with assurance arguments.

  • Assurance scope: Assurance for systems with strict requirements must cover the platform, controller functions, runtime decisions, engineering process, tools, and reusable components.It must also integrate the resulting evidence into a comprehensible and valid assurance argument that the requirements are satisfied.
  • Existing assurance techniques: Testing, formal proof, model checking, and simulation provide assurance evidence for selected properties, controllers, adaptation functions, or actions.Examples include robustness testing, safety and liveness proofs, reachable-state verification, and simulation-based analysis.
  • ENTRUST: ENTRUST combines complementary assurance evidence and integrates it systematically rather than treating individual evidence sources in isolation.Its contribution is an end-to-end methodology that includes development of assurance arguments for trustworthy self-adaptive systems.
  • Runtime assurance: ENTRUST extends runtime certification by dynamically evolving assurance arguments and evidence from runtime verification data, beyond monitoring assurance-case assumptions.The approach contrasts with runtime certification, which proactively monitors assumptions for early warnings.
  • Limits of existing work: Existing approaches generally focus on particular aspects of adaptation rather than integrating assurance across the complete self-adaptive system.The surveyed work commonly addresses controller functions, runtime decisions, adaptation effects, or other individual components.

8 CONCLUSION

The paper presents ENTRUST as an end-to-end methodology for engineering trustworthy self-adaptive software and dynamically generating assurance cases. Future work will evaluate usability, extend runtime verification, reduce overhead, and assess additional domains.

  • Conclusion: ENTRUST provides methods for verifiable controllers, design-time and runtime assurance evidence, and runtime instantiation of a system-specific assurance argument.The tool-supported instance targets trustworthy self-adaptive software systems.
  • Future work: Future work includes a controlled usability evaluation, runtime model checking of functional requirements, and reduction of runtime overheads.The proposed overhead reductions would exploit advances in probabilistic model checking at runtime.
  • Future work: The applicability of ENTRUST to additional systems and application domains remains a planned research direction.The paper identifies broader validation beyond the demonstrated settings as future work.
Loading 1703.06350v2…