Pith. sign in

REVIEW 4 major objections 5 minor 55 references

ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read ActivFORMS claims that a self-adaptive system can get formal guarantees on its feedback loop at design time and preserve them at runtime by directly executing the verified models, while using statistical model checking to keep adaptation…

desk verdict A solid, honestly scoped engineering-methods paper that consolidates prior work into an end-to-end approach with a real IoT deployment; the formal-guarantee claim is real but explicitly conditional on a tested-only VM and stub models. read the letter →

arxiv 1908.11179 v3 pith:HSNW3RJX submitted 2019-08-29 cs.SE

Danny Weyns , M. Usman Iftikhar This is my paper · ORCID
classification cs.SE
keywords self-adaptivesystemsMAPE-Kfeedbacklooptimedautomatastatisticalmodelcheckingdesign-timeverificationexecutableruntimemodelsIoTadaptationgoalevolutionat
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that a self-adaptive system can get formal guarantees on its feedback loop without paying the runtime cost of exhaustive verification. The proposed approach, ActivFORMS, verifies the MAPE-K (monitor–analyze–plan–execute) feedback loop's behavior at design time, then executes the exact verified models at runtime through a trusted virtual machine. Adaptation decisions are made by statistical model checking, which trades a small, user-tunable loss of accuracy for much lower time and memory use than exhaustive quantitative verification. The approach also supports live updates of adaptation goals and feedback loop models, and the paper demonstrates all of this on a deployed IoT building-security network.

What carries the argument

The load-bearing mechanism is the direct execution of verified feedback loop models: MAPE models are specified as networks of timed automata, checked against correctness properties at design time using a model checker, and then run at runtime by a “trusted virtual machine” that interprets the same timed automata, avoiding manual model-to-code translation that would break the guarantees. A second mechanism is statistical model checking, which uses bounded simulation of stochastic timed-automata quality models to estimate each adaptation option's quality properties, with user-set accuracy and confidence parameters that trade quality of estimates against verification time.

What would settle it

Run the deployed feedback loop model against a fresh interference pattern that is not represented in the quality models but is within the paper's stated assumptions (e.g., a non-normal distribution of link signal-to-noise ratio), and observe whether the system still keeps average packet loss below the goal; if it systematically violates the goal, the claim that the approach achieves the adaptation goals in operation would be falsified. Alternatively, feed identical inputs to the virtual machine and to a reference timed-automata semantics engine and compare state traces; any divergence in guards, delays, or channel synchronizations would falsify the guarantee-preservation claim.

Watch

Extended reading notes

Core claim

The central discovery is that correctness of the feedback loop and efficiency of runtime adaptation can be combined: instead of verifying the whole self-adaptive system at runtime, ActivFORMS verifies the feedback loop model once at design time and then directly executes that very model, preserving the guarantees under the assumption that the execution engine is trustworthy. At runtime, adaptation options are evaluated with statistical model checking, which provides estimates of quality properties within a specified accuracy and confidence, and the paper shows experimentally on a 15-mote IoT network that this selects configurations meeting the goals (packet loss under 10%, minimized energy) in about 37 seconds on average, with about 27% energy savings versus over-provisioning. It further shows that an exhaustive runtime verifier cannot scale to this setting, and that a new latency goal can be added on-the-fly with the desired effect.

Load-bearing premise

The guarantees rest on the stub models used at design time being faithful stand-ins for the real probes, effectors, and verifier, and on the virtual machine and update manager executing timed automata exactly as the modeling language's semantics require; the paper supports both with testing, not proof.

Editorial extensions

