Efficient Runtime Quantitative Verification Using Caching, Lookahead and Nearly-Optimal Reconfiguration

Simos Gerasimou, Radu Calinescu, Alec Banks

Self-adaptive systems used in safety-critical and business-critical applications must continue to comply with strict non-functional requirements while evolving in order to adapt to changing workloads, environments, and goals. Runtime quantitative verification (RQV) has been proposed as an effective means of enhancing self-adaptive systems with this capability. However, RQV frequently fails to provide the fast response times and low computation overheads required by real-world self-adaptive systems. To improve RQV efficiency, we introduce a set of techniques adapted from other areas of software engineering, namely, caching of recent verification results; limited lookahead; and nearly-optimal reconfiguration.

The main contributions of this work are:

  1. The integration of RQV with caching, limited lookahead and nearly-optimal reconfiguration.
  2. The extension of the open-source platform MOOS-IvP for the development of autonomous systems with runtime model checking capabilities.
  3. The first application of the RQV to the unmanned underwater vehicle (UUV) domain.
  4. A realistic case study from the UUV domain, used to carry out a preliminary assessment of the effectiveness of RQV extended with caching, limited lookahead, nearly-optimal reconfiguration, and combinations thereof.
The source code of the RQV-MOOS component is available to download here: RQV-MOOS.zip

Self-Adaptive UUV System

System characteristics
A self-adaptive UUV is used to carry out a surveillance and data gathering mission. The UUV is equipped with n≥1 on-board sensors that can measure the same attribute of the ocean environment (e.g., water current, salinity or thermocline). When used, the sensors take measurements with different, variable rates r1, r2, ...., rn, consume different amounts of energy e1, e2, ..., en for each measurement. These measurements have an accuracy that depends on the UUV speed s, and the (speed-dependent) probabilities p1, p2, ..., pn that the sensors produce measurements that are sufficiently accurate for the purpose of mission can be calculated from the technical specifications of the sensors. Finally, the n sensors can be switched on and off individually (e.g., to save battery power when not required), but these operations consume an amount of energy given by e1on, e2on, ..., enon and e1off, e2off, ..., enoff, respectively.
Adaptation
The UUV is required to self-adapt to changes in the observed sensor measurement rates ri , 1 ≤ i ≤ n, and to sensor failures by dynamically adjusting:
  1. the UUV speed s
  2. the sensor configuration x1, x2, ..., xn (where xi= 1 if the i-th sensor is on and 0 otherwise)
QoS Requirements
The UUV should comply with the following requirements at all times:
  • (R1) The UUV should take at least 20 measurements of sufficient accuracy per 10 surveyed metres.
  • (R2) The energy consumption of the sensors should not exceed 120 Joules for every 10 metres covered.
  • (R3) If requirements R1 and R2 are satisfied by multiple configurations, the UUV should use one of these configurations that minimises the cost function:
                                                                 cost = w1 x E + w2 x s-1
    where E represents the energy consumed by the sensors to survey a 10m mission distance, and wi, represent weights that reflect the relative importance of each component in the equation.

We formalise these requirements in continuous stochastic logic: uuv.csl
  • (R1)  R≥20measurement[C≤10/s]
  • (R2)  R≤120energy[C≤10/s]
  • (R3)  R=?energy[C≤10/s]
Formulating a parameterised CTMC model
We formulate a parameterised CTMC model comprising 7 states for each sensor, as shown below, in PRISM: uuv.sm
The model M of the entire n-sensor system is obtained through the parallel composition of the n sensor models, i.e., M = M1 || M2 || ... || Mn

approach

UUV system simulator

We implemented a fully-fledged simulator for the UUV self-adaptive system using MOOS-IvP, a widely used platform for the implementation of autonomous applications on unmanned marine vehicles. We designed and developed an RQV-MOOS component.
Scenario characteristics
In this particular scenario, a UUV is deployed on a 600s mission. The UUV is equipped with three on-board sensors and the requirements for the mission are identical to those described before.
Fail pattern:
  • n=1: -
  • n=2: 250:350
  • n=2: 50:150, 200:400, 450:550
Demo
  • Green circle indicates an operating sensor
  • White circle indicates an idle sensor
  • Red circle indicates a sensor with abnormal behaviour
  • Orange circle indicates a sensor that is tested whether it has recovered

Evaluation

To evaluate the effectiveness of RQV augmented with this set of techniques we carried out a broad range of experiments using a test suite comprising 24 scenarios. These scenarios considered instances of our self-adaptive UUV system with the different combinations of the following characteristics:
  • numbers of sensors n ∈ {3, 4, 6}
  • mission duration of 250, 500, 1000 and 2000 RQV steps (executed every 5s)
  • level of sensor rate fluctuations during periods of normal behaviour -low (up to 2%) and high (up to 10%)
  • pattern of sensor failures and/or significant drops in measurement rates

CTMC model of a UUV sensor
Effect of efficient RQV techniques on (a) the average time required to decide a new configuration during an RQV step (response times are averaged over 100 RQV steps); and (b) the total number of quantitative verification operations over 2000 RQV steps, for a scenario with high (i.e., up to 10%) sensor-rate fluctuation during normal operation.