Abstract
We present , a bounded to statically analyse Quality of Service ( ) properties of message-passing systems. We consider QoS properties on measurable application-level attributes as well as resource consumption metrics, for example, those relating monetary cost to memory usage. The applicability of is evaluated through case studies and experiments. A first case study is based on the AWS cloud while a second one analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of . These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.
Research partly supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No 778233, the PRIN PNRR project DeLICE (F53D23009130001), “by the MUR dipartimento di eccellenza”, by PNRR MUR project VITALITY (ECS00000041), Spoke 2 ASTRA - Advanced Space Technologies and Research Alliance , and Principles of Intelligent Behavior in Biological and Social Systems – PIBBSS, https://pibbss.ai/.
The authors thank the anonymous reviewers for their constructive comments and Omar Inverso for his suggestions.
Carlos G. Lopez Pombo—On leave from Instituto de Ciencias de la computación CONICET–UBA and Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires.
You have full access to this open access chapter, Download conference paper PDF
1 Introduction
Monolithic applications are steadily giving way to distributed cooperating components implemented as services. This transition was accelerated by the software-as-a-service motto triggered in the 21\(^\text {st}\) century by the service-oriented computing (SOC) paradigm, later evolved in e.g., cloud, fog, or edge computing. These paradigms envisage software systems as applications running over globally available computational and networking infrastructures to procure services that can be composed on the fly so that, collectively, they can fulfil given goals [1].
Key to this trend are Service Level Agreements (SLAs) that express the terms and conditions under which services interact. An essential element covered by SLAs are the quantitative constraints specifying non-functional behaviour of services. For example, the current SLA and pricing scheme for the AWS Lambda service [2, 3] declare constraints on quantifiable attributes. To the best of our knowledge, the standard practice is to informally specify the SLA of each service provided and then use run-time verification (like monitoring) to check quantitative non-functional properties. This approach makes it difficult to check system-level properties because SLAs (besides being informal) do not specify conditions on the composition of services.
Since their introduction in [4], choreographies stood out for a neat separation of concerns: choreographic models abstract away local computations focusing on the communications among participants; therefore, they are spot on for services since they reconcile the ‘atomistic’ view at the services’ interactions level with the ‘holistic’ view at the system level. Indeed, choreographies require to specify a high-level description of interactions (the global view) and relate it to a description of services’ behaviour (the local view). These are distinctive features of the choreographic framework presented in [5] to provide reasoning capabilities about the QoS of communicating systems, starting from the QoS of the underlying services. The basic idea in [5] is: (i) to specify constraints on quality attributes of local states of services and (ii) to verify through a bounded model-checking algorithm system-level QoS properties expressed in \(\mathcal{Q}\mathcal{L}\), a specific dynamic logic where temporal modalities are indexed with global choreographies (g-choreographies [6], a formal model of global views of choreographies). A simple example can illustrate this. Let be a service that converts files to various formats and invokes a storage service to the results of requests; both and charge customers depending on the size of stored data (as done e.g. by Amazon’s DynamoDB service). The request of to can be abstracted away with two finite-state machines whose states are decorated with constraints on the two quality attributes: monetary cost (\(\textsf{c}\)) and data size (\(\textsf{s}\)) as follows:
Intuitively, the formulae associated to states constraint the quality attributes upon the local computation executed in the states. For instance, both services store no data in their initial state; computation in may cost up to five units before the request to , which has no cost (\(\textsf{c} = 0\)) in \(q_0'\) since it is just waiting to execute the input. If, as we assume, communication is asynchronous, then the composition of and yields a run like where first sends the message and then received it. Then, the system-level QoS of the composition of and would be the result of aggregating the constraints on \(\textsf{c}\) and \(\textsf{s}\) along the run \(\pi \).
Structure & Contributions A main contribution of this paper is a tool to support the static analysis technique of QoS properties of message-passing systems. More precisely, we implement the bounded model-checking algorithm introduced in [5] (and summarised in Sect. 2) in a tool called (after for properties). By combining the SMT solver Z3 [7] and the choreographic development toolchain [8,9,10] (as discussed in Sect. 3), can model-check QoS properties expressed in \(\mathcal{Q}\mathcal{L}\), the dynamic temporal logic of [5]. is publicly available at [11].
A key feature of our approach is that the analysis of QoS properties of systems builds on the QoS constraints specified on the components of the system; as seen in the example above, features the capability of aggregating QoS constraints along the computation of systems.
Another contribution is the empirical evaluation of our approach (Sect. 4), which is done through: (a) a case study borrowed from the AWS Cloud [12], (b) a case study borrowed from the literature [13] where communication protocols are automatically extracted from code, and (c) synthetic examples designed to evaluate the scalability of .
Section 5 discusses related work; Sect. 6 concludes and sketches future work.
2 Preliminaries
We fix a set of participants (identifying interacting services) and a set of (types of) messages such that . The communication model of hinges on QoS-extended communicating finite-state machines [5] (qCFSMs for short). A CFSM [14] is a finite state automaton whose transitions are labelled by output or input actions. An output action (resp. input action ) specifies the output (resp. input) of a message from to (resp. received by from ). A qCFSM is a CFSM where QoS specifications, that is first-order formulae predicating over QoS attributes, decorate states. (Unlike CFSMs, qCFSMs feature accepting states, represented here as double circles.)
Example 1
Let \(\varGamma _\textrm{A}=\{5 \leqslant \textsf{mem} \leqslant 10, \textsf{cost} = 0.2 \cdot \textsf{mem}\}\) and \(\varGamma _\textrm{B}=\{\textsf{mem} = 0, \textsf{cost} = 1\}\) be two QoS specifications. In the system made of the qCFSMs
participant first sends message to , then and exchange messages and an unbounded number of times, and finally sends message to . \(\diamond \)
A QoS-extended communicating system (qCS for short) is a map assigning a qCFSM to participants in ; for instance, the map \(S\) where and are the qCFSM of Example 1 is a communicating system. Since QoS specifications do not affect communications, the semantics of qCSs is as the one of communicating systems. Let us recall how CFSMs interact.
Communicating systems are asynchronous: the execution of an output action allows the sender to continue even if the receiver is not ready to receive; message is appended in an infinite FIFO buffer, the channel , from where can consume . Formally, given a communicating system \(S\) on , we define a labelled transition system (LTS) whose transitions relate configurations and communication actions. A configuration is a pair \(\langle {\mathfrak {q} \ ; \ \mathfrak {\mathfrak b}} \rangle \) where \(\mathfrak q\) and \(\mathfrak b\) respectively maps each participant to a state of and each channel to a sequence of messages; state keeps track of the state of machine and buffer yields the messages sent from to and not yet consumed. Let \(s_0\) denote the initial configuration where, for all , is the initial state of and is the empty sequence for all channels .
A configuration \(\langle {\mathfrak {q} \ ; \ \mathfrak {\mathfrak b}} \rangle \) reaches another configuration \(\langle {\mathfrak {q'} \ ; \ \mathfrak {\mathfrak b'}} \rangle \) with a transition if there is a message such that either (1) or (2) below holds:
in (1) is sent on while in (2) it is received. Machines and buffers not involved in the transition are left unchanged. We write when \(s\) reaches \(s'\).
Let \(S\) be a communicating system, a sequence where I is an initial segment of natural numbers (i.e., \(i-1 \in I\) for each \(0 < i \in I\)) is a run of \(S\) if is a transition of \(S\) for all \( i \in I\). The set of runs of \(S\) is denoted as \(\varDelta ^\infty _{S}\) and the set of runs of length k is denoted as \(\varDelta ^k_{S}\). Note that \(\varDelta ^\infty _{S}\) may contain runs of infinite length, the set of finite runs of \(S\) is the union of all \(\varDelta ^k_{S}\) and will be denoted as \(\varDelta _{S}\). Given a run \(\pi \), we define \(\mathcal {L}[\pi ]\) to be the sequence of labels . The language of \(S\) is the set \(\mathcal {L}[S] = \{\mathcal {L}[\pi ] \;\big |\;\pi \in \varDelta ^\infty _{S}\}\). Finally, \( prf : \varDelta ^\infty _{S} \rightarrow 2^{\varDelta _{S}}\) maps each run \(\pi \in \varDelta ^\infty _{S}\) to its set of finite prefixes. As usual, for all \(\pi \in \varDelta ^\infty _{S}\), the empty prefix \(\epsilon \) belongs to \( prf (\pi )\).
The logic \(\mathcal{Q}\mathcal{L}\) is introduced in [5] to express system-level QoS properties. Akin \( DLTL \) [15], \(\mathcal{Q}\mathcal{L}\) is basically a linear temporal logic where atomic formulae, ranged over by \(\psi \), constrain quantitative attributes, and the ‘until’ modality is restricted to specific runs. The syntax of \(\mathcal{Q}\mathcal{L}\) is given by the grammar:
where \(\top \) is the truth value ‘true’, \(\lnot \) and \(\vee \) are the usual connectives for logical negation and disjunction, and the index \(\textsf{G}\) of the ‘until’ modality is a global choreography (g-choreographies for short) [6] meant to restrict the set of runs to be considered for the satisfiability of formulaeFootnote 1. G-choreographies can be thought of as regular expressions on the alphabet , where is used to stop iterations and represents an interaction where and exchange message . We let , and respectively denote choice operator, Kleene star, and sequential composition (with taking precedence over ).
Example 2
The g-choreography corresponds to the qCS in Example 1 with specifying the exchange of messages and between and . \(\diamond \)
A g-choreography \(\textsf{G}\) induces a causality relation on the underlying communication whereby the output of an interaction precedes the corresponding input and, for the sequential composition \(\textsf{G}; \textsf{G}'\) the actions in \(\textsf{G}\) precede those in \(\textsf{G}'\) when executed by a same participant. The language \(\mathcal {L}[\textsf{G}]\) of a g-choreography \(\textsf{G}\) consists of all possible sequences of communication actions compatible with the causal relation induced by \(\textsf{G}\) (note that \(\mathcal {L}[\textsf{G}]\) is prefix-closed). We write \(\hat{\mathcal {L}}[\textsf{G}]\) for the set of sequences in \(\mathcal {L}[\textsf{G}]\) that are not proper prefixes of any other sequence in \(\mathcal {L}[\textsf{G}]\). The definition of \(\mathcal {L}[\textsf{G}]\), immaterial here, can be found in [6]. The next example illustrates how to express a QoS property in \(\mathcal{Q}\mathcal{L}\).
Example 3
(QoS properties). The runs of the system where where and exchange message and three times can be specified by the g-choreography where \(\textsf{G}_{\textsf{exch}}\) is defined in Example 2. Then the \(\mathcal{Q}\mathcal{L}\) formula holds either if the first three exchanges do not have positive cost or if the cost of every subsequent exchange falls within the specified bounds. \(\diamond \)
The models of \(\mathcal{Q}\mathcal{L}\) are defined in terms of runs of a QoS-extended communicating systems and an aggregation function [5] that formalises the conditions for a QoS property to hold in a run. The aggregation function, denoted below as depends on application-dependent binary aggregation operators that define how QoS attributes accumulate along a run. Hereafter, we assume that each QoS attribute has an associated aggregation operator.
A configuration is accepting if all participants are in an accepting state; a completion of a run \(\pi \) of a system \(S\) is a sequence \(\pi '\) ending in an accepting configuration such that \(\pi \pi ' \in \varDelta ^\infty _{S}\). A QoS property \(\varPhi \) is satisfiable in \(S\) if there exists a run \(\pi \in \varDelta ^\infty _{S}\) with an accepting configuration such that \(\langle {\pi , \epsilon } \rangle \models _{S} \varPhi \) holds, where relation \(\langle {\_,\_} \rangle \models _{S} \_\) is defined as follows:
To handle atomic formulae, the first clause leverages real-closed fields (RCFs), a decidable formalisation of the first-order theory of real numbers [16, Thm. 37]. The ‘until’ modality requires \(\varPhi _2\) to hold at some point along \(\pi \), i.e. on a run \(\pi '\pi ''\) where completion \(\pi ''\) follow run \(\pi \), with \(\varPhi _1\) satisfied up to that point and \(\pi ''\) compatible with \(\textsf{G}\). A run \(\pi ''\) is compatible with a g-choreography \(\textsf{G}\) if it belongs to its language \(\hat{\mathcal {L}}[\textsf{G}]\).
A QoS property \(\varPhi \) is valid if, for all runs \(\pi \in \varDelta ^\infty _{S}\) that contain an accepting configuration, \(\langle {\pi , \epsilon } \rangle \models _{S} \varPhi \). Given a QoS property \(\varPhi \), a qCS \(S\), and a bound k, the algorithm in [5] returns true when it finds a run \(\pi \in \varDelta ^\infty _{S}\) of length at most k such that \(\langle {\pi , \epsilon } \rangle \models _{S} \varPhi \). Essentially, for each run of length at most k, the algorithm calls an auxiliary procedure that checks whether the run satisfies the QoS property by recursively following the definition of \(\models _{S}\) presented above.
3 A Bounded Model Checker for QoS
We now present the architecture of ; a detailed presentation of its command line interface and the relevant file formats is in the accompanying artefact submission [11]. A graphical representation of the architecture is on the right, where tilted boxes represent files or data objects, rectangular boxes represent modules or functions, while arrows represent control and data flows. Thick shadowed boxes identify the modules developed in this work, while thin boxes identify modules and other open-source libraries used by .
As , is implemented in Haskell. The two main modules are Parser and Solver (greyed dashed boxes). The former transforms the textual representations of inputs into internal Haskell representations used by the latter. More precisely, qCFSM parser leverages CFSM parser to process a textual description of the system from a .qosfsa file. Likewise, QL parser leverages G-chor parser ( g-choreographies parser) to process a .ql file containing a simple textual description of the \(\mathcal{Q}\mathcal{L}\) formula to verify. Both modules rely on the SMT-LIB parser (Haskell’s smt-lib package).
The format of .qosfsa files is an extension of .fsa format. This extension enables the specification of the set of QoS attributes of interest with (i) aggregation operators, (ii) QoS constraints associated to the states of machines, and (iii) accepting states of machines. Additionally, supports an extension of g-choreographies (a .qosgc file) to directly specify the QoS-related information over a g-choreography that can be projected on qCFSMs. This required to adapt G-chor projection and G-chor parser modules to support QoS specifications.
The .ql format borrows the g-choreography syntax of for the case of the ‘until’ modality. The Parser module produces the QoS-extended system and the QL formula from the input files and passes them to Solver, our implementation of the bounded model checking algorithm in [5] (cf. Sect. 2). More precisely, TS run enumerator invokes Transition system semantics (the TS module of ) to enumerate the runs of the system that fall within the bound given in input parameter k. The enumeration is performed by systematically traversing the transition system. The process begins with the set of runs of length 1. Subsequently, the set of runs of length \(i+1\) is generated by appending all possible single-step transitions to each run of length i. Future work will explore heuristic-based approaches to traverse the transition system, aiming to prioritize the enumeration of potential counterexamples.
Then, TS run enumerator invokes TS run checker on each enumerated run to check if it is a model of the \(\mathcal{Q}\mathcal{L}\) formula. Properties encompassing sub-formulas of the form \(\varPhi \;\mathbf {\textsf{U}}^{\textsf{G}}\;\varPhi '\) require TS run checker to invoke PomsetSemantics module in order to compute the language of \(\textsf{G}\) and to check membership of runs to it. To compute \(\hat{\mathcal {L}}[\textsf{G}]\), iterative subterms are replaced by their n-unfoldings, where \(0 \leqslant n \leqslant \texttt {u}\). The parameter u is configurable via the CLI of and defaults to the value of parameter k. An n-unfolding of a subterm is defined as the sequential composition of \(\textsf{G}'\) with itself n times. The implementation of on-the-fly unfolding computation during transition system traversal is left for future work.
As recalled in Sect. 2, we leverage RCFs to express QoS constraints [5]; hence, we interfaced with the state-of-the-art SMT solver Z3 [7] to check the validity of these constraints (i.e., \(\vdash _{ RCF }\)). Properties involving QoS constraints of an atomic formulae require TS run checker to invoke the SMT solver interface to produce and check SMT-LIB queries. The SMT solver interface is composed of a modified version of Haskell’s smt-lib package to build the SMT-LIB query and of Haskell’s SimpleSMT package to call Z3. The SMT-LIB query produced for an atomic formula \(\psi \) allows to check whether there exists a counterexample to the entailment . More precisely, the SMT-LIB query is structured as follows: (i) all quality attributes are declared as new symbols of sort Real using the declare-const command, and (ii) an assert statement is included with the expression . The construction of within the SMT-LIB query involves iterating through local states in run \(\pi '\). For each state, the following steps are performed: (i) the corresponding QoS specification is collected, (ii) new symbols are declared for the local instantiation of quality attributes, and (iii) quality attribute symbols in the QoS specification are renamed to match the newly declared symbols. The SMT-LIB query is then sent to Z3 using Haskell’s SimpleSMT package.
Finally, Solver returns a negative Verdict if the formula cannot be satisfied within the given bounds or a positive Verdict with a witnessing model (the run satisfying the QL formula) otherwise. To optimise computations, maintains a balanced binary search tree to store the result of computing atomic entailments \(\_ \vdash _{ RCF } \_\), and a hash table to memorises the results of (a) the computation of the language of g-choreographies indexing ‘until’ operators, and (b) the membership check of a run to the language of a g-choreography.
4 Evaluation
Our empirical study aims to evaluate applicability and scalability of our approach. Towards applicability, Sect. 4.1 develops a case study adopting SLAs from the AWS cloud [12] while Sect. 4.2 borrows a case study from [13] to show how our approach can leverage automatic extraction of communicating systems. Towards scalability, Sect. 4.3 analyses to measure its performance. Size and complexity of the case studies in Secs. 4.1 and 4.2 match what can be found in the literature (e.g., see [17,18,19]). As we will discuss later, the size of the models in Sect. 4.3 outmatches what can be found in system development.
The results presented in the next sections show that our framework can model SLAs present in industrial-strength scenarios (Sect. 4.1). Notably, can effectively verify relevant system-level QoS in such scenarios and produce counterexamples useful to refine a property being checked. Moreover, Sect. 4.2 can be used to effectively analyse system-level QoS properties of communicating systems automatically extracted from code.
4.1 SLA in the Amazon Cloud
The case study consists of a three-party version of the POP protocol [20] modelled after the OAuth authentication protocol [21]. More precisely, a client securely accesses a remote mailbox server after clearing authentication through a third party server . This is specified by the g-choreography where \(\textsf{G}_{\textsf{token}}\) models the phase of the OAuth protocol where acquires an authentication token granted if the credentials of the client are valid; the acquired token allows to prove its identity to the POP server . This can be modelled as follows:
We consider a system of qCFSMs, one per participant, realising the g-chore-ography \(\textsf{G}_{\textsf{auth}}\) (see [22, Appendix A] for the full model). The states of the qCFSMs are decorated by QoS specifications derived by publicly available SLAs. Specifically, we use the SLA of the Ory Network identity infrastructure [23] for , the one for reflects the SLA of clients of Amazon’s Simple Email Service (SES) [24], and the SLA of is modelled after the iRedMail service published in the AWS marketplace [25]. Our approach requires to constrain the quality attributes for each state of the participant while the constraints specified in the publicly available SLAs are relative to the whole execution. We overcome this obstacle by identifying the states in the qCFSMs which are relevant to the constraint. We then assign a corresponding QoS specification to each of these identified states. For example, the SLA of Amazon SES specifies that the price paid for each incoming email is \(10^{-4}\) USD; this decorates the state in the client’s qCFSM where mails are received.
We identified the quality attributes in Table 1 (left column) and the pricing and configuration parameters (right column in Table 1) that fix the elements of the computational infrastructure required. The value of the parameters are determined by the value of the instance type attribute, which models the type of the compute instanceFootnote 2 chosen by the user when configuring the services. This relation is rendered in our model with logical implications. For example, AWS stipulates that if the selected instance type is ‘t4g.nano’ (the smallest compute instance in the family ‘T4g’ represented as \(\textsf{instType} = 1\) in our model), the hourly rate for compute is 0.0042USD; this yields the implication
to be included in the QoS specification of the initial state of the server qCFSM together with analogous implications for other instance types. The full model of our case study is an LTS with 34 configurations and 38 transitions obtained by the composition of three qCFSMs: the client (15 states and 17 transitions), the server (12 states and 14 transitions), and the authentication server (4 states and 3 transitions). Note that CFSMs abstract away from local computations and focus only on the communication actions. Hence, the number of states and transitions only reflect the size of the communication protocol and not necessarily the size of the implementation. The QoS specifications we consider predicate over the 14 quality attributes in Table 1. Due to space limitations, here we only show the qCFSM for the server (the other qCFSMs are in [22, Appendix A]):
where \(\varGamma _\textrm{comp}= \{ 0.5 < \textsf{execTime} < 3, \textsf{execTimeServer} = \textsf{execTime} \}\) and \(\varGamma _\textrm{data}= \{ 10< \textsf{dataTransOut} < 500 \}\), respectively modelling states where the server is performing significant computations and states where the server has sent data to the client. The specification \(\varGamma _\textrm{init}\) models the configuration of the AWS instance as stated earlier (see [22, Appendix A] for a full description). Let us focus on some system-level properties to be checked with .
By inspecting the SLAs for AWS pricing scheme, we can derive the expression
for the overall cost of an execution of the system in terms of the aggregated values of the quality attributes, once the appropriate conversions are applied. We can then consider the \(\mathcal{Q}\mathcal{L}\) formulae in Table 2 to check if the cost for receiving one email falls below a given threshold (\(\varPhi _1\)) and some relations between the total cost of an execution and the number of emails retrieved by the client (\(\varPhi _2\), \(\varPhi _3\), and \(\varPhi _4\), which require to iterate the g-choreography \(\textsf{G}_\textsf{msg}\)). Both the validity of \(\varPhi _1\) and a counterexampleFootnote 3 for \(\varPhi _2\) are computed by in less than a second. In these cases it is not necessary to check for high values of the bound \(\textsf{k}\) because no iterative g-choreography occurs in \(\varPhi _1\) and the counterexample of \(\varPhi _2\) is found at \(\mathsf {k=26}\). The validity of the other formulae for a high value of \(\textsf{k}\) is checked by in less than 3 min.
4.2 Model Extraction
We show how to apply on a model automatically inferred from the OCaml code of the case study in [13]. The system inferred in [13] is as followsFootnote 4
The user requests the master to resolve a problem (whose nature is inconsequential here). The master splits the problem into two tasks and sends them to the worker, which replies to the master with the solutions of each task; between these replies, the master sends a ‘work-in-progress’ message to the user. Finally, the master sends the final result to the user by combining the partial results
The QoS specifications involve price, number of tasks computed, and allocated memory, respectively denoted with \(\textsf{p}\), \(\textsf{t}\), and \(\textsf{mem}\). The contraints over these attributes have been manually specified and assigned to the states of the qCFSMs. For instance, we assume each problem instance (requested from the user) to require at most 5 units of memory and model this by adding a contraint over \(\textsf{mem}\) to the states where memory is allocated for the problem intance. Similarly, we assume the result of the problem to require at most 1 unit of memory. Additionally, we assume that the master charges a flat fee of 10 monetary units once the computation is completed, while the worker’s cost varies based on the size of the task. We check the following \(\mathcal{Q}\mathcal{L}\) properties:
where \(\textsf{G}\) describes the process of computing one problem instance, starting with and ending with ([22, Appendix C] reports the details about the models of this case study.) Formula \(\varPhi _1\) uses the necessity modality to express bounds on the price of the computation of one problem instance. Formulas \(\varPhi _2\) and \(\varPhi _3\) use the necessity modality to express bounds on the price and the memory used after computing any number of problem instances. Formula \(\varPhi _4\) states that (i) up to the computation of the first problem instance, the price falls below a bound depending on the number of tasks computed, and (ii) afterwards, the price is always bounded by 25 right after any number of computed problem instances. We applied on these formulas with bounds that correspond to unfolding loops once and twice (\(\textsf{k} = 18\) and \(\textsf{k} = 32\) are, respectively, the lengths of runs where the master sends the result of one and two problem instances and the user stops). The results of the experiments are summarised in Table 3 where times are in seconds. Noticeably, for satisfiability the results with \(\textsf{k} = 18\) subsume those with \(\textsf{k} = 32\); also, for \(\varPhi _4\), a bound of 32 is needed to find a counterexample, which shows that the formula is satisfiable but not valid.
4.3 Performance
The performance of depends on the cost of checking if a formula \(\varPhi \) holds on any run of the system S of length at most k; this cost is dominated by the evaluation of the ‘until’ sub-formulaeFootnote 5 \(\varPhi _1 \;\mathbf {\textsf{U}}^{\textsf{G}}\;\varPhi _2\) which depends on the complexity of \(\textsf{G}\) and of \(\varPhi _1\) and \(\varPhi _2\). We therefore generate synthetic properties following the pattern \(\varPhi \equiv \varPhi _1 \;\mathbf {\textsf{U}}^{\textsf{G}}\;\varPhi _2\) and varying the size and complexity of \(\textsf{G}\). Formulas \(\varPhi _1\) and \(\varPhi _2\) are created to cover (i) the best case (any run that matches the language of \(\textsf{G}\) satisfies \(\varPhi \)), (ii) the worst case (no run matching the language of \(\textsf{G}\) satisfies \(\varPhi \)), and (iii) the ‘average’ case (only a single random run that matches the language of \(\textsf{G}\) satisfies \(\varPhi \)).
The performance analysis of was driven by experimentsFootnote 6 tailored to address the following questions:
-
Loop unfolding. How does performance evolve as we increase the number of loop unfoldings in g-choreographies indexing ‘until’ sub-formulae?
-
Nested choices. How does average performance evolve as we increase the number of nested choices in g-choreographies indexing ‘until’ sub-formulae?
Loop unfolding. The experiments are performed on the set of qCFSMs described in the AWS cloud case study in Sect. 4.1. To help the reader understand the size of the problem, we show below the number of runs of this system as a function of the bound k on the size of the runs. Due to interleaving of the transitions in the asynchronous communication, the number of runs grows exponentially when the number of loop unfoldings in the POP protocol increases.
We synthetically generate six families of \(\mathcal{Q}\mathcal{L}\) formulas with the shape \(\varPhi _1 \;\mathbf {\textsf{U}}^{\textsf{G}}\;\varPhi _2\) where \(\textsf{G}= \textsf{G}_\textsf{init};{\textsf{G}_\textsf{msg}}^n\), for \(1 \leqslant n \leqslant 10\), with \(\textsf{G}_\textsf{init}\) and \(\textsf{G}_\textsf{msg}\) defined as in Sect. 4.1. The first three families of formulas are constructed to be satisfiable while the last three to be unsatisfiable. The unsatisfiable formulas are constructed by guaranteeing that no run compatible with \(\textsf{G}\) satisfies \(\varPhi _2\). For each formula we execute with a bound \(\texttt {k} = 16 + 10n\), which guarantees that the runs of the system that match \(\textsf{G}\) are reached. The results are shown in Fig. 1. Figure 1a plots the time it takes for to find a model for the three families of satisfiable formulas as a function of n. The three families differ in how \(\varPhi _1\) and \(\varPhi _2\) are constructed: (i) both as atomic truth values, (ii) \(\varPhi _1\) as an atomic truth value and \(\varPhi _2\) as a QoS constraint, or (iii) both as QoS constraints. Figure 1b plots the time takes to report that no model was found for the three families of unsatisfiable formulas as a function of n. The results show that the main source of computational burden, as the number of loop unfoldings increases, is the verification of the QoS constraint in \(\varPhi _1\), the first operand of the ‘until’ operator. In Fig. 1a and Fig. 1b, this is manifested by the green line growing significantly faster than the other two lines. The explanation for this is that, due to the semantics of the ‘until’, the verification of \(\varPhi _1\) has to be performed in every prefix of the run and, when \(\varPhi _1\) is a QoS constraint, each verification is done by calling Z3 with a different SMT-LIB query.
Nested choices. To evaluate the performance of in the presence of nested choices indexing ‘until’ sub-formulae, we will construct synthetic systems by varying the number of nested choices in the g-choreography of the system. We consider systems of two participants taking turns in sending a message to each other; the sender of each turn chooses between two messages. Due to the branching nature of this behaviour, the number of runs in a system grows as \(2^n\) where n is the number of nested choices (i.e., the number of turns). We synthetically generate systems with this behaviour by varying n from 1 to 10. Remarkably, nested choices correspond to nested conditional statements and accepted metrics recommend to keep low the nesting level of conditional statements. In particular, an accepted upper bound of cyclomatic complexityFootnote 7 is 15, which corresponds to less than 4 nested conditional statements.
To generate these systems, we craft QoS-extended g-choreography in .qosgc format and then leverage G-chor projection to obtain the qCFSMs of the system. The QoS specifications comprise five QoS attributes and determine unique values for them in each accepting state, enabling the construction of \(\mathcal{Q}\mathcal{L}\) formulas that are satisfied by only one run of the system. In this way, we can use these generated cases to evaluate the performance of in finding the only run that satisfies a formula in a search space of exponential size in n.
The formula is generated by following the pattern \(\top \ \;\mathbf {\textsf{U}}^{\textsf{G}}\;\ \psi \), were \(\textsf{G}\) matches every run of the system and \(\psi \) is a QoS constraint, determining the value of the five QoS attributes, that is satisfied by only one run. Figure 2a shows the generated \(\textsf{G}\) for two nested choices. See [22, Appendix B] for a detailed view of the files used in this case study. The bound k is set high enough to guarantee that all runs of the system are reached by the analysis. For each value of n, we generate 100 different random instances of the \(\mathcal{Q}\mathcal{L}\) formula, where the only run that satisfies the formula is chosen randomly, and execute on each instance. Figure 2b shows the results as a boxplot per number of nested choices. Remarkably, both the average execution time and its variance grow as n increases. This is due to the fact that the difference in time between the best and worst case scenarios, where the model is found either in the first or the last enumerated run matching \(\textsf{G}\), increases with n. The apparent bias in dispersion towards lower execution times is just a visual effect due to the logarithmic scale of the y-axis.
5 Related Work
We position in the category of static analysers of system-level QoS properties. There is a vast literature on QoS, spanning a wide range of contexts and methods [27, 28], QoS for choreographies [29, 30], and formal models and analysis procedures that have been proposed without tool supported analysis.
A tool for the automatic analysis of QoS properties appeared in [31] where QoS specifications were expressed as theory presentations over quantitative attributes but only considering convex polytopes; this restriction is not present in our language. Unlike , the approach in [31] relies on “monolithic” specifications of QoS, rendering hard its application to distributed systems without adding some composition mechanisms. We instead assign QoS contracts to states of communicating services and then aggregate them in order to analyse properties along executions of the whole system.
The Envisage project [32] aims to provide a framework for the development and deployment of virtualized scalable services in the cloud. System design and analysis is done in ABS [33, 34] which enables resource-awareness in design and deployment decisions [35,36,37]. In ABS resource awareness revolves around the concept of elasticity and the capability of simulating the execution of the system under deployment constraints. The analysis is performed to evaluate bounds over fixed attributes (Speed, Bandwidth, Memory, and Cores) in order to inspect consumption of those resources over simulated executions. On the contrary, is agnostic to the attribute’s nature, as far as it is measurable, and provides a static analysis procedure capable of exploring the whole execution space (with respect to a predefined bound to the trace length) in the search for counterexamples of arbitrary dynamic temporal properties, not only bounds.
Metric functions are used in [38] to verify SLAs of client-server systems via the interactive theorem prover KeY [39]. We can deal with multiparty system and the analysis of QoS properties of is fully automatic. Other abstract models of QoS such as quantales [40] or c-semirings [41,42,43] have been proposed. Process calculi capable of expressing SLAs appeared in [41] and in [43] without a specific analysis technique. A variant of the \(\mu \)-calculus equipped with the capability of expressing QoS properties and an analysis algorithm has been presented in [42] without an implementation.
Automatic extraction of local QoS contracts from global QoS specifications is defined and implemented in [29]; the paper proposes applications including the use of the derived contracts for monitoring but no static analysis procedure of the QoS systems’ behaviour is proposed. On the same basis, monitoring algorithms were presented in [30] and contracts are used for run-time prediction, adaptive composition, or compliance checking.
Probabilistic model checking (PMC) [44, 45] implemented in PRISM [46] features the automated analysis of quantitative properties. The main differences with respect to our work are the modelling language and the properties that can be checked. First, PMC models are usually expressed as Markov chains while does not feature probabilistic information. Second, RCFs are more expressive than the reward functions adopted in [44] since they allow to express first order formulae over QoS attributes. For example, the QoS specifications shown in Sect. 4.1 cannot be expressed with PRISM’s reward functions. Finally, while in PMC properties are expressed as temporal formulae over bounds on the expected cumulative value of a reward, can verify dynamic temporal formulae where atoms are first order formulae over QoS attributes and temporal modalities are indexed with g-choreographies. Our setting leads to the computation of an aggregation function that collects QoS specifications of states along a run, which is not the case in PMC. Timed automata [47] are used in UPPAAL [48] to verify real-time systems. Our QoS specifications can predicate about time but, unlike in UPPAAL, the behaviour of systems is independent of it. It is therefore not straightforward to compare with tools like PMC or UPPAAL as they are designed for different purposes. Extending with time and probabilities is indeed an intriguing endeavour.
6 Conclusions and Future Work
We presented , a tool to verify QoS properties of message-passing systems. We build a bounded model checker upon the dynamic logic and semi-decision procedure recently presented in [5] which rely on choreographic models. To our best knowledge, is the first tool to support the static analysis of QoS for choreographic models of message-passing systems. The satisfiability of QoS constraints in atomic formulas is delegated to the SMT solver Z3 while is used to handle the choreographic models and their semantics. Notably, can handle any quality attribute that takes values in the real numbers (if it is equipped with an appropriate aggregation operator), making it highly versatile. Experiments to evaluate the applicability of our approach were conducted over case studies based on the AWS cloud and on models automatically extracted from code. Experiments to evaluate the scalability of our approach were conducted over synthetically generated models and properties.
Our experiments demonstrate the effectiveness of . Nevertheless, there is room for improvement. We are considering abstract semantics where runs are partitioned in equivalence classes so that we have to check only representative runs of such classes in order to tackle the computational blow up due to asynchronous communications as discussed in Sect. 4.
In scope of future work is also the definition of a domain-specific language to ease the modelling phase. For instance, such language could feature data types to express non-cumulative attributes (as those used in Sect. 4.1).
Notes
- 1.
Logical connectives \(\wedge \) and \(\implies \) are defined as usual while possibility \(\langle {\textsf{G}} \rangle \varPhi \) and necessity \([\textsf{G}] \varPhi \) are defined as \(\top \;\mathbf {\textsf{U}}^{\textsf{G}}\;\varPhi \) and \(\lnot \langle {\textsf{G}} \rangle \lnot \varPhi \) respectively.
- 2.
In AWS jargon, compute refers to computational infrastructure, i.e., virtual computers that are rented through services like Amazon Elastic Compute Cloud (EC2).
- 3.
A run with 0 email retrievals, hinting at a fixed cost for executing the services.
- 4.
The thick gray arrow is the only addition we made to the original case study.
- 5.
This requires to query the SMT-LIB to solve QoS constraints; we use Z3 as a black-box which we cannot control; therfore, its computational costs are factored out.
- 6.
We used Z3 v4.10.2 and an 8-cores MacBook Pro (Apple M1) with 16 GB of memory.
- 7.
Cyclomatic complexity [26] measures the complexity of programs according to the number of independent paths represented in the source code.
References
Fiadeiro, J.L., Lopes, A., Bocchi, L.: An abstract model of service discovery and binding. Formal Aspects Comput. 23(4), 433–463 (2011)
Amazon: AWS Lambda Service Level Agreement. https://aws.amazon.com/lambda/sla/
Amazon: AWS Lambda Pricing. https://aws.amazon.com/lambda/pricing/
World Wide Web Consortium: Web Services Description Language (WSDL) Version 2.0 Part 1: Core Language. https://www.w3.org/TR/wsdl20/
Lopez Pombo, C.G., Martinez Suñé, A.E., Tuosto, E.: A dynamic temporal logic for quality of service in choreographic models. In: Ábrahám, E., Dubslaff, C., Tarifa, S.L.T., eds.: Proceedings of 20th International Colloquium on Theoretical Aspects of Computing - ICTAC 2023. Volume 14446 of Lecture Notes in Computer Science., Lima, Perú, Springer-Verlag (December 2023), pp. 119–138 (2023). https://doi.org/10.1007/978-3-031-47963-2_9
Tuosto, E., Guanciale, R.: Semantics of global view of choreographies. J. Logical Algebraic Methods. Program. 95, 17–40 (2018)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C., Rehof, J., eds.: Proceedings of 14th International Conference Tools and Algorithms for the Construction and Analysis of Systems TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008. Volume 4963 of Lecture Notes in Computer Science., Springer-Verlag (2008), pp. 337–340 (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Coto, A., Guanciale, R., Tuosto, E.: Choreographic development of message-passing applications - A tutorial. In Bliudze, S., Bocchi, L., eds.: Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings. Volume 12134 of Lecture Notes in Computer Science., Springer (2020) 20–36
Coto, A., Guanciale, R., Lange, J., Tuosto, E.: ChorGram: tool support for choreographic development (2015). https://bitbucket.org/eMgssi/chorgram/src/master/
Lange, J., Tuosto, E., Yoshida, N.: A tool for choreography-based analysis of message-passing software. In: Gay, S., Ravara, A., eds.: Behavioural Types: from Theory to Tools. Automation, Control and Robotics. River (2017), pp. 125–146 (2017)
Lopez Pombo, C.G., Martinez-Suñé, A.E., Tuosto, E.: MoCheQoS: Automated Static Analysis of Quality of Service Properties of Communicating Systems - Artifact. https://zenodo.org/doi/10.5281/zenodo.10038447. Git repository available at https://bitbucket.org/aemartinez/chorgram/src/mocheqos-fm24/. June 2024
Amazon: AWS Global Infrastructure. https://aws.amazon.com/about-aws/global-infrastructure. Accessed 27 March 2024
Imai, K., Lange, J., Neykova, R.: Kmclib: automated inference and verification of session types from OCaml programs. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 379–386. Cham, Springer International Publishing, Lecture Notes in Computer Science (2022)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)
Henriksen, J.G., Thiagarajan, P.: Dynamic linear time temporal logic. Ann. Pure Appl. Logic 96(1–3), 187–207 (1999). Originally published in [49]
Tarski, A.: A decision method for elementary algebra and geometry. Memorandum RM-109, RAND Corporation (1951) Later published in [50] and reprinted in [51]
Albert, E., et al.: Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. Serv. Oriented Comput. Appl. 8(4), 323–339 (2014). This article refines and substantially extends [52]
Iraci, G., Chuang, C.E., Hu, R., Ziarek, L.: Validating IoT devices with rate-based session types. Proc. ACM Program. Lang. 7(OOPSLA2), 1589–1617 (2023)
Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. In: Dillig, I., Tasiran, S., eds.: Proceedings of 31st International Conference Computer Aided Verification (CAV 2019), Part I. Volume 11561 of Lecture Notes in Computer Science., Springer-Verlag (July 2019), pp. 97–117 (2019). https://doi.org/10.1007/978-3-030-25540-4_6
Anonymous: Post office protocol: Version 2 (1985). https://rfc-editor.org/rfc/rfc937.txt
Hardt, D.: The OAuth 2.0 Authorization Framework (2012). https://rfc-editor.org/rfc/rfc6749.txt
Lopez Pombo, C.G., Martinez Suñé, A.E., Tuosto, E.: MoCheQoS: automated analysis of quality of service properties of communicating systems. On-line (November 2023) https://arxiv.org/abs/2311.01415
Ory: Ory - API-first Identity Management, Authentication and Authorization. For Secure, Global, GDPR-compliant Apps. https://www.ory.sh/. Accessed 3 April 2024
Amazon Web Services, Inc.: Bulk Cloud Email Service - Amazon Simple Email Service - AWS. https://aws.amazon.com/ses/. Accessed 3 April 2024
Amazon Web Services Inc.: AWS Marketplace: iRedMail (IMAP, SMTP, POP3) Email Server on Ubuntu 18.04 LTS. https://aws.amazon.com/marketplace/pp/prodview-xswbskbnidz5e. Accessed 3 April 2024
McCabe, T.J.: A complexity measure. IEEE Trans. Softw. Eng. SE-2(4), 308–320 (1976)
Aleti, A., Buhnova, B., Grunske, L., Koziolek, A., Meedeniya, I.: Software architecture optimization methods: a systematic literature review. IEEE Trans. Software Eng. 39, 658–683 (2013)
Hayyolalam, V., Kazem, A.A.P.: A systematic literature review on QoS-aware service composition and selection in cloud environment. J. Netw. Comput. Appl. 110, 52–74 (2018)
Ivanović, D., Carro, M., Hermenegildo, M.V.: A constraint-based approach to quality assurance in service choreographies. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q., eds.: Proceedings of 10th International Conference on Service-Oriented Computing – ICSOC 2012. Volume 7636 of Lecture Notes in Computer Science., pp. 252–267. Springer-Verlag (November 2012). https://doi.org/10.1007/978-3-642-34321-6_17
Kattepur, A., Georgantas, N., Issarny, V.: Qos analysis in heterogeneous choreography interactions. In: Basu, S., Pautasso, C., Zhang, L., Fu, X., eds.: Proceedings of the 11nd International Conference on Service Oriented Computing – ICSOC ’13. Volume 8274 of Lecture Notes in Computer Science., Springer-Verlag (December 2013), pp.23–38 (2013). https://doi.org/10.1007/978-3-642-45005-1_3
Martinez Suñé, A.E., Lopez Pombo, C.G.: Automatic quality-of-service evaluation in service-oriented computing. In: Nielson, H.R., Tuosto, E., eds.: Proceedings of Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019. Volume 11533 of Lecture Notes in Computer Science., Springer-Verlag (June 2019), pp. 221–236 (2019). https://doi.org/10.1007/978-3-030-22397-7_13
Envisage: Engineering Virtualized Services. http://envisage-project.eu
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M., eds.: Revised papers of the 9th International Symposium Formal Methods for Components and Objects (FMCO 2010). Volume 6957 of Lecture Notes in Computer Science., Springer-Verlag (2012), pp. 142–164 (2012)
The ABS Framework. https://abs-models.org, https://github.com/abstools/abstools
de Gouw, S., Mauro, J., Nobakht, B., Zavattaro, G.: Modeling deployment decisions for elastic services with ABS. On-line (2016). http://www.envisage-project.eu/modeling-deployment-decisions-for-elastic-services-with-abs/
de Gouw, S., Mauro, J., Nobakht, B., Zavattaro, G.: Declarative elasticity in ABS. In: Aiello, M., Johnsen, E.B., Dustdar, S., Georgievski, I., eds.: Proceedings of Service-Oriented and Cloud Computing (ESOCC 2016) - 5th IFIP WG 2.14 European Conference. Volume 9846 of Lecture Notes in Computer Science., Springer-Verlag (September 2016), pp. 118–134 (2016). https://doi.org/10.1007/978-3-319-44482-6_8
de Boer, F.S., et al.: Analysis of SLA compliance in the cloud - an automated, model-based approach. In: Ancona, D., Pace, G., eds.: Proceedings of Second Workshop on Verification of Objects at RunTime EXecution (VORTEXECOOP/ISSTA 2018). Volume 302 of EPTCS. (July 2019) pp. 1–15 (2019)
Giachino, E., de Gouw, S., Laneve, C., Nobakht, B.: Statically and dynamically verifiable SLA metrics. In: Ábrahám, E., Bonsangue, M.M., Johnsen, E.B., eds.: Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Volume 9660 of Lecture Notes in Computer Science., Springer (2016), pp. 211–225 (2016). https://doi.org/10.1007/978-3-319-30734-3_15
Din, C.C., Bubel, R., Hähnle, R.: Key-abs: a deductive verification tool for the concurrent modeling language ABS. In Felty, A.P., Middeldorp, A., eds.: Proceedings of 25th International Conference on Automated Deduction - CADE-25. Volume 9195 of Lecture Notes in Computer Science., Springer-Verlag (August 2015), pp. 517–526 (2015). https://doi.org/10.1007/978-3-319-21401-6_35
Rosenthal, K.I.: Quantales and their application. Volume 234 of Pitman research notes in mathematics series. Longman Scientific & Technical (1990)
Buscemi, M.G., Montanari, U.: Cc-pi: a constraint-based language for specifying service level agreements. In: De Nicola, R., ed.: Proceedings of 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2007). Volume 4421 of Lecture Notes in Computer Science., Springer-Verlag (2007), pp. 18–32 (2007). https://doi.org/10.1007/978-3-540-71316-6_3
Lluch-Lafuente, A., Montanari, U.: Quantitative \(\mu \)-calculus and CTL based on constraint semirings. Electron. Notes Theoret. Comput. Sci. 112, 37–59 (2005). Proceedings of the Second Workshop on Quantitative Aspects of Programming Languages (QAPL 2004)
De Nicola, R., Ferrari, G., Montanari, U., Pugliese, R., Tuosto, E.: A process calculus for QoS-aware applications. In: Jacquet, J.M., Picco, G.P., eds.: Proceedings of 7th International Conference Coordination Models and Languages, COORDINATION 2005. Volume 3454 of Lecture Notes in Computer Science., Springer-Verlag (April 2005), pp. 33–48 (2005). https://doi.org/10.1007/11417019_3
Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: The 6th Joint Meeting on European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering: Companion Papers. ESEC-FSE Companion ’07, New York, NY, USA, Association for Computing Machinery (September 2007), pp. 449–458 (2007)
Baier, C., Katoen, J.P., eds.: Principles of Model Checking. The MIT Press (2008)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification, pp. 585–591. Lecture Notes in Computer Science, Berlin, Heidelberg, Springer (2011)
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134–152 (1997)
Henriksen, J.G., Thiagarajan, P.: Dynamic linear time temporal logic. Report Series BRICS-RS-97-8, Basic Research in Computer cience (1997). https://tidsskrift.dk/brics/issue/view/2365
Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951) Originally published in [16] and reprinted in [51]
Tarski, A.: A Decision method for elementary algebra and geometry. In: Caviness, B.F., Johnson, J.R. (eds) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Vienna (1998). Originally published in [16] and reprinted from [50]. https://doi.org/10.1007/978-3-7091-9459-1_3
de Boer, F.S., Hähnle, R., Johnsen, E.B., Schlatte, R., Wong, P.Y.: Formal modeling of resource management for cloud architectures: an industrial case study. In: Paoli, F.D., Pimentel, E., Zavattaro, G., eds.: Proceedings of First European Conference Service-Oriented and Cloud Computing (ESOCC 2012). Volume 7592 of Lecture Notes in Computer Science., Springer-Verlag (September 2012), pp. 91–106 Refined and substantially extended in [17]. https://doi.org/10.1007/978-3-642-33427-6_7
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Ethics declarations
Data Availability
The source code of the tool, the code for generating the experimental data, and detailed instructions on how to reproduce the results presented in this paper are available in the Zenodo repository with the identifier https://doi.org/10.5281/zenodo.10038447. (See citation in [11]).
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2025 The Author(s)
About this paper
Cite this paper
Pombo, C.G.L., Suñé, A.E.M., Tuosto, E. (2025). Automated Static Analysis of Quality of Service Properties of Communicating Systems. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds) Formal Methods. FM 2024. Lecture Notes in Computer Science, vol 14934. Springer, Cham. https://doi.org/10.1007/978-3-031-71177-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-031-71177-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-71176-3
Online ISBN: 978-3-031-71177-0
eBook Packages: Computer ScienceComputer Science (R0)