Self-Adaptive Software Needs Quantitative Verification at Runtime

Reference: Calinescu, R., Ghezzi, C., Kwiatkowska, M. & Mirandola, R. (2012). Self-Adaptive Software Needs Quantitative Verification at Runtime. Communications of the ACM 55(9): 69–77. DOI: 10.1145/2330667.2330686. URL

Summary

This paper argues that self-adaptive software must move a class of quantitative analysis from design time into runtime. Non-functional requirements — reliability, availability, performance, cost — are often stated probabilistically or in terms of expected costs/rewards, and the standard design-time way to establish them is quantitative (probabilistic) model checking over Markov models (DTMCs/MDPs, CTMCs) using tools such as PRISM. The authors’ thesis is that because the environment, workloads, and component behaviours a system actually meets are only known once it is running — and keep changing — the same quantitative verification must be re-run continuously, at runtime, to check whether requirements still hold and to guide adaptation when they do not.

Concretely, the approach keeps an operational stochastic model of the system as part of the Knowledge (a Models@run.time artefact), continuously updates its parameters from monitored data (e.g. observed failure rates, response times), and re-verifies the relevant probabilistic/reward properties against that model. When verification predicts a requirement violation, the results drive the Plan step — selecting a reconfiguration whose verified properties restore the guarantees. The chief engineering challenge the paper foregrounds is efficiency: full model checking is expensive, so runtime use demands incremental and parametric verification techniques so the analysis can keep pace with adaptation. The work is a cornerstone of the runtime-assurance agenda, giving self-adaptation continuous, evidence-based guarantees rather than one-off design-time certificates.

Key Ideas

Move quantitative verification from design time to runtime: continuously re-check probabilistic/reward requirements as conditions change.
Keep an operational stochastic model (DTMC/MDP/CTMC) in the system’s runtime knowledge, updated from monitored data.
Verification results drive adaptation: a predicted violation triggers selection of a reconfiguration with verified properties.
Targets non-functional requirements — reliability, performance, availability, cost — that are naturally quantitative.
Central obstacle is efficiency; needs incremental/parametric model checking to run within the MAPE-K loop’s time budget.

Connections

Conceptual Contribution

Claim: Because the conditions under which non-functional requirements must hold are known only at runtime and keep changing, quantitative (probabilistic) verification has to be performed continuously at runtime, not once at design time.
Mechanism: Maintain a parametric stochastic model of the system in the runtime knowledge base, update it from monitored data, and re-run quantitative model checking (reliability/performance/cost properties) to detect predicted violations and choose verified reconfigurations — using incremental/parametric techniques for efficiency.
Concepts introduced/used: Runtime Quantitative Verification, Runtime Assurance, Models@run.time, MAPE-K, Formal Verification
Stance: engineering / position + method
Relates to: A concrete realisation of the perpetual-assurance goal of Software Engineering for Self-Adaptive Systems - A Second Research Roadmap; the probabilistic counterpart to the model-based runtime formal methods of ActivFORMS - Active Formal Models for Self-Adaptation.

Backlinks

Linked Pages

ActivFORMS - Active Formal Models for Self-Adaptation

ActivFORMS: Active Formal Models for Self-Adaptation

Reference: Iftikhar, M. U. & Weyns, D. (2014). ActivFORMS: Active Formal Models for Self-Adaptation. In Proc. 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2014), ACM, pp. 125–134. DOI: 10.1145/2593929.2593944. URL

Summary

ActivFORMS (“Active FORmal Models for Self-adaptation”) is an approach in which a formal model of the feedback loop is not merely used to verify a design and then discarded, but is directly executed as the running adaptation logic. The feedback loop’s MAPE-K behaviour is specified as a network of timed automata; those automata are verified against the adaptation goals (using model checking, e.g. Uppaal), and then the same verified model is deployed and executed by a virtual machine that interprets the automata at runtime. Because the artefact that runs is the artefact that was verified, ActivFORMS closes the usual gap between a verified design and the code that actually executes.

The approach’s second contribution is on-the-fly change of the adaptation logic with guarantees: because the executing model is a first-class runtime object, a new (re-verified) feedback-loop model can be installed at runtime to change how the system adapts, extending assurance from the managed application to the manager itself. ActivFORMS is a flagship example of models@run.time used for assurance: the running formal model is simultaneously the system’s knowledge, its executable controller, and the object of verification. Weyns and collaborators later extended it with runtime goal management and statistical model checking, and it stands as a canonical answer to the roadmaps’ call for practical runtime assurance of self-adaptive systems.

