The evolution of Large-Scale Distributed Systems is strongly associated with the development of solutions for smart cities. They consist of a large-number of sensors, processing centers and services deployed in a wide geographical area. Due to their complexity and heterogeneity, such systems face a high-level of uncertainty and the failure of one node can a ect the availability of the whole solution. Monitoring services collect data about the state of components and elaborate a diagnosis, aiming to increase the reliability of the system. This paper proposes an Abstract State Machine model to capture the properties and behavior of monitoring services addressing system failures. The method encompasses the translation of the requirements of the system to ground models. We discuss the formal solution with respect to the problem domain and execute a simulation of the model. We discuss the suitability of the method for distributed systems and compare it with other modeling approaches.
Large-Scale Distributed Systems (LDS) aggregate computing resources through a wide area network. Such systems o er scalability and transparency of resources and compose services for building various applications. Their complexity introduces many challenges like heterogeneity, node or communication failures. Recovery and high availability of the system require reliable monitoring.
One of the trends for developing a sustainable future is supported by smart cities. They encompass applications for enhancing transportation, energy usage, waste disposal. Sensors, data centers and computing resources collaborate to process data and provide services to end devices. These services face failures and availability issues of LDS. Monitors play a key role in detecting issues and providing data for adaptation plans to bring the system to a normal execution mode. Monitoring processes are complemented with adaptation processes, which respond to the existing problems with various restoration plans. The main contribution of the paper consists in analyzing and validating correct behavior of monitors, whose accuracy enhances the robustness of the system.
The goal of this paper is to integrate the formal modeling capabilities of the
Abstract State Machines (ASMs) for de ning a monitoring solution for LDS. We
motivate the choice of ASMs by comparing them with other formal methods with
respect to their suitability for distributed systems. We present the requirements
of the system from the perspective of a smart city application and propose
a structure for the monitoring framework. Requirements are translated to a
control state ASM. The use of formal methods for de ning a solution helps in
understanding possible aws of the model before deployment [
The remainder of the paper is structured as follows. Section 2 captures the problem domain and the research objectives of the paper. Essential concepts related to the ASM formal method are presented in Section 3. Section 4 describes the structure of the monitoring framework and is continued by its formal specication and validation in Section 5. Related work is discussed in Section 6, after which conclusions are drawn in Section 7. 2
The evolution of distributed systems, Internet of Things (IoT) and network capabilities played an important role in the adoption of ubiquitous solutions for smart cities. Widely distributed sensors for tra c, pollution and environment continuously collect data that are integrated in various applications. The aim is to sustainably develop cities and improve the quality of life of the the inhabitants.
One of the main areas of interest is provisioning of medical services. Asthma
is a chronic in ammatory disease manifested by air ow obstruction, coughing
and/or chest tightness. The condition is directly a ected by the environment
and by the behavioral patterns of the patient. The bene ts of a smart city
application empowers patients to take informed decisions and prevent severe
asthma attacks. In a smart city network, air quality sensors provide data related
to the percentage of dust particles and pollutants, while meteorological data
supply humidity and temperature values. Information about tra c is important
for avoiding crowded areas and also indicate the pollution level. Such sensors
are distributed in an LDS and data they provide can be integrated with activity
patterns extracted from smart gadgets for building a knowledge base. Hosseini
et al. [
System nodes refer to sensors and services, which are o ered by various cloud providers (Amazon, Microsoft Azure, etc.). Node problems are propagated to the whole system, making it hard to identify the source. We emphasize the role of the monitors for ensuring availability of the system and propose a formal model for it. The proposal closely follows the subsequent research questions and objectives.
Research Question 1. Can formal methods capture properties of LDS monitors? How does applying formal methods to distributed systems di er from modeling traditional applications? We analyze existing formal methods and establish the best option given the characteristics of distributed systems. The choice of the ASM technique is justi ed in Section 3 together with the de nition of speci c control structures and properties that can be speci ed using this approach.
Research Question 2. How can unavailability issues of smart city applications be tackled by the monitoring solution? In Section 4 we present the main requirements of the system and how the proposed monitoring model addresses them. We emphasize the unavailability issues and discuss the novelty of our approach.
Research Question 3. How does the ASM model re ect the properties of
the monitoring framework?
We de ne the structure of the monitoring solution, capture the work ow in terms
of control state diagram and discuss the important transitions of the system. We
also declare states and rules with the aid of AsmetaL language, which re ect the
behavior of the monitors. Section 5 discusses in more details these aspects.
3
While traditional software development processes integrated formal methods
easier, the evolution of agile methods, distributed systems and novel business models
introduced more challenges. Kossak and Mashkoor [
Given the characteristics of the system described in Section 2, we are
interested in adopting the technique that supports modeling properties of distributed
systems like concurrency and non-determinism. The expressiveness of the model
is important due the heterogeneous nature of the target system. According to
[
Petri Nets have been widely used for modeling distributed systems. In [
ASMs rely on the concept of evolving algebras proposed by Yuri Gurevich in
[
The speci cation of an ASM consists of a nite set of transition rules of the
type: if Condition then Updates [
Rules consist of di erent control structures that re ect parallelism (par), sequentiality (seq), causality (if...then) and inclusion to di erent domains (in). With the forall expression, a machine can enforce concurrent execution of a rule R for every element x satisfying a condition ': forall x with ' do R. Non-determinism is expressed through the choose rule: choose x with ' do R. De nition 1. A control state ASM is an ASM following the structure of the rules illustrated in Fig. 1: any control state i veri es at most one true guard, condk, triggering, thus, rulek and moving from state i to state sk. In case no guard is ful lled, the machine does not perform any action.
i cond1 ..... condn rule1 rulen j1 jn if ctl state = i then if cond1 then rule1 ctl state := j1 end if ........ if condn then rulen ctl state := jn end if end if Functions in ASMs are classi ed according to permissions on di erent operations. Static functions refer speci cally to constants, while dynamic functions can be updated during execution. Controlled functions are written only by the machine, while monitored ones are written by the environment and read by the machine. Both the machine and its environment can update shared functions. 4
This paper describes the monitoring component for an LDS, which is responsible to identify failures and unavailability of constituent nodes. The description of the system starts from the presentation of requirements and is completed by an architectural model, which emphasizes robustness achieved through redundancy. 4.1
Req. 1. Monitoring processes will observe each node of the LDS. In order to avoid single points of failure, a set of monitors is assigned to every node. Req. 2. Before starting data collection, the monitor submits a request to verify node availability. If no answer is received, the node is considered unavailable. Req. 3. Data collected by the monitor is used for detecting unavailability problems and failures.
Req. 4. A monitor that detects a problem must disseminate it locally to other monitors assigned to the same node and carry out a collaborative evaluation. Req. 5. Monitoring speci c data and events are temporarily logged in a local storage from where they can be retrieved for analysis processes. Req. 6. Monitoring processes run continuously in background of the execution. Req. 7. Each monitor is characterized by a trustworthiness level, based on its performance. Bad assessment of data indicates a lower trustworthiness. Req. 8. Monitoring data are also used for system adaptation and evaluation of recon guration solutions. 4.2
d stPho—ne ——Sen—reque —Reply P—rovider2 ...
S21 rve ——O e ——Obs bserve mj+1 ...mk ... S2n rve ——O e ——Obs bserve mk+1 ...ml Computer ...
Providers
Ss1 ... Ssn ml+——Ob1serve..——.Obmserve p mp—+—Obs1erve..——.Obmserve r
We assume that sensors are deployed among various providers. Sensor Spi of a provider P is assigned a set of monitors Monitors (Spi) = fmi1, ..., mikg. The monitors observe the node by carrying out speci c processes: checking availability, collecting raw data, building higher-level metrics, interpreting data and logging. In order to reduce the communication overhead, monitors interact only when a problem is detected and a collaborative decision is required.
Monitoring components indicate abnormal situations together with corresponding data to the adaptation layer, where a case based repository is consulted and an action plan is proposed. After the deployment of the plan the adapters request data from the monitors in order to check the e ciency of their actions. 5 5.1
The model contains ASM monitor agents, each carrying out its own execution according to the the requirements mentioned in Section 4.1. Fig. 3 displays the control state ASM ground model of the monitor agent. The monitor is initialized in the Inactive state. If the monitor is deployed by the middleware, then it can be assigned to a node. From there, the agent moves to the Active state from where monitoring speci c processes start.
The monitor sends a request to the node after which it moves to the Wait for response state. The guard Reply arrived is veri ed and if an answer to the request is acknowledged, the monitor processes it by calculating the latency and moves further to the Collect data state. If no reply is recorded, the monitor veri es if the request has exceeded the maximum allowed delay (Timeout guard). In this case it stops the current request and moves to the Report problem state. If the Timeout guard is false, the agent remains in theWait for response state.
Inactive
Monitor deployed
Yes
Assign to node Gather metrics
Retrieve information
Yes Query database
No Yes
Collect data Repository available
No Assign diagnosis
Process response Yes
Reply arrived
Wait for response Interpret data
Problem discovered
No
Timeout
Yes Monitor trustworthy
Log
No Log data
Yes
In the Collect data state, the monitor gathers raw data from the node (CPU usage, memory usage, available storage, number of executing tasks). It moves afterwards to the Retrieve information state. If the guard Repository available is veri ed, the logs are queried. The monitor moves to the Assign diagnosis state, where data are interpreted. If the guard Problem discovered holds then the monitor moves to the Report problem state, otherwise it moves to the Log data state. From Report problem state, the monitor communicates the detected problem to other monitors assigned to the same node and moves to the Log data state. Information are then saved in the local repository.
Listing 5.1. AsmetaL speci cation of the monitor program r u l e r MonitorProgram = par i f ( m o n i t o r s t a t e ( s e l f ) = ACTIVE) then par r SendRequest [ s e l f ]
m o n i t o r s t a t e ( s e l f ) := WAIT FOR RESPONSE endpar e n d i f
i f ( m o n i t o r s t a t e ( s e l f ) = WAIT FOR RESPONSE) then i f ( h e a r t b e a t r e s p o n s e a r r i v e d ( l a s t ( h e a r t b e a t s ( s e l f ) ) ) ) then i f ( heartbeat timeout ( l a s t ( h e a r t b e a t s ( s e l f ) ) ) ) then par r StopRequest [ ]
m o n i t o r s t a t e ( s e l f ) := REPORT PROBLEM endpar e l s e par endpar e n d i f r ProcessResponse [ ] m o n i t o r s t a t e ( s e l f ) := COLLECT DATA e n d i f e n d i f i f ( m o n i t o r s t a t e ( s e l f ) = COLLECT DATA) then par r GatherMetrics [ ] m o n i t o r s t a t e ( s e l f ) := RETRIEVE INFO endpar e n d i f i f ( m o n i t o r s t a t e ( s e l f ) = RETRIEVE INFO) then seq i f ( i s R e p o s i t o r y A v a i l a b l e ) then
r QueryDb [ ] e n d i f m o n i t o r s t a t e ( s e l f ) := ASSIGN DIAGNOSIS endseq e n d i f i f ( m o n i t o r s t a t e ( s e l f ) = ASSIGN DIAGNOSIS) then seq r I n t e r p r e t D a t a [ ] i f ( isProblemDiscovered ( s e l f ) ) then
m o n i t o r s t a t e ( s e l f ) := REPORT PROBLEM e l s e
m o n i t o r s t a t e ( s e l f ) := LOG DATA e n d i f endseq e n d i f i f ( m o n i t o r s t a t e ( s e l f ) = REPORT PROBLEM) then par r G o s s i p I s s u e [ ] m o n i t o r s t a t e ( s e l f ) := LOG DATA endpar e n d i f i f ( m o n i t o r s t a t e ( s e l f ) = LOG DATA) then par r Log [ ] i f ( isMonitorTrustworthy ( s e l f ) ) then
m o n i t o r s t a t e ( s e l f ) := ACTIVE e l s e
m o n i t o r s t a t e ( s e l f ) := INACTIVE e n d i f endpar
At the end of the monitoring cycle, the trustworthiness of the monitor is calculated and if the Monitor trustworthy guard holds, a new cycle starts. Otherwise, the monitor moves to the Inactive state from where it needs to be reinitialized by the middleware. We, thus, avoid having faulty monitors in the system. 5.2
ASMETA 1is a toolset for simulating and validating ASM models written in the AsmetaL language, which capture control structures and functions. The Monitor domain is part of the Agent universe and it behaves as an ASM machine, having its own states and transitions. Monitor state is expressed as a controlled function which is updated by the agent itself. Monitors assigned to a node are expressed as a sequence, each storing a sequence of Hearbeat requests sent to the node. The function isProblemDiscovered is left abstract. isMonitorTrustworthy function is calculated at the end of a monitoring cycle. The calculation of heartbeat timeout is a derived function combining a monitored value and a controlled function. The signature of domains and functions of the Monitor agent are important for the representation of the control state ASM from Section 5.1 in Listing 5.1 2. 5.3
Currently, validation deals only with the separate processes for each agent. It
checks the work ow and the transitions from di erent states. The model was
validated with AsmetaV tool, which allows the creation of scenarios with the
aid of the Avalla language described by [
For validation we created an instance of the Node domain, which is assigned three Monitor agents. We checked how various inputs a ect the control ow of the monitors and if the rules and states of the agent match the control state ASM ground model from Fig. 1 as displayed in Listing 5.2. In a future step of the validation process we plan to analyze the interaction between monitor agents and the function to update the con dence degree of a monitor. 6
Formal methods have distinguished themselves through the ability to capture
mathematical properties in software speci cation. LDS systems introduce a higher
complexity and heterogeneity that needs to be handled. We consulted the area
of formal methods and chose the ASM technique proposed by [
Modeling LDS has been addressed in several cloud and grid related projects.
CloudML, an extension of the UML language for expressing cloud speci c
processes, has been proposed by the MODACloud project for specifying adaptable
Quality of Service (QoS) models, monitoring operation rules and data [
Listing 5.2. Example on an AsmetaV scenario ssssssteeeecettttepnhhhaasreeesiaaaoirrrgtttnbbbMeeeeodaaantttim(((tmmmoornooo1innntiiiotttrooosrrr(231n)))od:::e===1 )hhh eee:aaa=rrr ttt bbb[ meeeaaaotttni213to;;;r 1 , monitor 2 , monitor 3 ] ; check m o n i t o r s t a t e ( monitor 1 ) = WAIT FOR RESPONSE and m o n i t o r s t a t e ( monitor 2 ) = cssssssshteeeeeeettttttepckhhhhhhWWeeeeee maaaaaaAArrrrrrIIoTTttttttnbbbbbbFFieeeeeetOOaaaaaaoRRttttttr RRllrrrrsEEaaeeeetSSttassssPPeepppptOOnneooooNNcc(nnnnyySSmssssEE((eeeeohhnaaaaaaeeinnrrrraatddrrrrorriiiittrvvvvbbmmeeee1eeoodddd)aann((((ttii=hhhhtt31eeeeooC))aaaarrOrrrr::Lsstttt==LbbbbttEaaeeeeCttaaaa15eeTtttt5;((;D3221mmA))))ooTnnA::::====iittaoontttrrfdrrra33uuul seee))me;;;==o;RnEWitPAoOIrRTTsFtPOaRRtOeRB(LEmESMPoOn;iNtSoEr; 2 ) = cssshteeettepckihRseERmaPeroOptnRboiTestaiPottRroOrlsBaytLtAaEetvMneac(iyamlna(odbhnleiematoro:tr=nbi1et)afoatr=l2sseRt)aE;t:T=eR(ImE2V0o;EniItNoFrO3 )an=d LmOoGnDi AtoTrA;s t a t e ( monitor 2 ) = s e t isMonitorTrustworthy ( monitor 3 ) := true ; csshteetepckiLsOPmGrooDnbAilteTomArDasintsdac otevme(ormneoidtn(oimtroosrnti1att)oer=(1mA)oSn:S=iItGoNtrrD3uIe)A;=GNAOCSTISIVEa n;d m o n i t o r s t a t e ( monitor 2 ) = s e t isMonitorTrustworthy ( monitor 2 ) := true ; cshteepck amnodn imt oorn isttoart es t(amtoen(imtoorni1t)or=3 R)E=POWRTAIPTROFOBLRERMESaPnOdNSmEo;n i t o r s t a t e ( monitor 2 ) = ACTIVE
Formal modeling was also used for building models for grid services and
processes. The ASM technique contributed to the description of the job
management and service execution in [
ASMs have been also proposed for realization of web service composition. In
[
Formal methods ensure reliable software solutions. LDS introduce a high complexity in the system and building formal models for them is still a challenging task. We discussed in this paper the aspects of monitoring LDS, proposed a set of requirements and translated them to an ASM model. The choice of the ASM technique was justi ed by comparing it with other available formal methods.
The current model is limited to a set of states and rules that capture the work ow of the monitors. Timing related constraints, which are essential for LDS, could not be expressed. However, the focus is on ensuring the correctness of the monitoring behavior and improving the overall robustness of the system.
As a future work, we will improve the formal model to capture ner-level details. We plan to achieve loose-coupling by employing ASM modules for di erent functionality of the monitoring framework. In order to ensure the correctness of the solution we will perform veri cation with the aid of AsmetaSMV tool.