If this is right

  • Design-time verification of the feedback loop becomes a practical, reusable step: for the deployed network, all twelve correctness properties were verified in about 1.5 seconds on average.
  • Runtime adaptation decisions can be made within a fraction of the adaptation cycle, and the accuracy/confidence settings give engineers a tunable knob between decision quality and time.
  • Statistical model checking enables scaling to networks where exhaustive runtime verification is infeasible (up to 25 motes and roughly 7,800 adaptation options in the paper's scalability tests).
  • Adding or changing an adaptation goal at runtime is feasible, and the experiment shows a latency goal can be added while packet-loss and energy goals remain close to their targets.
  • Compared to a conservative reference approach, satisfying the packet-loss goal can be achieved with substantial energy savings (about 27% in the deployment).

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same template-and-verify cycle could be reused across systems of the same family, effectively making formal feedback-loop correctness a library asset rather than a per-system proof effort.
  • Because the SMC accuracy/confidence parameters are explicit, an extension that tunes them online (e.g., tightening accuracy when the system is stable and loosening it during rapid change) is a natural and possibly direct improvement that the paper does not explore.
  • The approach's reliance on known distributions for uncertain variables suggests a boundary condition: actors with unknown or changing distribution shapes would need online distribution estimation or non-parametric simulation, which the paper does not cover.
  • Direct execution of verified models may enable safe dynamic replacement of individual MAPE components at runtime, moving toward compositional assurance that the paper only partly realizes with its whole-model update mechanism.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper presents ActivFORMS, an end-to-end, model-driven approach for engineering self-adaptive systems based on MAPE-K feedback loops. The approach has four stages: design-time modeling and verification of feedback loop models, deployment and direct execution of those models, runtime selection of adaptation options via statistical model checking, and on-the-fly evolution of adaptation goals and feedback loop models. The authors instantiate the approach in ActivFORMSi, which uses timed automata, Uppaal for design-time verification, Uppaal-SMC for runtime statistical model checking, a custom virtual machine for direct model execution, and an online update manager for dynamic goal changes. The evaluation is carried out on DeltaIoT, a real IoT network deployed at KU Leuven, and includes comparisons with an over-provisioning reference approach and with runtime quantitative verification (RQV) using PRISM. The paper claims three contributions: correct behavior of the feedback loop, efficient achievement of adaptation goals, and support for runtime changes of adaptation goals.

Significance. If the claims hold, the paper makes a useful contribution to the self-adaptive systems community by combining design-time correctness of the feedback loop with runtime statistical model checking and dynamic goal updates. Its strengths include a concrete property set (P1-P12), the use of standard tools (Uppaal, Uppaal-SMC, PRISM), a real deployed IoT testbed, public provision of artifacts and test reports, and a clear discussion of assumptions and limitations. The empirical comparison against both a practical baseline and a formal runtime verification approach is valuable, and the paper is honest about the model-level scope of its guarantees. The central risk is that the headline guarantee of correct feedback-loop behavior at runtime depends on two links that are tested but not formally established: the virtual machine's conformance to Uppaal semantics and the fidelity of the stub models used at design time. This is load-bearing because the paper explicitly claims that design-time guarantees are preserved at runtime by direct execution.

major comments (4)
  1. [§3.2.1, §3.2.3, §5.2] The central guarantee-preservation claim rests on the premise that the model execution engine executes the feedback loop model 'correctly, i.e., according to the semantics of the modeling language' (§3.2.1). Section 5.2 states that the trustworthiness of the virtual machine is obtained through extensive testing, not through formal proof. Given that the VM translates Uppaal XML into an internal task-graph representation with its own scheduling of guards, invariants, urgent/committed locations, broadcast synchronization, and time, this is a substantial semantic gap. The paper should either provide conformance evidence (for example, systematic differential testing of the VM against Uppaal on the published template models, with coverage metrics, or a semantic-preservation argument for the translation) or explicitly reword the guarantee claim to say that the design-time guarantees are preserved only if the engine is trusted, with testing being the current evidence.
  2. [§3.1.2, §5.1.3 (P10)] The correctness properties, including P10 (A[] !Effector.ResultsIncorrect), are verified against domain-specific stub models, but ActivFORMS does not prescribe how to ensure that these stubs comply with the behavior of the external elements they represent; Section 3.1.2 offers only general guidelines. This is load-bearing for the claim that ActivFORMS 'supports correctness of the behavior of the feedback loop.' The paper should state explicitly in the Stage I/II guarantee summaries, the abstract, and the conclusions that the correctness guarantees are scoped to the behavior space exercised by the stubs and to the assumption of stub fidelity. Ideally, it should also describe or reference a concrete conformance technique (e.g., model-based testing between stubs and the actual probe/effector interfaces) and report the evidence obtained for DeltaIoT.
  3. [§6.3, Fig. 21] The field comparison against the reference approach and RQV is central to the efficiency claim, but the paper does not report the number of independent 12-hour runs performed per condition or the run-to-run variability. Without that information, statements such as 'RQV realizes a slightly worse result' and 'ActivFORMSi significantly reduces energy consumption by about 27%' cannot be fully assessed. Please add the number of replications, per-condition means and standard deviations, and, if appropriate, a statistical test or effect-size measure. If only one run per condition was performed, the claims should be labelled as illustrative.
  4. [§6.4, Fig. 22] The scalability conclusion for a 25-mote network appears to be an extrapolation: the reported verification time is for one randomly selected adaptation option, and the total verification time is obtained by multiplying that mean by the number of options (7776). No end-to-end adaptation run under the 8-minute verification limit is reported for this configuration. The paper should state that this is an extrapolation, not a measured end-to-end result, and should discuss whether the relaxed settings (E=95%, A=90%, RSEM=1%) still satisfy the packet-loss requirement (R1: less than 10% average loss) with the required confidence.
minor comments (5)
  1. [§6.1] The statement that verification time 'increased with 55.1% to an average of 2.12 sec' is arithmetically inconsistent with the reported baseline of 1.55 sec; please correct the numbers or the percentage.
  2. [§6.5] The text says 'Figure 22 shows the test results' for the latency goal, but the latency results appear in Fig. 23; please fix the cross-reference.
  3. [§5.1.3] Property numbering is inconsistent: the list uses P1-P12, but the surrounding text refers to 'Pr1 to Pr7', 'Pr 8', and 'Pr 11'; please unify the notation.
  4. [§6.4] The formula for the number of adaptation options is garbled as '6 m 5'; please provide the exact expression, presumably 6^(m/5).
  5. [Fig. 9 caption] The normality statement based on a Shapiro-Wilk p-value of 0.06 should be phrased as 'failure to reject normality at the 0.05 significance level' rather than as an assertion of normality.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central claims are validated against a real IoT deployment and two baselines; VM/stub assumptions are explicit scoping limitations, not circular reductions.

full rationale

I walked the claimed derivation chain: design-time Uppaal verification of MAPE models against stubs, direct execution by the model execution engine, runtime SMC-based selection of adaptation options, and on-the-fly model updates. No equation in the paper is fitted to the measured QoS outcomes, and the final comparisons are made against the real DeltaIoT deployment plus a reference approach and RQV, not against the authors' own models. The offline calibration of SMC run counts ('we run simulations on a relevant set of samples ... and empirically determine the number of runs') determines an accuracy/confidence setting, not the packet-loss, energy, or latency results, so it is not a fitted input renamed as a prediction. Self-citations (e.g., templates from [G. de la Iglesia and Weyns 2015], VM details from [Iftikhar et al. 2016]) are numerous, but the paper re-verifies the concrete DeltaIoT MAPE models and reports verification times and state counts; the central claim does not reduce to the cited prior work. The two genuine gaps are explicitly stated scoping conditions rather than circular steps: the guarantee transfer depends on the engine executing models 'according to the semantics of the modeling language,' with trust 'obtained through extensive testing' (Sections 3.2.1 and 5.2), and stub-model fidelity is left to general guidelines ('ActivFORMS does not prescribe how to design these models and ensure compliance'). These are threats to validity of the runtime guarantee, not self-definitional reductions; P10 is checked on an effector stub, but the reported achieved QoS is measured on the deployed system. No load-bearing uniqueness theorem or imported ansatz appears. Score 0.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The approach depends on the fidelity of stub models, the correctness of the model execution engine, and valid stochastic assumptions. These are stated in the paper but not independently discharged; they are the price of the guarantee transfer.

free parameters (3)
  • SMC simulation run count per quality query = Not stated; determined offline per RSEM target, e.g., 30 runs for RSEM 0.5%
    Determined empirically via offline experiments on a sample of configurations (Section 5.3.1); directly controls runtime accuracy and adaptation time.
  • Link-specific SNR calibration parameters alpha and beta = Per-link values from field experiments before deployment
    Used to set transmission power so SNR >= 0; fitted before deployment (Section 5.1.1, Example 2).
  • Verification settings: accuracy E, confidence A, RSEM threshold = E.g., E=99%, A=90%, RSEM=0.5% in the main experiments
    User-chosen thresholds balance verification time and estimate quality; the paper evaluates their tradeoff but does not derive them from first principles.
assumptions (4)
  • domain assumption Stub models used at design time faithfully represent the external probes, effectors, and verifier behavior.
    Needed for verification results to transfer to operation; stated in Section 3.1.2.
  • domain assumption The model execution engine executes timed automata models correctly according to Uppaal semantics.
    Stage II guarantee scope (Section 3.2.3); the engine is 'trusted' based on testing, not formal proof.
  • domain assumption Uncertainty variables in runtime models have known or determinable probability distributions.
    Required for statistical model checking validity; stated in the assumptions list in the introduction.
  • standard math Statistical model checking inference (Chernoff-Hoeffding and sequential confidence intervals) is valid.
    Background from Uppaal-SMC and the Agha and Palmskog survey; standard.

how reviews work

0 comments
Cite this review

Pith. "Pith review of ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems." pith.science (2026). https://pith.science/paper/HSNW3RJX

@misc{pith2026190811179,
  author       = {Pith},
  title        = {Pith review of: ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HSNW3RJX}},
  note         = {Machine review of arXiv:1908.11179}
}
read the original abstract