Key Ideas

Executable verified models: specify the MAPE-K feedback loop as timed automata, verify them, then directly execute the verified model — no separate hand-coded controller.
A model-execution virtual machine interprets the automata at runtime, eliminating the design-to-code assurance gap.
On-the-fly adaptation of the adaptation logic: install a new, re-verified feedback-loop model at runtime with retained guarantees.
Extends assurance to the managing system, not just the managed application.
A leading instance of Models@run.time for assurance; later extended with runtime goal management and statistical model checking.

Connections

Conceptual Contribution

Claim: Assurance for self-adaptive systems is strongest when the verified formal model of the feedback loop is itself executed, so the running adaptation logic and the verified artefact are one and the same — and can be replaced at runtime with retained guarantees.
Mechanism: Model the MAPE-K loop as timed automata, model-check them against goals, and run the verified model on a model-execution virtual machine as a first-class Models@run.time object that can be swapped for a re-verified model on the fly.
Concepts introduced/used: Runtime Assurance, Models@run.time, MAPE-K, Formal Verification, Feedback Loop
Stance: engineering / framework
Relates to: The formal/model-based counterpart to the probabilistic Self-Adaptive Software Needs Quantitative Verification at Runtime; a concrete realisation of the perpetual-assurance agenda in Software Engineering for Self-Adaptive Systems - A Second Research Roadmap.

Software Engineering for Self-Adaptive Systems: A Second Research Roadmap

Reference: de Lemos, R., Giese, H., Müller, H. A., Shaw, M., et al. (2013). Software Engineering for Self-Adaptive Systems: A Second Research Roadmap. In Software Engineering for Self-Adaptive Systems II, LNCS 7475, Springer, pp. 1–32. DOI: 10.1007/978-3-642-35813-5_1. URL

Summary

The second SEAMS roadmap, produced four years after the first, takes stock of the field’s progress and re-sets the agenda around what the community had learned to be the genuinely hard problems. Where the first roadmap partitioned the space, this one is organised around four thematic challenges that had emerged as central: design space (systematically characterising the choices a designer of a self-adaptive system faces), processes (development and lifecycle processes that span design time and runtime), decentralisation of control loops (moving beyond a single MAPE-K loop to multiple, interacting control loops and coordination patterns among them), and practical run-time verification and validation (V&V).

The roadmap’s sharpest emphasis is on assurance: it argues that self-adaptive systems demand a continuous supply of evidence that requirements are still met as the system and its environment change, shifting V&V from a design-time gate to a runtime, incremental activity. It highlights the need to reason explicitly about the uncertainty that motivates adaptation, to make control loops (and their interactions) explicit architectural entities, and to develop perpetual assurance techniques — including quantitative and formal methods applied at runtime — that keep pace with adaptation. It is the standard “state of the field, part II” reference for engineering and assuring self-adaptive software.

Key Ideas

Four thematic challenges: design space, processes (design-time + runtime), decentralised control loops, and practical run-time V&V.
Decentralised control: self-adaptive systems increasingly need multiple interacting MAPE-K loops with explicit coordination, not one central loop.
Perpetual / runtime assurance: continuous, incremental evidence that goals still hold, replacing one-shot design-time verification.
Uncertainty is first-class: adaptation exists to handle it, so it must be modelled and reasoned about explicitly across the lifecycle.
Positions runtime quantitative verification and formal runtime models as key enabling techniques for assurance.

Connections

Conceptual Contribution

Claim: Four years on, the hard core of engineering self-adaptive systems is decentralised control, lifecycle processes spanning design/runtime, and — above all — continuous runtime assurance under uncertainty.
Mechanism: Reorganise the agenda around design space, processes, decentralisation of control loops, and practical run-time V&V; treat uncertainty as first-class and pursue perpetual assurance via runtime quantitative/formal verification.
Concepts introduced/used: Runtime Assurance, MAPE-K, Requirements Under Uncertainty, Feedback Loop, Runtime Quantitative Verification
Stance: roadmap / community agenda
Relates to: The sequel to Software Engineering for Self-Adaptive Systems - A Research Roadmap; its assurance emphasis is realised in Self-Adaptive Software Needs Quantitative Verification at Runtime and ActivFORMS - Active Formal Models for Self-Adaptation, and its decentralised-control theme extends the single loop of The Vision of Autonomic Computing.

