Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures.
Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance.
To address this need, we introduce ENTRUST, a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware.
ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop
(1) high-integrity self-adaptive software and
(2) assurance cases arguing the suitability of the software for its intended application.
To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop
proof-of-concept self-adaptive software for embedded and service-based systems from the environment monitoring and e-finance domains, respectively.
The main contributions of this work are:
The ENTRUST methodology for the joint development of trustworthy self-adaptive software systems and their associated assurance cases;
An instantiation of the ENTRUST methodology comprising a formally verifiable controller architecture for self-adaptive software systems that integrates quantitative verification at runtime into the system controller;
Stages and key artefacts of the ENTRUST methodology.
The ENTRUST self-adaptive system and assurance case workflow comprises the following design-time and runtime stages:
Design-time ENTRUST stages
Stage 1: Development of Verifiable Models
This stage enables the development of models for:
The controller of the self-adaptive system that implements the estblished MAPE workflow.
The relevant aspects of the controlled software system and its environment.
These models are:
verifiable, i.e., they can be used in conjunction with methods such as model checking or simulation, to obtain evidence that the system and controller meet their requirements.
application-specific, i.e., their development requires domain knowledge, is based on a controlled system specification, and is informed by the system requirements.
The controller models are based on application-independent controller model template(s) that model the generic aspects of the MAPE workflow and contain placeholders for the application-specific elements of an ENTRUST controller.
The controlled software system and environment models are incomplete due to unknown at design-time parameters, nondeterminism (i.e., alternative options whose likelihoods are unknown), missing parts, or some combination of all of these.
Stage 2: Verification of Controller Models
This stage verifies the controller models over a set of generic controller requirements (e.g., deadlock freeness, reachability, liveness) to produce controller assurance evidence.
The controller assurance evidence may also include evidence that some of the system requirements are satisfied, e.g., that irrespective of the system's uncertainty certain application-specific failsafe operating modes are always reachable.
The methods employed to produce this assurance evidence depend on the types of produced models, and on the generic controller requirements and system requirements. Example methods include formal verification, theorem proving and simulation.
Stage 3: Partial Instantiation of Assurance Argument Pattern
This stage uses the controller assurance evidence from Stage 2 to support the partial instantiation of a generic assurance argument pattern for self-adaptive software.
The partially-instantiated assurance argument contains application-independent evidence that a verified controller platform functions as intended and has placeholders for the assurance evidence that be obtained only at runtime, i.e., when the uncertainties associated with the self-adaptive system are resolved.
Stage 4: Enactment of the Controller
This stage assembles the controller of the self-adaptive system.
The process involves integrating the verified controller platform, which contains application-independent controller functionality, with the application-specific controller elements, and with the sensors and effectors that interface the controller with the controlled software system.
Stage 5: Deployment of the Self-Adaptive System
In the last design-time stage, the integrated controller and controlled components of the self-adaptive system are installed, preconfigured and activated by means of an application-specific process.
Runtime ENTRUST stages
Stage 6: Self-adaptation
In this stage, the deployed self-adaptive system is dynamically adjusting its parameters and architecture based on observed internal and environmental changes.
The controller executes a typical MAPE loop, uses information obtained from monitoring the system and its environment, and produces up-to-date system and environment models.
The analysis of these models assesses the system compliance with its requirements after changes, and the planning and execution of suitable reconfigurations if necessary.
Stage 7: Synthesis of Dynamic Assurance Argument
The final stage uses the adaptation correctness evidence produced by the MAPE loop to fill in the placeholders from the partial assurance argument, and to devise the complete assurance case for the reconfigured self-adaptive system.
Tool-Supported ENTRUST Instance
Architecture of an ENTRUST self-adaptive system.
We present a tool-supported ENTRUST instance that supports the engineering of self-adaptive systems with the architecture shown above.
The reusable verified controller platform at the core of this architecture comprises:
A Trusted Virtual Machine that directly interprets and executes models of the steps from the MAPE control loop
A Probabilistic Verification Engine that is used to verify stochastic models of the controlled system and its environment during the analysis step of the MAPE loop.
()
Assurance evidence for the Trusted Virtual Machine and Probabilistic Verification Engine have been obtained through testing.
We make available the test suite used to obtain the evidence for the virtual machine and a description of this test suite.
The test suite for the probabilistic verification engine is available on the engine's webpage.
Stage 1: Development of Verifiable Models
Timed automata executable models of the MAPE loop and stochastic models of the controlled system and its environment are developed.
Controller models
A network of timed automata modelling the four steps of the MAPE control loop is devised starting from a set of template automata
models, shown below.
System specific ENTRUST controllers can be developed by specialising these templates as follows:
(1) replacing the signal placeholders (e.g, <sensorSignal1>) with real
signal names
(2) defining the guard and action functions
(3) devising the yellow shaded Planner and Executor automaton regions
For the Monitor automaton, <sensorSignal1> ... <sensorSignaln> should be replaced with
sensor signals announcing relevant changes in the controlled system. Also, the functions process(), analysisRequired(), and monitorCleanup() should be implemented so that to process the
sensor data, to decide if the change specified by this data entails the invocation of the analyzer through the startAnalysis! signal, and to carry out any necessary cleanup, respectively.
For the Analyzer automaton, signals verify! and verifDone! are used to
invoke the runtime probabilistic verification engine (detailed in enactment of ENTRUST controller). The
functions analyse()
, adaptationRequired(), and analyserCleanup() should be implemented so
that to analyse the verification results and determine a configuration that satisfies QoS requirements, to decide if the new
configuration requires the system to adapt via sending the startPlanning! signal to the planner automaton,
and to carry out any cleanup that may be required, respectively.
For the Planner automaton, the yellow shaded automaton region should be developed to construct a stepwise reconfiguration
plan given the new system configuration. Also, the function plannerCleanup() should be implemented to
perform any required cleanup, and the startExecuting! signal invokes the executor automaton.
For the Executor automaton, the yellow shaded automaton region should be developed to realise the reconfiguration plan and
<executorSignal1> ... <executorSignaln> should be replaced with appropriate effector signals
implementing the adaptation decisions in the controlled system. Also, the functions executorInit() and executorCleanup() should make any required initialisations before the executor starts, and
perform any necessary cleanup, respectively.
Event triggered MAPE model templates
We make available the UPPAAL event triggered and
time triggered ENTRUST controller templates.
Parametric stochastic models
ENTRUST uses parametric stochastic Markovian models of the controlled software system and its environment during the analysis and planning steps of the MAPE
control loop.
These models are system specific and need to be developed from scratch to support the runtime quantitative verification
(RQV) of the software attributes associated with the QoS requirements of the self-adaptive system.
Stage 2: Verification of Controller Models
The MAPE models comprising an ENTRUST controller are verified using a trusted model checker (e.g., UPPAAL).
This operation provides evidence that the ENTRUST controller satisfies key safety and liveness properties that may include both generic and application-specific properties. A non-exhaustive list of such properties is provided in the table below.
Generic properties that should be satisfied by an ENTRUST controller
P1
The ENTRUST controller is deadlock free.
A▢ not deadlock
P2
Whenever analysis is required, the Analyser eventually carries out this action.
A▢(Monitor.StartAnalysis → A◇ Analyzer.Analyse)
P3
Whenever the system requirements are violated, a stepwise reconfiguration plan is eventually assembled.
A▢(Analyzer.Adapt → A◇ Planner.PlanCreated)
P4
Whenever a stepwise plan is assembled, the Executor eventually implements it.
A▢(Planner.PlanCreated → A◇ Executor.PlanExecuted)
P5
Whenever the Monitor starts processing the received data, it eventually terminates its execution.
A▢(Monitor.ProcessSensorData → A◇ Monitor.Finished)
P6
Whenever the Analyser begins the analysis, it eventually terminates its execution.
A▢(Analyzer.Analyse → A◇ Analyzer.AnalaysisFinished)
P7
A plan is eventually created, each time the Planner starts planning.
A▢(Planner.Plan → A◇ Planner.PlanCreated)
P8
Whenever the Executor starts executing a plan, the plan is eventually executed.
A▢(Executor.Execute → A◇ Executor.PlanExecuted)
P9
Whenever adaptation is required, the current configuration and the best configuration differ.
A▢(Analyzer.Adapt → currentConfig != newConfig)
Stage 3: Partial Instantiation of Assurance Argument Pattern
The ENTRUST assurance argument pattern builds on our previous work on software safety assurance, in which we created a
catalog of reusable assurance case
patterns.
The ENTRUST pattern is depicted below in Goal Structuring Notation (GSN), a community standard widely used in industry for developing assurance cases.
The main elements of GSN can be found here.
ENTRUST assurance argument pattern.
The elements surrounded by curly brackets '{' and '}' need to be instantiated for each self-adaptive system.
The away goal ReqsPreservedByPlatform confirms that the controlled system handles correctly the reconfiguration commands received through effectors. This away goal is assured using standard assurance processes.
The away goal NoErroneousBehaviour (shown below) justifies the absence of erroneous behaviours (e.g., deadlock) due to the adoption of a new configuration.
This away goal is based on the Hazardous Contribution Software Safety Argument pattern defined in the GSN catalog.
Away goal NoErroneousBehaviour.
Stage 4: Enactment of the Controller
The artifacts generated and verified in previous ENTRUST stages, i.e., the controller and stochastic models, are combined with the ENTRUST verified controller platform and application-specific sensor, effector and stochastic model management components.
Although the sensor, verification engine and effector components are application specific, they include functionality common
across applications, i.e., generic signals (e.g.,verify! and planExecuted?) through which these components synchronise with the MAPE automata. To facilitate the enactment process, we provide abstract Java classes that support this common functionality.
Stage 5: Deployment of the Self-Adaptive System
The ENTRUST controller and the controlled software system are integrated into a self-adaptive software system that is then installed, preconfigured and set running. This pre-configuration must select initial values for all the parameters of the controlled system.
Stage 6: Self-Adaptation
The deployed self-adaptive system is dynamically adjusting its configuration in line with the observed internal and environmental changes.
The system and environment information received by the Monitor through Sensors is used to resolve the unknowns from the stochastic models of the controlled system and its environment (e.g., probabilities of transition to 'failure' states, rates of transition to `success' states etc.).
Then, the Analyzer employs the Probabilistic Verification Engine to reverify the compliance of the self-adaptive system with its runtime-assured requirements.
If the requirements are no longer met, the Analyzer uses the verification results to identify a new system configuration that restores this compliance, or to find out that such a configuration does not exist and to select a predefined failsafe configuration.
The step-by-step actions needed to achieve the new configuration are then established by the Planner and implemented by the Executor through the Effectors of the controlled system.
Stage 7: Synthesis of Dynamic Assurance Argument
The ENTRUST assurance case evolves in response to the results of the MAPE process.
The use of continual verification within the ENTRUST control loop produces assurance evidence that underpins the dynamic generation of assurance cases.
The assurance case resulting from this stage captures the full argument and evidence for the justification of the current configuration of the self-adaptive system.
Versions of the adaptation assurance evidence and of the dynamic assurance argument are stored in the Knowledge Repository.
Software Systems Used to Evaluate ENTRUST
Unmanned Underwater Vehicle Embedded System
A UUV equipped with n ≥ 1 on-board sensors (that can measure the same characteristic of the ocean environment, e.g., water current or salinity) is
deployed to carry out a data gathering mission. When used, the sensors take measurements with different, variable rates r1,
r2, . . . , rn. The probability that each sensor produces measurements that are sufficiently accurate for the purpose of
the mission depends on the UUV speed sp, given by p1, p2, . . . , pn. For each measurement taken,
different amount of energy is consumed, given by e1, e2, . . . , en. 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.
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 sp
the sensor configuration x1, x2, . . . , xn (where xi = 1 if the i-th sensor is on and
xi = 0 otherwise)
so that the following QoS requirements are satisfied at all times:
ID
Description
R1
(throughput): The UUV should take at least 20 measurements of sufficient accuracy for every 10 metres of mission distance
R2
(resource usage): The energy consumption of the sensors should not exceed 120 Joules per 10 surveyed metres
R3
(cost): If requirements R1 and R2 are satisfied by multiple configurations, the UUV should use one of these configurations that minimises
energy consumption and maximises UUV speed.
R4
(failsafe): If a configuration that meets requirements R1 - R3 is not identified within 2 seconds after a sensor rate change, the UUV speed must be reduced to 0m/s, so that the UUV does not
advance until its sensors recover or new instructions are provided by a human operator.
Foreign Exchange Trading System
Foreign exchange trading (FX) workflow.
An FX customer (called a trader) can use the system in two operation modes. In the expert mode, FX executes a loop that analyses market
activity, identifies patterns that satisfy the trader's objectives, and automatically carries out trades. Thus, the Market watch service
extracts real-time exchange rates (bid/ask price) of selected currency pairs. This data is used by a Technical analysis service that
evaluates the current trading conditions, predicts future price movement, and decides if the trader's objectives are: (i) "satisfied" (causing the
invocation of an Order service to carry out a trade); (ii) "unsatisfied" (resulting in a new Market watch invocation); or
(iii) "unsatisfied with high variance" (triggering an Alarm service invocation to notify the trader about discrepancies/opportunities not
covered by the trading objectives). In the normal mode, FX assesses the economic outlook of a country using a Fundamental analysis
service that collects, analyses and evaluates information such as news reports, economic data and political events, and provides an assessment on
the country's currency. If satisfied with this assessment, the trader can use the Order service to sell or buy currency, in which case a
Notification service confirms the completion of the trade.
Multiple service-providers could support concrete implementations that provide the functionality required by the n=6 services in the FX
system. Each
service comprises an interface with which it can be invoked at runtime as well as a service-level-agreement (SLA), a
contract that defines various QoS characteristics, e.g., reliability, performance (response time), and price, that both parties (service provider and
FX system, as service consumer) are obliged to comply with.
The FX system should dynamically select third-party implementations for each of the n ≥ 1 services from the workflow above for which
in-house implementations are not available, in order to meet the following QoS requirements:
ID
Description
R1
(reliability): Workflow executions must complete successfully with probability at least 0.9
R2
(response time): The total response time per workflow execution should be at maximum 5s
R3
(cost): If requirements R1 and R2 are satisfied by multiple configurations, the system should use one of these configurations that minimises both price and response time.
R4
(failsafe): If a configuration that meets requirements R1 - R3 cannot be identified within 2 seconds after a change in service characteristics is signalled by the sensors of the self-adaptive FX system, the Order service invocation is bypassed, so that FX cannot make any order using obsolete data (e.g., old exchange rates).
Evaluation
To evaluate the correctness, effectiveness and generality of ENTRUST methodology, we carried out extensive experiments using two software systems from different application domains:
(1) an embedded mission-critical system from the unmanned vehicle domain;
(2) a service-based business-critical system from the exchange trade domain.
We also assess the efficiency and scalability of ENTRUST by measuring the CPU time taken for carrying out specific stages of the ENTRUST methodology.
Case study 1: Applying ENTRUST to the UUV system
Stage 1: Development of Verifiable Models
Controller models
We specialised the ENTRUST model templates and developed the MAPE models below for the UUV system. NB: The yellow shaded areas in Planner and Executor show the UUV-specific steps for assembling a plan and executing the
adaptation, respectively.
UUV MAPE automata that instantiate the event triggered ENTRUST model templates.
Parametric stochastic models
We model the behaviour of the i-th UUV sensor as a continuous-time Markov chain (shown below). From the initial state
s0, the system transitions to state s1 or s6 if the sensor is switched on (xi = 1) or off
(xi = 0), respectively. The sensor takes measurements with rate ri, as indicated by s1 → s2. A measurement is accurate with probability pi enabling the transition s2 → s3; when inaccurate, the transition s2 → s4 is taken. While the sensor is active this operation is repeated, as modelled by the transition s5 → s1.
A "measure” structure, shown in green dashed rectangular box, associates a reward of 1 when taking an
accurate measurement. An "energy"
structure, shown in red solid rectangular boxes, associates the energy used to switch the sensor on
(eon ) and off
(eoff ) and to perform a measurement (ei) with the respective event transitions.
The system model M is given by the parallel composition of the n sensor models, i.e., M = M1||...||Mn.
CTMC model Mi of the i-th UUV sensor.
The system QoS requirements R1 – R3 are formalised as the Continuous Stochastic Logic (CSL) formulae:
ID
CSL formula
R1
R≥20{"measure"} [C≤10/s]
R2
R≤120{"energy"} [C≤10/s]
R3
minimise (w1E + w2s-1), where E = R=?energy [C≤10/s]
* 10/s represents the time taken by the UUV to cover 10m at speed s, and w1, w2 are weigths
Requirement R4 encodes a condition-action policy, and thus it is formalised in Computation Tree Logic (CTL):
We used UPPAAL to verify that the network of MAPE automata satisfies the all
the generic properties of the ENTRUST controller from the table in ENTRUST stage 2, and the application-specific property formalising requirement R4 (failsafe).
We make available the UPPAAL models of the ENTRUST controller developed for the UUV system.
Stage 3: Partial Instantiation of Assurance Argument Pattern
The figure below depicts the partially-instantiated assurance argument pattern for the self-adaptive UUV system, in which we shaded the (partially) instantiated GSN elements.
The goal R1Achieved is supported by: (1) sub-claim R1Verified, whose associated solution placeholder R1Result remains uninstantiated and should constantly be updated by the ENTRUST controller at runtime; and (2) the away goal ReqsPreservedByPlatform.
Similar reasoning applies for the goals R2Achieved and R3Achieved.
The (failsafe) goal R4Achieved is fully instantiated because the solution R4Result was obtained in ENTRUST Stage 2
(i.e., UPPAAL verification evidence that R4 is achieved irrespective of the configuration of the self-adaptive system).
Partially-instantiated assurance argument for the UUV system.Stage 4: Enactment of the Controller
We assembled a fully-fledged ENTRUST controller for the UUV system by integrating the controller and stochastic models with our verified controller platform and by implementing Java classes that specialise the abstract Sensors, Effectors, and VerificationEngine classes.
The Sensors class synchronises with the Monitor automaton through the newRate! signal, while the Sensors and Effectors classes invoke the relevant API methods of our UUV simulator.
The specialised verification engine instantiates the parametric models Mi, 1 ≤ i ≤ n, and verifies the CSL formulae for requirements R1 - R3.
Stage 5: Deployment of the Self-Adaptive System
We used the open-source MOOS-IvP for the implementation of autonomous applications on unmanned marine vehicles and we developed a fully-fledged three-sensor UUV simulator.
We then exploited the publish-subscribe architecture of MOOS-IvP to interface the ENTRUST sensors and effectors with the UUV simulator, we installed the controller and the controlled system on a normal computer, and we preconfigured the system to start with zero speed and all its sensors switched off.
Stage 6: Self-Adaptation
We illustrate the adaptation decisions made by the ENTRUST controller at runtime using a particular scenario (from a set of seeded
changes) including a sudden degradation of a sensor service of the UUV system.
The UUV system comprises n = 3 sensors with: measurement rates r1=5, r2=4, r3=4; energy consumed per
measurement e1=3, e2=2.4, e3=2.1; and energy used for switching a sensor on and off e1on=10, e2on=8, e3on=5 and e1off=2, e2off=1.5, e3off=1, respectively. Suppose that the current UUV configuration is (x1,
x2, x3, s)= (0,1,1,2.8) and sensor 3 experiences a service degradation such that r3new=1.
The ENTRUST controller receive this new measurement rate through the monitor. Since the sensor rates differ from those in the knowledge
repository, the guard analysisRequired() returns true and the startAnalysis!
signal is sent. The analyser model upon receiving the signal, it invokes the runtime probabilistic verification engine, whose results
for requirements R1–R3 are depicted below. The analyse() action filters the results as follows:
configurations that violate requirements R1 or R2, i.e., the shaded areas from the figure, are discarded. The remaining configurations
are feasible, so their cost is computed for w1=1 and w2=200. The configuration minimising the cost (i.e.,
(x1,x2,x3,s)= (1,1,0,3.2) – circled in the figure) is selected as the best configuration. Since the
best and the current configurations
differ, the adaptationRequired() holds and the analyzer invokes the planner through the
startPlanning! signal to assemble a stepwise reconfiguration plan with which i) sensor 2 is switched on; ii) next, sensor 3 is
switched off; and iii) finally the speed is adjusted to 3.2m/s. When the plan is assembled, the executor receives the startExecuting? signal and is enforcing this plan to the UUV system through sending the relevant signals (sensorON!, sensorOFF!, changeSpeed!) to effectors.
Verification results for requirement (a) R1, (b) R2, and (c) cost of the feasible configurations.
The best configuration (circled) corresponds to (x1,x2,x3,s)= (1,1,0,3.2), and the shaded regions correspond to requirement violations.
Stage 7: Synthesis of Dynamic Assurance Argument
Following the adaptation decision made in the previous ENTRUST stage, the ENTRUST controller must now guarantee satisfaction of QoS
requirements using the new UUV configuration (x1,x2,x3,s)= (1,1,0,3.2).
The fully instantiated assurance argument is shown below.
Fully-instantiated assurance argument for the UUV system. Shading is used to show the elements instantiated at runtime.
Case study 2: Applying ENTRUST to the FX system
Stage 1: Development of Verifiable Models
Controller models
We specialised the ENTRUST model templates and developed the MAPE models below for the FX system. NB: The yellow shaded areas in Planner and Executor show the UUV-specific steps for assembling a plan and executing the
adaptation, respectively.
FX MAPE automata that instantiate the event triggered ENTRUST model templates.
Parametric stochastic models
We model the behaviour of the FX system as a discrete-time Markov chain (shown below). From the initial state
s0, the system transitions to state s1 with probability 0.66 or s9 with probability 0.34,
activating the expert or normal mode, respectively. In the expert mode, FX uses the Market watch and Technical
analysis services to analyse market activity. Depending on this analysis, an Alarm is triggered, an Order is made or a Market watch
invocation is repeated, with probability 0.11, 0.28, and 0.61, respectively. In the normal mode, FX uses the Fundamental analysis
service to collect information about currency pairs of interest. With probability 0.27 an Order is made, whereas with
probability 0.73 FX returns to the initial state s0.
pMW, pTA, ..., timeMW, timeTA, ..., and priceMW, priceTA, ..., represent the reliability (i.e. success probability), the response time and the price, respectively, of the services selected to implement the MW, TA, ... system operations.
We define the following cost/reward structures:
A "price" structure, shown in solid red rectangular boxes , associates priceMW, priceTA,.... with the services selected to implement the MW, TA, ... system operations.
A "response time" structure, shown in blue dashed rectangular boxes, associates timeMW, timeTA, ... with the services selected to implement the MW, TA, ... system operations.
Parametric DTMC model of the FX system.
The system QoS requirements R1 – R3 are formalised as the Probabilistic Computation Tree Logic (PCTL) formulae:
ID
PCTL formula
R1
P≥0.9 [ F "done" ]
R2
R≤5{"time"}[F "done"]
R3
minimise (w1P + w2T), where P = R=?{"price"}[F "done"] and T = R=?
{"time"}[F "done"]
Requirement R4 encodes a condition-action policy, and thus it is formalised in Computation Tree Logic (CTL):
We used UPPAAL to verify that the network of MAPE automata satisfies the all
the generic properties of the ENTRUST controller from the table in ENTRUST stage 2, and the application-specific property formalising requirement R4 (failsafe).
We make available the UPPAAL models of the ENTRUST controller developed for the FX system.
Stage 3: Partial Instantiation of Assurance Argument Pattern
The figure below depicts the partially-instantiated assurance argument pattern for the self-adaptive FX system.
Shaded GSN elements are those partially instantiated.
The goal R1Achieved is supported by: (1) sub-claim R1Verified, whose associated solution placeholder R1Result remains uninstantiated and should constantly be updated by the ENTRUST controller at runtime; and (2) the away goal ReqsPreservedByPlatform.
Similar reasoning applies for the goals R2Achieved and R3Achieved.
The (failsafe) goal R4Achieved is fully instantiated because the solution R4Result was obtained in ENTRUST Stage 2
(i.e., UPPAAL verification evidence that R4 is achieved irrespective of the configuration of the self-adaptive system).
Partially-instantiated assurance argument for the FX system.Stage 4: Enactment of the Controller
We assembled a fully-fledged ENTRUST controller for the FX system by integrating the controller and stochastic models with our verified controller platform and by implementing Java classes that specialise the abstract Sensors, Effectors, and VerificationEngine classes.
The Sensors class synchronises with the Monitor automaton through the newServicesCharacteristics! signal, while the Sensors and Effectors classes invoke the relevant API methods of our FX simulator.
The specialised verification engine instantiates the parametric DTMC model, and verifies the CSL formulae for requirements R1 - R3.
Stage 5: Deployment of the Self-Adaptive System
We implemented a prototype version of the FX system using Java web services deployed in Tomcat/Axis, and a Java FX workflow that we integrated with the ENTRUST controller.
For simplicity and without loss of generality, we installed the components of the self-adaptive FX system on a normal computer, and we preconfigured the system to start by using the first web service implementation available for each service (i.e. MW0, TA0 etc.), except for the Order service for which NoSvc was selected initially (to ensure that the failsafe requirement R4 was satisfied until a configuration meeting requirements R1--R3 was selected by the controller).
Stage 6: Self-Adaptation
We illustrate the adaptation decisions made by the ENTRUST controller using a scenario in which one of the selected service implementations experiences a significant reliability degradation.
The FX system comprises n = 6 services and for each service there are 2 concrete service implementations (i.e., 64 possible configurations), whose characteristics are as follows:
Service ID
Reliability
Time (s)
Price (p)
MW0
0.976
5
0.5
MW1
0.995
10
0.5
TA0
0.998
6
0.6
TA1
0.985
4
1.0
FA0
0.998
23
1.6
FA1
0.990
25
0.7
Service ID
Reliability
Time (s)
Price (p)
Al0
0.915
15
0.6
Al1
0.990
9
0.9
Or0
0.995
25
0.6
Or1
0.95
20
1.3
No0
0.990
5
1.8
No1
0.990
8
0.5
where MW*: Market Watch, TA*: Technical Analysis, FA*: Fundamental Analysis, Al*: Alarm, Or*: Order, No*: Notification
The current configuration of active service implementations is (MW, TA, Al, Or, No, FA)=(MW1, TA0, FA0, Al0, Or0, No1) which was obtained due to decrease in reliability of Market Watch service MW0 (pnewMW0=0.9) and increase in response time of Fundamental Analysis service FA1 (timenewFA1=1.2s).
Suppose that MW0 recovers (pnewMW0=0.976).
The ENTRUST controller receives the updated services characteristics (e.g., reliability) through the monitor.
Since the services characteristics are different from those in the knowledge repository, the guard analysisRequired() holds and the startAnalysis! signal is sent.
The analyser model upon receiving the signal, it invokes the probabilistic verification engine, whose results
for requirements R1–R3 are depicted below.
The analyse() action filters the results as follows:
configurations that violate requirements R1 or R2, i.e., the shaded areas from the figure, are discarded.
The remaining configurations are feasible, so their cost is computed for w1=1 and w2=2.
The configuration (MW, TA, Al, Or, No, FA)=(MW0, TA0, FA0, Al1, Or0, No1) has the minimum cost and thus it is selected as the best system configuration.
Since the best and the current configurations differ, the adaptationRequired() holds and the analyzer invokes the planner through the startPlanning! signal to assemble a stepwise reconfiguration plan with which:
(1) MW0 replaces MW1; and
(2) Al1 replaces Al0.
Once the plan is ready, the executor receives the startExecuting? signal and is realising this plan to the FX system through sending the signal changeService! to effectors.
Verification results for requirement (a) R1, (b) R2, and (c) cost of the feasible configurations.
The configuration index i1i2i3i4i5i6 in number base 2 corresponds to the FX configuration that uses services (MWi1, TAi2, FAi3, Ali4, Ori5, Noi6).
The best configuration (circled) has index 510=0001012, corresponding to (MW0, TA0, FA0, Al1, Or0, No1).
Shaded regions correspond to requirement violations.
Stage 7: Synthesis of Dynamic Assurance Argument
Following the adaptation decision made in the previous ENTRUST stage, the ENTRUST controller must now guarantee satisfaction of QoS
requirements using the new FX configuration (MW, TA, Al, Or, No, FA)=(MW0, TA0, FA0, Al1, Or0, No1).
We show below the fully instantiated assurance argument.
Fully-instantiated assurance argument for the FX system. Shading is used to show the elements instantiated at runtime.
Correctness
To examine whether ENTRUST self-adaptive systems make the right adaptation decisions and generate valid assurance cases, we carried out experiments that involved running the UUV and FX systems in realistic environments comprising (simulated) unexpected changes specific to their domains.
For the UUV system, the experiments were seeded with failures including sudden degradation in the measurement rates of sensors and complete failures of sensors, and with recoveries from these problems. For the FX system, we considered variations in the response time and the probability of successful completion of third-party service invocation.
Change Scenarios for the Self-Adaptive UUV System
Change scenarios for the self-adaptive UUV system over 2100 seconds of simulated time.
Extended shaded regions indicate the sensors switched on at each point in time, and narrow shaded areas show the periodical testing of sensors switched off due to degradation (to detect their recovery).
The labels A-H correspond to the following events:
The UUV starts with the initial state and configuration
Sensor 3 experiences degradation(rnew3=1), so the higher-rate but less energy efficient sensor 1 is switched on (allowing a slight increase in speed to sp=3.2m/s) and sensor 3 is switched off;
Sensor 3 recovers and the initial configuration is resumed;
Sensor 2 experiences a degradation, and is replaced by sensor 1, with the speed increased to sp=3.1m/s;
Sensor 2 recovers and the initial configuration is resumed;
Both sensor 2 and sensor 3 experience degradations, so sensor 1 alone is used, with the UUV travelling at a lower speed sp=2.1 m/s;
Periodic tests (which involve switching sensors 2 and 3 on for short periods of time) are carried out to detect a potential recovery of the degraded sensors;
Sensors 2 and 3 resume operation at nominal rates and the initial UUV configuration is reinstated.
Change Scenarios for the Self-Adaptive FX System
Change scenarios for the self-adaptive FX system. The thick continuous lines depict the services selected at each point in time.
The labels A-G correspond to the following events:
The FX starts with the initial services characteristics and uses a configuration comprising the services =(MW0, TA0, FA0, Al1, Or0, No1), which satisfies requirements R1 and R2 and optimises R3;
The Market Watch service MW0 experiences a significant reliability degradation (pnewMW0=0.9), so FX starts using MW1 and switches to the faster but slightly less reliable Fundamental Analysis service FA1;
Due to an increase in response time of Fundamental Analysis service FA1 (timenewFA1=1.2), the FX switches to using FA0 and also replaces the Alarm service Al1 with the faster but more expensive service Al0;
The Market Watch service MW0 recovers, so FX switches back to this services and also resumes using the less reliable Alarm service Al1;
The Technical Analysis service TA0 and the Notification service No1 exhibit unexpected degradations in reliability (pnewTA0=0.98) and in response time (timenewNo1=1s), respectively, so the FX system self reconfigures to use (MW0, TA1, FA1, Al0, Or0, No0);
As a result of a reliability degradation in the OrderOrder Or0 (pnewOr0=0.91) and recovery of the Technical Analysis service TA0, the FX system replaces services MW0, TA1, FA1 and Or0 with MW1, TA0, FA0 and Or1, respectively;
All the degraded services recover, so the initial configuration (MW0, TA0, FA0, Al1, Or0, No1) is reinstated.
Efficiency and Scalability
To assess the efficiency and scalability of ENTRUST, we measured the CPU time taken by:
We repeated each scenario 10 times, and report the following boxplots for (1) and (2).
CPU time for the UPPAAL verification of the generic controller properties
* the UUV system is equipped with 3 sensors, and the FX system comprises two third-party implementations per service
CPU time for the runtime probabilistic model checking of the QoS requirements after changes
Sensitivity Analysis
Finally, we assessed how changes in the weights w1,w2 from the UUV cost (R3) and the energy usage of the n UUV sensors (R2) affect the adaptation decisions made by ENSTRUST. To this end, we used UUVs with n ∈ {3,4,5,6} sensors and for each UUV variant (i.e., n value) we ran 30 independent experiments with the weights w1,w2 randomly drawn from the interval [1, 500], and the energy consumption for taking a measurement and switching on and off a sensor (i.e., ei, eion and eioff, 1 ≤ i ≤ n, respectively) randomly drawn from the interval [0.1J,10J].
The experimental results provide evidence that ENTRUST successfully reconfigured the system irrespective of the weight and energy usage values. If a configuration satisfying requirements R1-R3 existed for a specific change and system characteristics combination, ENTRUST reconfigured the UUV system to use this configuration. When no configuration satisfying requirements R1-R3 was available, ENTRUST employed the zero-speed failsafe configuration from requirement R4 until configurations satisfying requirements R1-R3 were again possible after a sensor recovery.
We make available the CPU time taken for runtime probabilistic model checking and the PRISM-generated assurance evidence.
