{"id":"7e58c4b2-8584-4a4b-a76e-243452ef5b72","arxiv_id":"1908.11179","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"ActivFORMS combines design-time verification of feedback-loop models with runtime statistical model checking and on-the-fly goal updates, validated on a 15-mote IoT deployment.","lead":"This paper presents ActivFORMS, a method for building self-adaptive software systems that uses formally verified models of the feedback loop and statistical model checking at runtime to choose adaptations. It was tested on a real IoT building-monitoring network in Leuven, showing lower energy use than a standard over-provisioning approach and faster decisions than exhaustive runtime verification.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The runtime guarantee transfer rests on a tested-only virtual machine and stub models, not on proven equivalence with Uppaal semantics; a conformance gap would undermine the correctness claim.","rationale":"The reader's weakest-assumption analysis identifies the same load-bearing concern: preservation of design-time guarantees depends on faithful stub models and a correct model execution engine, both supported by testing rather than proof. I agree with the CONDITIONAL verdict. The paper is internally consistent: Section 3.1.2 and Section 3.2.3 explicitly scope the guarantees to the verified model space and to the assumption that the engine respects Uppaal semantics, and Section 6.6 lists threats to validity. However, these scoping statements do not reduce the load on the untrusted transfer step. The formal verification of MAPE models is not in question; the gap is between the verified model and the executing artifact. I also considered the offline calibration of SMC run counts as an alternative concern, but it is less central because Uppaal-SMC probability estimation uses sequential confidence intervals, and the paper discloses the limitation. A differential conformance test of the VM against Uppaal would directly settle whether the guarantee-transfer assumption is justified or needs to be upgraded from testing to formal proof.","tokens_in":47164,"tokens_out":3790,"duration_ms":41889,"concrete_test":"Run randomized differential conformance testing between Uppaal and the ActivFORMS virtual machine: generate a large corpus of small timed-automata networks covering urgent/committed locations, broadcast channels, invariants, and the P-style reachability/liveness properties used in Section 5.1.3, compute each property in Uppaal, then execute the same model on the VM with identical inputs and compare property outcomes and action traces. Any mismatch would show that design-time guarantees are not automatically preserved at runtime and would require either a fixed VM or a formal refinement proof.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's headline guarantee is that design-time verification of MAPE models is preserved at runtime by direct execution. Section 3.2.1 states that guarantees are preserved only 'if this engine executes the feedback loop model correctly, i.e., according to the semantics of the modeling language,' and Section 5.2 says the trustworthiness of the virtual machine is obtained 'through extensive testing,' not formal proof. 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 translation is a substantial semantic gap. The paper provides no conformance evidence that the VM's observable behavior matches Uppaal's operational semantics beyond the attached test suite. A second, related gap is stub fidelity: Section 3.1.2 explicitly says ActivFORMS does not prescribe how to ensure stub models comply with the external elements they represent, only offering general guidelines. Consequently, properties such as P10 (`A[] !Effector.ResultsIncorrect`) are verified against an effector stub, not the actual managed system. The paper is honest about these scopes, but the central claim that ActivFORMS 'supports correctness of the behavior of the feedback loop' depends on exactly these untrusted links.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":47359,"tokens_out":4573,"duration_ms":46043,"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":[{"comment":"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.","section":"§3.2.1, §3.2.3, §5.2"},{"comment":"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.","section":"§3.1.2, §5.1.3 (P10)"},{"comment":"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.","section":"§6.3, Fig. 21"},{"comment":"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.","section":"§6.4, Fig. 22"}],"minor_comments":[{"comment":"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.","section":"§6.1"},{"comment":"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.","section":"§6.5"},{"comment":"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.","section":"§5.1.3"},{"comment":"The formula for the number of adaptation options is garbled as '6 m 5'; please provide the exact expression, presumably 6^(m/5).","section":"§6.4"},{"comment":"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.","section":"Fig. 9 caption"}],"recommendation":"major_revision","confidential_remarks":"The paper is heavily based on the authors' prior publications, but those prior works are disclosed and the integration into an end-to-end approach with a real deployment is a clear increment. The main issue is not novelty but the gap between the headline guarantee and the test-based trust assumptions for the virtual machine and stub models; this is fixable by either adding conformance evidence or carefully rescoping the claims. I would be supportive of a revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know this paper is a well-built consolidation of the authors' earlier work on ActivFORMS, and it delivers what it promises: an end-to-end method for engineering self-adaptive systems with verified MAPE-K feedback loops, runtime statistical model checking for option selection, and basic online goal updates. The evaluation is genuinely strong for this subfield: a 15-mote LoRa network deployed at KU Leuven, comparison against an over-provisioning reference and against runtime quantitative verification with PRISM, plus scalability tests up to 25 motes. The results show their SMC-based approach verifying options in seconds where RQV verifies only 8 of 216 options in the allowed 8 minutes, and cutting energy use about 27% versus the reference while staying under the packet-loss goal. That is a real, useful result.\n\nWhat is genuinely new is the integration: direct execution of timed-automata MAPE models verified at design time, using SMC at runtime instead of exhaustive verification, and on-the-fly goal/model updates. The authors are honest that SMC at runtime is an application of an established technique, not a new method. The concrete property set P1-P12 and the template-instantiation rules are a practical contribution, and the website artifact support is more than most papers in this area provide.\n\nThe soft spot is exactly where the stress-test note lands. The headline guarantee that design-time verification is preserved at runtime rests on a \"trusted\" virtual machine and online update manager whose trustworthiness is established through extensive testing, not formal proof. The translation from Uppaal timed automata into an internal task-graph representation with its own scheduling semantics is a nontrivial gap, and the paper provides no conformance evidence beyond a test suite. Similarly, stub models used in verification are not formally tied to the actual probes, effectors, and verifier; Section 3.1.2 says ActivFORMS does not prescribe how to ensure stub compliance. Property P10 is checked against an effector stub, not the deployed system. These limitations are openly disclosed, which I respect, but they mean the word \"guarantee\" must be read as \"guarantee relative to model and engine assumptions.\" That is a real caveat, but it is not a fatal flaw: the paper never hides it, and the validation on the physical network provides some compensating evidence.\n\nThe evaluation is a single case study, and the SMC run counts are calibrated offline, so generalization is limited. Those are addressable concerns, not fundamental problems.\n\nThis paper deserves a serious referee. It is a solid systems-and-methods contribution that advances the state of practice in self-adaptive systems, and the authors are unusually clear about scope. I would recommend accepting it conditional on the authors either tightening the guarantee language to explicitly state the tested-only basis of the VM and stubs, or adding conformance evidence. For someone working on runtime verification or self-adaptation, this is worth citing; for a reading group, it is a useful example of honest engineering evaluation.","headline":"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.","tokens_in":47934,"tokens_out":1795,"would_cite":true,"duration_ms":21219,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["self-adaptive systems","MAPE-K feedback loop","timed automata","statistical model checking","design-time verification","executable runtime models","IoT adaptation","goal evolution at runtime"],"falsifier":"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.","tokens_in":46910,"feed_emoji":"🔄","tokens_out":6796,"duration_ms":58780,"temperature":0.7,"pith_summary":"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.","feed_headline":"Verified feedback-loop models execute directly at runtime","feed_subtitle":"A model-based approach keeps adaptation fast, adds goals on the fly, and beats exhaustive runtime checking.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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)."],"supporting_citations":[{"why":"Provides the timed automata formalism whose semantics underlies all feedback loop and quality models.","marker":"[Alur and Dill 1994]"},{"why":"Supplies the model checker and modeling language used for design-time verification of the feedback loop.","marker":"[Behrmann et al. 2004]"},{"why":"Defines stochastic timed automata semantics and the statistical model checking queries used for runtime analysis.","marker":"[David et al. 2015]"},{"why":"Establishes the MAPE-K feedback loop structure that ActivFORMS organizes its managing system around.","marker":"[Kephart and Chess 2003]"},{"why":"Provides the quiescence-based update protocol that the online update manager uses for safe model replacement.","marker":"[Kramer and Magee 1990]"},{"why":"Defines runtime quantitative verification, the state-of-the-art baseline that ActivFORMS compares against and beats on scalability.","marker":"[Calinescu et al. 2011]"},{"why":"Supplies the MAPE model templates that make feedback loop design and verification reusable across applications.","marker":"[G. de la Iglesia and Weyns 2015]"},{"why":"Contributes the earlier executable feedback loop models and virtual machine that the current trusted execution engine builds on.","marker":"[Iftikhar and Weyns 2014]"},{"why":"Introduces the IoT exemplar used for the deployment and experiments that validate the approach.","marker":"[Iftikhar et al. 2017]"}],"fun_headline_variants":["Verified feedback loops run directly, no runtime exhaustive checks","Model-based adaptation: verify once, execute at runtime","Statistical model checking makes self-adaptation efficient","ActivFORMS: verified feedback loops with on-the-fly goals","Runtime adaptation with formal guarantees, not exhaustive checks"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Verified feedback loops run directly, no runtime exhaustive checks","Model-based adaptation: verify once, execute at runtime","Statistical model checking makes self-adaptation efficient","ActivFORMS: verified feedback loops with on-the-fly goals","Runtime adaptation with formal guarantees, not exhaustive checks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000547,"raw_usage":{"total_tokens":2622,"prompt_tokens":958,"completion_tokens":1664,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":574,"completion_tokens_details":{"reasoning_tokens":1587}},"tokens_in":574,"tokens_out":1664,"duration_ms":12547,"temperature":1.0,"reasoning_tokens":1587,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T10:21:39.402120+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"2004] to create feedback loop models","cited_arxiv_id":null,"evidence_quote":"Supplies the model checker and modeling language used for design-time verification of the feedback loop."}],"review_version":1}