In this vault

MAPE-K

The reference control loop of Autonomic Computing and self-adaptive software: an autonomic manager runs a closed feedback loop of Monitor → Analyse → Plan → Execute over a shared Knowledge base, acting on a managed element through sensors (probes/gauges) and effectors.

Monitor — collect and aggregate sensor data from the managed element and its environment.
Analyse — detect when adaptation is needed (symptoms, constraint/SLA violations, drift from goals).
Plan — select a course of action (a strategy/tactic, reconfiguration, or repair).
Execute — enact the plan through effectors on the managed element.
Knowledge — models, policies, goals, and history shared across the four phases (see Models@run.time).

Introduced in The Vision of Autonomic Computing (Kephart & Chess 2003) as the organising abstraction for the self-* properties (self-configuration, self-healing, self-optimisation, self-protection). It is the connective tissue linking architecture-based adaptation (Rainbow - Architecture-Based Self-Adaptation with Reusable Infrastructure), reference models (Three-Layer Reference Model), and the broader survey landscape (Self-Adaptive Software - Landscape and Research Challenges).

In this vault

Models@run.time

The principle that a self-adaptive system should keep a causally-connected, runtime-accessible model of itself (and often of its environment and goals) that both reflects the running system and can be used to reason about and drive adaptation. Where classic model-driven engineering uses models at design time, models@run.time extends abstract models into the running system as first-class artefacts that the adaptation logic queries and updates.

Such a runtime model is the natural home for the Knowledge in a MAPE-K loop: the Monitor phase keeps it in sync with reality, and the Analyse/Plan phases reason over it rather than over raw code. Architecture-based approaches like Rainbow - Architecture-Based Self-Adaptation with Reusable Infrastructure make the software architecture the runtime model against which constraints are evaluated and repairs planned.

Runtime Assurance

The provision of continuous, runtime evidence that a self-adaptive system still satisfies its requirements as the system, its environment, and its workload change — replacing (or supplementing) one-shot design-time verification with an incremental, always-on activity. Because self-adaptation defers decisions to runtime precisely to cope with uncertainty, the guarantees must be re-established at runtime too; the SEAMS roadmaps call this perpetual assurance and treat it as the field’s defining challenge.

Runtime assurance is realised through several complementary techniques in this vault: quantitative (probabilistic) verification at runtime (Self-Adaptive Software Needs Quantitative Verification at Runtime), executable verified formal models of the feedback loop (ActivFORMS - Active Formal Models for Self-Adaptation), and control-theoretic guarantees synthesised for the adaptation controller (Automated Design of Self-Adaptive Software with Control-Theoretical Formal Guarantees). All of them keep a runtime model in the MAPE-K knowledge base and re-check goals against it as conditions drift.

In this vault

Runtime Quantitative Verification

The application of quantitative (probabilistic) model checking — verifying reliability, performance, availability, and cost/reward properties over stochastic models such as discrete- and continuous-time Markov chains and Markov decision processes — continuously at runtime rather than only at design time. An operational stochastic model of the system is kept in the runtime knowledge as a Models@run.time artefact, its parameters are updated from monitored data, and the relevant properties are re-verified so that predicted requirement violations can trigger and guide adaptation.

Introduced as an agenda for self-adaptation by Self-Adaptive Software Needs Quantitative Verification at Runtime (Calinescu, Ghezzi, Kwiatkowska & Mirandola 2012), it is a central technique of Runtime Assurance. Its practicality hinges on efficiency — incremental and parametric verification methods that fit inside the adaptation loop’s time budget.

In this vault

Self-Adaptation

A system’s capability to modify its own behaviour or structure at runtime in response to internal or environmental change, without external intervention. It is typically implemented as a MAPE-K loop (Monitor-Analyse-Plan-Execute over a Knowledge base), the control abstraction introduced by Autonomic Computing.

In this vault

Runtime Verification

A lightweight verification technique in which a monitor checks at execution time whether the observed trace of a system satisfies a formal specification, raising alarms or triggering recovery on violation. It complements model checking by handling systems too large or open for exhaustive analysis.

Self-Adaptive Software Needs Quantitative Verification at Runtime

Summary

Key Ideas

Connections

Conceptual Contribution

Tags

Backlinks