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:
- The integration of RQV with caching, limited lookahead and
nearly-optimal reconfiguration.
- The extension of the open-source platform MOOS-IvP for the
development of autonomous systems with runtime model checking
capabilities.
- The first application of the RQV to the unmanned underwater
vehicle (UUV) domain.
- 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:
- the UUV speed s
- 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 = M
1 || M
2 || ... || M
n
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
- indicates an operating sensor
- indicates an idle sensor
- indicates a sensor with abnormal behaviour
- 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
|
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.
|