Self-adaptation equips a computing system with a feedback loop that enables it dealing with change caused by uncertainties during operation, such as changing availability of resources and fluctuating workloads. To ensure that the system complies with the adaptation goals, recent research suggests the use of formal techniques at runtime. Yet, existing approaches have three limitations that affect their practical applicability: (i) they ignore correctness of the behavior of the feedback loop, (ii) they rely on exhaustive verification at runtime to select adaptation options to realize the adaptation goals, which is time and resource demanding, and (iii) they provide limited or no support for changing adaptation goals at runtime. To tackle these shortcomings, we present ActivFORMS (Active FORmal Models for Self-adaptation). ActivFORMS contributes an end-to-end approach for engineering self-adaptive systems, spanning four main stages of the life cycle of a feedback loop: design, deployment, runtime adaptation, and evolution. We also present ActivFORMS-ta, a tool-supported instance of ActivFORMS that leverages timed automata models and statistical model checking at runtime. We validate the research results using an IoT application for building security monitoring that is deployed in Leuven. The experimental results demonstrate that ActivFORMS supports correctness of the behavior of the feedback loop, achieves the adaptation goals in an efficient way, and supports changing adaptation goals at runtime.

Figures

Figures reproduced from arXiv: 1908.11179 by the authors.

Figure 1
Figure 1. Basic building blocks of a self-adaptive system with MAPKE-K feedback loop [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. The four stages of ActivFORMS: I. Model & Verify, II. Deploy, III. Verify & Adapt, and IV. Evolve [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Workflow of service-based health assistance system [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (21 more)
Figure 4
Figure 4. Figure 4: Examples models of the feedback loop for the health assistance system [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: Example of sub models to check the goal violation property of the health assistance system [PITH_FULL_IMAGE:figures/full_fig_p011_5.png]
Figure 6
Figure 6. Figure 6: ActivFORMS runtime architecture (runtime models are marked with [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: Example of an updated and a new runtime model to deal with a new goal in the health assistance system [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]
Figure 8
Figure 8. Figure 8: DeltaIoT system with network topology and example of a sensor [PITH_FULL_IMAGE:figures/full_fig_p016_8.png]
Figure 9
Figure 9. Figure 9: Profiles of uncertainties for one of the motes in Figure 8. [PITH_FULL_IMAGE:figures/full_fig_p017_9.png]
Figure 10
Figure 10. Figure 10: Reusable templates for specifying MAPE models [PITH_FULL_IMAGE:figures/full_fig_p022_10.png]
Figure 11
Figure 11. Figure 11: Two template instances for the MAPE models of DeltaIoT [PITH_FULL_IMAGE:figures/full_fig_p023_11.png]
Figure 12
Figure 12. Figure 12: Templates for probe and effector stubs [PITH_FULL_IMAGE:figures/full_fig_p024_12.png]
Figure 13
Figure 13. Figure 13: The model is used to estimate the packet loss for a given adaptation option, using the following query: [PITH_FULL_IMAGE:figures/full_fig_p028_13.png]
Figure 13
Figure 13. Figure 13: Quality model to estimate packet loss We consider two types of uncertainties: the traffic load generated by the different motes and the signal to noise ratio per link (SNR). For these uncertainties we need to assign values in the model before the verification starts. …
Figure 14
Figure 14. Figure 14: Decision making at a particular point in time with two adaptation goals [PITH_FULL_IMAGE:figures/full_fig_p030_14.png]
Figure 15
Figure 15. Figure 15: shows the quality model to estimate latency for DeltaIoT. (a) Mote (b) Gateway (c) System [PITH_FULL_IMAGE:figures/full_fig_p031_15.png]
Figure 16
Figure 16. Figure 16: Updated analyzer model for DeltaIoT to deal with latency [PITH_FULL_IMAGE:figures/full_fig_p032_16.png]
Figure 17
Figure 17. Figure 17: Selection of the best adaptation option with three adaptation goals. [PITH_FULL_IMAGE:figures/full_fig_p033_17.png]
Figure 18
Figure 18. Figure 18: Verification times for properties that check the correctness of the MAPE feedback loop [PITH_FULL_IMAGE:figures/full_fig_p034_18.png]
Figure 19
Figure 19. Figure 19: Tradeoff between accuracy and adaptation time with ActivFORMS [PITH_FULL_IMAGE:figures/full_fig_p035_19.png]
Figure 20
Figure 20. Figure 20: Impact of verification settings on quality properties (E: accuracy; A: confidence; R: RSEM) [PITH_FULL_IMAGE:figures/full_fig_p036_20.png]
Figure 21
Figure 21. Figure 21: Results for a DeltaIoT setting with 15 motes and two adaptation goals. [PITH_FULL_IMAGE:figures/full_fig_p037_21.png]
Figure 22
Figure 22. Figure 22: Time and memory results of the scalability tests for ActivFORMS and RQV (based on 100 runs for one [PITH_FULL_IMAGE:figures/full_fig_p037_22.png]
Figure 23
Figure 23. Figure 23: Impact of dynamically adding a latency goal [PITH_FULL_IMAGE:figures/full_fig_p038_23.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

55 extracted references · 33 canonical work pages

  1. [8]

    IEEE Transactions on Software Engineering (in print) (2018)

    Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases. IEEE Transactions on Software Engineering (in print) (2018). DOI:http://dx.doi.org/10.1109/TSE.2017.2738640 J. C´amara, R. de Lemos, and N. Laranjeiro et al

    arXiv 2018

  2. [13]

    Springer-Verlag, Berlin, Heidelberg, Chapter Software Engineering for Self-Adaptive Systems: A Research Roadmap, 1–26

    Software Engineering for Self-Adaptive Systems. Springer-Verlag, Berlin, Heidelberg, Chapter Software Engineering for Self-Adaptive Systems: A Research Roadmap, 1–26. DOI:http://dx.doi.org/10.1007/978-3-642-02161-9 1 B. Cheng et al

    work page doi:10.1007/978-3-642-02161-9

  3. [18]

    IEEE Communications Magazine 52, 12 (2014), 36–41

    6TiSCH: Deterministic IP-enabled Industrial Internet (of Things). IEEE Communications Magazine 52, 12 (2014), 36–41. N. Esfahani, E. Kouroshfar, and S. Malek

    work page 2014

  4. [19]

    In19th Symposium and the 13th European Conference on Foundations of Software Engineering

    Taming Uncertainty in Self-adaptive Software. In19th Symposium and the 13th European Conference on Foundations of Software Engineering. ACM, 234–244. DOI:http://dx.doi.org/10.1145/2025113.2025147 A. Filieri, H. Hoffmann, and M. Maggio

    arXiv

  5. [20]

    In 36th International Conference on Software Engineering

    Automated Design of Self-adaptive Software with Control-theoretical Formal Guarantees. In 36th International Conference on Software Engineering. ACM, 299–310. DOI:http://dx.doi.org/10.1145/2568225.2568272 A. Filieri, G. Tamburrelli, and C. Ghezzi

    arXiv

  6. [21]

    IEEE Transactions on Software Engineering 42, 1 (2016), 75–99

    Supporting Self-Adaptation via Quantitative Verification and Sensitivity Analysis at Run Time. IEEE Transactions on Software Engineering 42, 1 (2016), 75–99. DOI:http://dx.doi.org/10.1109/TSE.2015.2421318 D. G. de la Iglesia and D. Weyns

    arXiv 2016

  7. [22]

    ACM Transactions on Autonomous and Adaptive Systems 10, 3 (2015), 15:1–15:31

    MAPE-K Formal Templates to Rigorously Design Behaviors for Self-Adaptive Systems. ACM Transactions on Autonomous and Adaptive Systems 10, 3 (2015), 15:1–15:31. DOI:http://dx.doi.org/10.1145/2724719 D. Garlan, S. Cheng, and A. Huang et al

    doi:10.1145/2724719 2015

  8. [25]

    InSoftware Engineering for Adaptive and Self-Managing Systems

    DeltaIoT: A Self-adaptive Internet of Things Exemplar. InSoftware Engineering for Adaptive and Self-Managing Systems. IEEE Press, 76–82. DOI:http://dx.doi.org/10.1109/SEAMS.2017.21 U. Iftikhar and D. Weyns

    work page doi:10.1109/seams.2017.21 2017

Show all 55 references
  1. [26]

    In Software Engineering for Adaptive and Self-Managing Systems

    ActivFORMS: Active Formal Models for Self-adaptation. In Software Engineering for Adaptive and Self-Managing Systems. ACM, 125–134. DOI:http://dx.doi.org/10.1145/2593929.2593944 M. Jackson

  2. [30]

    InFuture of Software Engineering

    Self-Managed Systems: An Architectural Challenge. InFuture of Software Engineering. FOSE ’07. 259–268. DOI:http://dx.doi.org/10.1109/FOSE.2007.19 M. Kwiatkowska, G. Norman, and D. Parker

    2007 doi

  3. [31]

    DOI:http://dx.doi.org/10.1007/s100090050010 A

    Uppaal in a Nutshell.International Journal on Software Tools Technology Transfer1, 1-2 (1997), 134–152. DOI:http://dx.doi.org/10.1007/s100090050010 A. Legay, S. Sedwards, and L.M. Traonouez

    1997 doi

  4. [33]

    In Foundations of Software Engineering

    Proactive Self-adaptation Under Uncertainty: A Probabilistic Model Checking Approach. In Foundations of Software Engineering. ACM, 1–12. DOI:http://dx.doi.org/10.1145/2786805.2786853 L. Nahabedian, V . Braberman, and N. D’Ippolito et al

  5. [34]

    InSoftware Engineering for Adaptive and Self-Managing Systems

    Assured and Correct Dynamic Update of Controllers. InSoftware Engineering for Adaptive and Self-Managing Systems. ACM, 96–107. DOI:http://dx.doi.org/10.1145/2897053.2897056 U. Noreen, A. Bounceur, and L. Clavier

  6. [35]

    InInternational Conference on Advanced Technologies for Signal and Image Processing

    A study of LoRa low power and wide area network technology. InInternational Conference on Advanced Technologies for Signal and Image Processing. 1–6. DOI:http://dx.doi.org/10.1109/ATSIP.2017.8075570 P. Oreizy, N. Medvidovic, and R. Taylor

    2017

  7. [37]

    In 5th ACM/SPEC International Conference on Performance Engineering

    Uncertainties in the Modeling of Self-adaptive Systems: A Taxonomy and an Example of Availability Evaluation. In 5th ACM/SPEC International Conference on Performance Engineering . DOI:http://dx.doi.org/10.1145/2568088.2568095 F. Quin, D. Weyns, T. Bamelis, S. Singh Buttar, and...

  8. [38]

    ACM Transactions on Autonomous and Adaptive Systems 4, 2 (2009), 14:1–14:42

    Self-adaptive Software: Landscape and Research Challenges. ACM Transactions on Autonomous and Adaptive Systems 4, 2 (2009), 14:1–14:42. P. Sawyer, N. Bencomo, J. Whittle, E. Letier, and A. Finkelstein

    2009

  9. [39]

    In 2010 18th IEEE International Requirements Engineering Conference

    Requirements-Aware Systems: A Research Agenda for RE for Self-adaptive Systems. In 2010 18th IEEE International Requirements Engineering Conference. 95–103. S. Shevtsov, M. Berekmeri, D. Weyns, and M. Maggio

    2010

  10. [40]

    IEEE Transactions on Software Engineering (in print) (2017)

    Systematic Literature Review on Control-Theoretical Software Adaptation. IEEE Transactions on Software Engineering (in print) (2017). DOI:http://dx.doi.org/10.1109/TSE.2017.2704579 S. Shevtsov, M. U. Iftikhar, and D. Weyns

    2017

  11. [41]

    In International Workshop on Control Theory for Software Engineering

    SimCA vs ActivFORMS: Comparing Control- and Architecture-based Adaptation on the TAS Exemplar. In International Workshop on Control Theory for Software Engineering . ACM, 1–8. DOI:http://dx.doi.org/10.1145/2804337.2804338 V . E. Souza, A. Lapouchnian, K. Angelopoulos, and J. M...

  12. [44]

    In 39th International Conference on Software Engineering

    ProEva: Runtime Proactive Performance Evaluation Based on Continuous-Time Markov Chains. In 39th International Conference on Software Engineering. 484–495. DOI:http://dx.doi.org/10.1109/ICSE.2017.51 G. Su, Y . Feng, T. Chen, and D. S. Rosenblum

    2017 doi

  13. [45]

    IEEE Transactions on Software Engineering 42, 7 (July 2016), 623–639

    Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters. IEEE Transactions on Software Engineering 42, 7 (July 2016), 623–639. DOI:http://dx.doi.org/10.1109/TSE.2015.2508444 G. Tamura, N. Villegas, and H. M¨uller et al...

    2016

  14. [46]

    In Formal Methods and Testing, R

    Model Based Testing with Labelled Transition Systems. In Formal Methods and Testing, R. Hierons, J. Bowen, and M. Harman (Eds.). Springer-Verlag, 1–38. http://dl.acm.org/citation.cfm?id=1806209.1806210 F. Trollmann, J. Faehndrich, and S. Albayrak

  15. [47]

    In Software Engineering for Adaptive and Self-Managing Systems

    Hybrid Adaptation Policies, Towards a Framework for Classification and Modelling of Different Combinations of Adaptation Policies. In Software Engineering for Adaptive and Self-Managing Systems. ACM. Y . Vandewoude. 2007.Dynamically Updating Component-Oriented Systems. Ph.D. Di...

    2007

  16. [48]

    ACM Transactions on Autonomous and Adaptive Systems (TAAS) 8, 4 (2014), 18:1–18:33

    Model-Driven Engineering of Self-Adaptive Software with EUREMA. ACM Transactions on Autonomous and Adaptive Systems (TAAS) 8, 4 (2014), 18:1–18:33. DOI:http://dx.doi.org/10.1145/2555612 D. Weyns

    2014 doi

  17. [50]

    InSoftware Engineering for Adaptive and Self-Managing Systems

    Tele Assistance: A Self-adaptive Service-based System Examplar. InSoftware Engineering for Adaptive and Self-Managing Systems. IEEE Press, 88–92. http://dl.acm.org/citation.cfm?id=2821357.2821373 D. Weyns and M. U. Iftikhar

  18. [51]

    In Models at Runtime, International Conference on Autonomic Computing

    Model-Based Simulation at Runtime for Self-Adaptive Systems. In Models at Runtime, International Conference on Autonomic Computing. 364–373. DOI:http://dx.doi.org/10.1109/ICAC.2016.67 D. Weyns, M. U. Iftikhar, D. G. de la Iglesia, and T. Ahmad. 2012a. A Survey of Formal Method...

    2016

  19. [52]

    In Software Engineering for Adaptive and Self-Managing Systems

    Do External Feedback Loops Improve the Design of Self-adaptive Systems? A Controlled Experiment. In Software Engineering for Adaptive and Self-Managing Systems . IEEE Press, 3–12. http://dl.acm.org/citation.cfm?id= 2487336.2487341 D. Weyns, S. Malek, and J. Andersson. 2012b. F...

    2012

  20. [53]

    In 17th International Requirements Engineering Conference, RE

    RELAX: Incorporating Uncertainty into the Specification of Self-Adaptive Systems. In 17th International Requirements Engineering Conference, RE . IEEE Computer Society, 79–88. DOI:http://dx.doi.org/10.1109/RE.2009.36 H. Younes

    2009 doi

  21. [54]

    In28th International Conference on Software Engineering

    Model-based Development of Dynamically Adaptive Software. In28th International Conference on Software Engineering. ACM, 371–380. DOI:http://dx.doi.org/10.1145/1134285.1134337 ACM Transactions on Software Engineering and Methodology, V ol. X, No. X, Article X, Pub. date: January

  22. [55]

    2004] to create feedback loop models

    ActivFORMS: A Model-Based Approach to Engineer Self-Adaptive Systems with Guarantees X:47 Appendix A: Uppaal Language Grammar ActivFORMSi uses the Uppaal model checker [Behrmann et al. 2004] to create feedback loop models. This appendix summarizes the grammar of the C-like mod...

    2004

  23. [56]

    int mote2Id = 2; mote3Id = 2

    ActivFORMS: A Model-Based Approach to Engineer Self-Adaptive Systems with Guarantees X:49 } Qualities type struct { int motesLoad[MAX_MOTES]; int linksSNR[MAX_LINKS]; } Environment type struct { ManagedSystem deltaIoT; Qualities qualities; Environment environment; } Configurat...

    2011

  24. [57]

    EnergyConsumption

    ActivFORMS: A Model-Based Approach to Engineer Self-Adaptive Systems with Guarantees X:59 (power = 7 ? PCR7 : (power = 8 ? PCR8 : (power = 9 ? PCR9 : (power = 10 ? PCR10 : (power = 11 ? PCR11 : (power = 12 ? PCR12 : (power = 13 ? PCR13 : (power = 14 ? PCR14 : PCR15))))))))))))...

    2019

  25. [77]

    DOI:http://dx.doi.org/https://doi.org/10.1016/B978-0-12-802855-1.00003-4 G. A. Moreno, J. C´amara, D. Garlan, and B. Schmerl

    doi

  26. [235]

    Autili, P

    DOI:http://dx.doi.org/https://doi.org/10.1016/0304-3975(94)90010-8 M. Autili, P. Inverardi, and M. Tivoli

    doi

  27. [341]

    Cheng and J

    DOI:http://dx.doi.org/10.1109/TDSC.2015.2429128 B. Cheng and J. M. Atlee

    2015

  28. [1963]

    Probability Inequalities for Sums of Bounded Random Variables. J. Amer. Statist. Assoc. 58, 301 (1963), 13–30. http://www.jstor.org/stable/2282952 U. Iftikhar, J. Lundberg, and D. Weyns

    1963

  29. [1990]

    IEEE Transactions on Software Engi- neering 16, 11 (1990), 1293–1306

    The Evolving Philosophers Problem: Dynamic Change Management. IEEE Transactions on Software Engi- neering 16, 11 (1990), 1293–1306. DOI:http://dx.doi.org/10.1109/32.60317 J. Kramer and J. Magee

    1990 doi

  30. [1994]

    Theoretical Computer Science 126, 2 (1994), 183 –

    A theory of timed automata. Theoretical Computer Science 126, 2 (1994), 183 –

    1994

  31. [1997]

    Annals of Software Engineering

    The Meaning of Requirements. Annals of Software Engineering. Springer 10480. 3, 1 (1997), 5–21. DOI:http://dx.doi.org/10.1023/A:1018990005598 J. Kephart and D. Chess

    1997 doi

  32. [1998]

    In 20th International Conference on Software Engineering

    Architecture-based Runtime Software Evolution. In 20th International Conference on Software Engineering. IEEE Computer Society, 177–186. http://dl.acm.org/citation.cfm?id=302163.302181 ACM Transactions on Software Engineering and Methodology, V ol. X, No. X, Article X, Pub. da...

  33. [2003]

    Computer 36, 1 (2003), 41–50

    The Vision of Autonomic Computing. Computer 36, 1 (2003), 41–50. DOI:http://dx.doi.org/10.1109/MC.2003.1160055 J. Kramer and J. Magee

    2003 arXiv

  34. [2004]

    Computer 37, 10 (2004), 46–54

    Rainbow: Architecture-Based Self-Adaptation with Reusable Infrastructure. Computer 37, 10 (2004), 46–54. DOI:http://dx.doi.org/10.1109/MC.2004.175 T. H´erault, R. Lassaigne, and F. Magniette et al

    2004 doi

  35. [2006]

    ACM Transactions on Autonomous and Adaptive Systems 1, 2 (2006), 223–259

    A Survey of Autonomic Communications. ACM Transactions on Autonomous and Adaptive Systems 1, 2 (2006), 223–259. DOI:http://dx.doi.org/10.1145/1186778.1186782 D. Dujovne, T. Watteyne, X. Vilajosana, and P. Thubert

    2006

  36. [2007]

    InFuture of Software Engineering, FOSE ’07

    Research Directions in Requirements Engineering. InFuture of Software Engineering, FOSE ’07. 285–303. DOI:http://dx.doi.org/10.1109/FOSE.2007.17 B. Cheng et al

    2007 doi

  37. [2008]

    In6th International Conference on Computational Methods in Systems Biology

    Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway. In6th International Conference on Computational Methods in Systems Biology. Springer-Verlag, 231–250. DOI:http://dx.doi.org/10.1007/978-3-540-88562-7 18 A. David,...

    doi

  38. [2010]

    In18th IEEE International Requirements Engineering Conference

    Fuzzy Goals for Requirements-Driven Adaptation. In18th IEEE International Requirements Engineering Conference. IEEE Computer Society, 125–134. DOI:http://dx.doi.org/10.1109/RE.2010.25 G. Behrmann, A. David, and K. G. Larsen

    2010 doi

  39. [2011]

    DOI:http://dx.doi.org/10.1109/TSE.2010.92 R

    Dynamic QoS Management and Optimization in Service-Based Systems.IEEE Transactions on Software Engineering 37, 3 (2011), 387–409. DOI:http://dx.doi.org/10.1109/TSE.2010.92 R. Calinescu, D. Weyns, and S. Gerasimou et al

    2011 doi

  40. [2013]

    DOI:http://dx.doi.org/10.1007/s00450-012-0232-2 G

    Requirements-driven Software Evolution.Computer Science 28, 4 (2013), 311–329. DOI:http://dx.doi.org/10.1007/s00450-012-0232-2 G. Su, T. Chen, D.S. Feng, Y .and Rosenblum, and P.S. Thiagarajan

    2013 doi

  41. [2014]

    Springer, 101–136

    Using Models at Runtime to Address Assurance for Self-Adaptive Systems . Springer, 101–136. DOI:http://dx.doi.org/10.1007/978-3-319-08915-7 4 ACM Transactions on Software Engineering and Methodology, V ol. X, No. X, Article X, Pub. date: January

    doi

  42. [2015]

    International Journal on Software Tools for Technology Transfer17, 4 (2015), 397–415

    Uppaal SMC tutorial. International Journal on Software Tools for Technology Transfer17, 4 (2015), 397–415. DOI:http://dx.doi.org/10.1007/s10009-014-0361-y R. de Lemos et al. 2013.Software Engineering for Self-Adaptive Systems: A Second Research Roadmap. Springer, Berlin, Heide...

    2015 doi

  43. [2016]

    ACM Transactions on Autonomous and Adaptive Systems10, 4 (2016), 23:1–23:28

    Analyzing Latency-Aware Self-Adaptation Using Stochastic Games and Sim- ulations. ACM Transactions on Autonomous and Adaptive Systems10, 4 (2016), 23:1–23:28. DOI:http://dx.doi.org/10.1145/2774222 R. C´amara, J.and de Lemos, C. Ghezzi, and A. Lopes

    2016 doi

  44. [2017]

    In Software Engineering for Adaptive and Self-Managing Systems

    Runtime Monitoring and Resolution of Probabilistic Obstacles to System Goals. In Software Engineering for Adaptive and Self-Managing Systems. 1–11. DOI:http://dx.doi.org/10.1109/SEAMS.2017.5 R. Calinescu, L. Grunske, and M. Kwiatkowska et al

    2017 doi

  45. [2018]

    ACM Trans

    A Survey of Statistical Model Checking. ACM Trans. Model. Comput. Simul. 28, 1, Article 6 (Jan. 2018), 39 pages. DOI:http://dx.doi.org/10.1145/3158668 R. Alur and D. L. Dill

    2018 doi

  46. [2019]

    Software Engineering of Self-Adaptive Systems.Chapter in Handbook of Software Engineering, Springer (2019). D. Weyns, N. Bencomo, and R. Calinescu et al

    2019

  47. [9633]

    DOI:http://dx.doi.org/10.1007/978-3-662-49665-7 16 G

    Springer-Verlag, 269–286. DOI:http://dx.doi.org/10.1007/978-3-662-49665-7 16 G. Su, T. Chen, Y . Feng, and D. S. Rosenblum

    doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.