Mahsa Zarneshan
email: m.zarneshan@ut.ac.ir

Fatemeh Ghassemi
email: fghassemi@ut.ac.ir

Marjan Sirjani
email: marjan.sirjani@mdh.se

Formal Modeling and Analysis of Medical Systems

Keywords: Communication patterns, Actor, Message passing, Reduction

Medical systems are composed of medical devices and apps which are developed independently by different vendors. A set of communication patterns, based on asynchronous message-passing, has been proposed to loosely integrate medical devices and apps. These patterns guarantee the point-to-point quality of communication service (QoS) by local inspection of messages at its constituent components. These local mechanisms inspect the property of messages to enforce a set of parametrized local QoS properties. Adjusting these parameters to achieve the required point-to-point QoS is non-trivial and depends on the involved components and the underlying network. We use Timed Rebeca, an actor-based formal modeling language, to model such systems and asses their QoS properties by model checking. We model the components of communication patterns as distinct actors. A composite medical system using several instances of patterns is subject to state-space explosion. We propose a reduction technique preserving QoS properties. We prove that our technique is sound and show the applicability of our approach in reducing the state space by modeling a clinical scenario made of several instances of patterns.

Introduction

Medical systems are composed of medical devices and apps which are developed independently by different vendors. The ASTM F2761 standard [START_REF]Astm f2761 -medical devices and medical systems -essential safety requirements for equipment comprising the patient-centric integrated clinical environment (ice)[END_REF] proposes an architecture for integrated clinical environments (ICE) that enable a componentbased approach to medical systems. The AAMI-UL JC 2800 standards completes F2671 by defining safety/security requirements for both the ICE architecture and its development process. A set of communication requirements that enables dynamic composition of devices and apps has been identified [START_REF] Robby | Integrated clinical environment device model: Stakeholders and high level requirements[END_REF]. As a solution, a set of communication patterns has been proposed in [START_REF] Ranganath | Communication patterns for interconnecting and composing medical systems (extended version)[END_REF] that can serve as the schema to describe the communication needs of devices/apps. These communication patterns, based on asynchronous message-passing, facilitate development and forensic analysis of clinical scenarios. The use of message passing as the basic communication model is quite common in Internet of Things applications. While the individual components can be very different and operate independently, their interactions typically expose and deliver important emergent properties [START_REF] Hatcliff | Rationale and architecture principles for medical application platforms[END_REF].

These communication patterns consist of a set of components which are responsible to check a set of quality of service (QoS) properties locally. The combination of these quality of service properties should guarantee point-to-point communication requirements. These local QoS properties are parametrized by a set of thresholds on timing behavior of messages like the interval time between consequent messages, the lifetime of messages, etc. A medical system may use several instances of such patterns among its constituent devices and apps. Adjusting these parameters is non-trivial and depends not only to the architecture of the system but also the underlying network. Communication failures in medical systems may result in loss of life. For example, the X-ray machine should stop after two seconds, otherwise it causes harmful prolonged exposure. We can exploit formal methods to verify that the configuration of parameters results the pointto-point communication requirements of medical systems at design time. We use the actor-based formal modeling language of Rebeca [START_REF] Sirjani | Modeling and verification of reactive systems using Rebeca[END_REF][START_REF] Sirjani | Rebeca: Theory, applications, and tools[END_REF] to verify medical systems. Actor model is a computational model for event-based distributed systems in which actors communicate by asynchronous message-passing. The computation model of Rebeca helps to model the communication patterns with minimal effort and mistake. We exploit the timed extension of Rebeca to address local QoS properties defined in terms of the timing behavior of messages. Timed Rebeca [START_REF] Reynisson | Modelling and simulation of asynchronous real-time systems using timed rebeca[END_REF][START_REF] Sirjani | On time actors[END_REF] is supported by the Afra tool which efficiently verifies timed properties by model checking. Timed Rebeca supports inheritance among actors which facilitates modeling of communication patterns that their components communicate with the shared network entity.

In this paper we model and analyze communication patterns in Timed Rebeca using the implementation architecture proposed for the communication patterns [START_REF] Ranganath | Communication patterns for interconnecting and composing medical systems (extended version)[END_REF]. The components of patterns are modeled by distinct actors. Since the timing behavior network have effect on satisfying QoS properties of pattern, we also model network as a separate entity from actors. As the number of devices increases in a medical systems, the resulting semantic model may explode which prohibits application of the model checking technique. To tackle the problem, we propose a partial reduction technique for merging states such that the QoS properties of communication patterns are preserved. We prove the correctness of our reduction. We have implemented the reduction technique in a tool in Java which automatically reduces the semantic model generated by Afra. We illustrate the applicability of our reduction technique through a case study on a clinical scenario made of several instances of patterns. Our experimental result shows that our reduction technique can minimize the number of states almost to 30%.

Preliminaries

As we model communication patterns by Rebeca, first we provide an outline of patterns and then explain timed Rebeca.

Communication Patterns

Devices and apps involved in a communication pattern are known as components that communicate with each other via a communication substrate, e. g., networking system calls or a middleware. Each pattern is composed of a set of roles accomplished by components. We remark that a component may participate in several patterns with different roles simultaneously. Patterns are parametrized by a set of local QoS properties that their violation can lead to a failure. In addition, each pattern has a point-to-point QoS requirement that should be guaranteed by communication substrate. There are four communication patterns:

-Publisher-Subscriber: a publisher role broadcasts data about a topic and every devices/apps that need it can subscribe to data. Publisher does not wait for any acknowledge or response from subscribers. -Requester-Responder: a requester role requests data from a specific responder and waits for data from the responder. -Sender-Receiver: a sender role sends data to a specific receiver and waits until either data is accepted or rejected. -Initiator-Executor: an initiator role requests a specific executor to perform an action and waits for action completion or its failure.

As the communication patterns of Sender-Receiver and Initiator-Executor patterns resemble the Requester-Responder pattern, we only focus on Publisher-Subscriber and Requester-Responder patterns in this paper

Publisher-Subscriber

In this pattern, the component with the publisher role sends a publish message to those components that have subscribed previously. This pattern is parameterized with the following local QoS properties:

-MinimumSeparation (N pub ): if the interval between two consecutive publish messages from the publisher is less than N pub , then the second one is dropped by announcing a fast Publication failure. -MaximumLatency (L pub ): if the communication substrate fails to accept publish message within L pub time units, it informs the publisher of timeout. -MinimumRemainingLifeTime (R pub ): if the data arrive at the subscriber late, i.e., after R pub time units since publication, the subscriber is notified by a stale data failure. -MinimumSeparation (N sub ): if the interval between arrival of two consecutive messages at the subscriber is less than N sub , then the second one is dropped.

-MaximumSeparation (X sub ): if the interval between arrival of two consecutive messages at the subscriber is greater than X sub then the subscriber is notified by a slow publication failure. -MaximumLatency (L sub ): if the subscriber fails to consume a message within L sub time units, then it is notified by a slow consumption failure. -MinimumRemainingLifeTime (R sub ): if the remaining life time of the publish message is less than R sub , then the subscriber is notified by a stale data failure.

Each communication pattern owns a point-to-point QoS Requirement that should be guaranteed by the communication substrate. In this pattern the requirement is "the data to be delivered with lifetime of at least R sub , communication substrate should ensure maximum message delivery latency (Lm) does not exceed R pub -R sub -L pub ≥ L m ".

For example assume a pulse oximeter device which publishes pulse rate data of the patient. A patient monitor application can subscribe to this data to get the patients pulse rate. In other words, the application communicates with the device using the Publisher-Subscriber pattern.

Requester-Responder

In this pattern, the component with the role requester, sends a request message to the component with the role responder. The responder should replies within a time limit as specified by its local QoS properties. This pattern is parameterized with the following local QoS properties:

-MinimumSeparation (N req ): if interval between two consecutive request messages is less than N req , then the second one is dropped with a fast Request failure. -MaximumLatency (L req ): if the response message does not arrive within L req time units, then the request is ended by a timeout failure. -MinimumRemainingLifeTime (R req ): if the response message arrives at the requester with a remaining lifetime less than R req , then the requester is notified by a stale data failure. -MinimumSeparation (N res ): if the duration between the arrival of two consecutive request messages is less than N res , then the request is dropped while announcing a excess load failure. -MaximumLatency (L res ): if the response message is not provided within the L res time units, the request is ended by a timeout failure. -MinimumRemainingLifeTime (R res ): if the request message with the promised minimum remaining lifetime cannot be responded by the responder, then request is ended by a data unavailable failure.

The point-to-point QoS Requirement defined for this pattern concerns the delivery of response with lifetime of at least R req . So the communication substrate should ensure that "the sum of maximum latencies to deliver the request to the responder (L m ) and the resulting response to the requester (L m ) does not

exceed L req + R req -L res -R req ≥ L m + L m ".
For example assume a patient monitor application that communicates with a blood pressure (BP) monitor using the Requester-Responder pattern. The application requests blood pressure measurement from the BP which periodically measures the blood pressure of the patient.

Timed Rebeca and Actor Model

Actor model [START_REF] Agha | ACTORS -A Model of Concurrent Computation in Distributed Systems[END_REF][START_REF] Hewitt | Viewing control structures as patterns of passing messages[END_REF] is a concurrent model based on computational objects, called actors, that communicate asynchronously with each other. Actors are encapsulated modules with no shared variables. Each actor has a unique address and mailbox. Messages sent to an actor are stored in its mailbox. Each actor is defined through a set of message handlers to specify the actor behavior upon processing of each message.

Rebeca [START_REF] Sirjani | Modeling and verification of reactive systems using Rebeca[END_REF][START_REF] Sirjani | Rebeca: Theory, applications, and tools[END_REF] is an actor model language with a Java-like syntax which aims to bridge the gap between formal verification techniques and the real-world software engineering of concurrent and distributed applications. Rebeca is supported by a robust model checking tool, named Afra3 . Timed Rebeca is an extension of Rebeca for modeling and verification of concurrent and distributed systems with timing constraints. As all QoS properties in communication patterns are based on time, we use Timed Rebeca for modeling and formal analysis of patterns by Afra. Hereafter, we use Rebeca as short for Timed Rebeca in the paper.

The syntax of Timed Rebeca [START_REF] Reynisson | Modelling and simulation of asynchronous real-time systems using timed rebeca[END_REF][START_REF] Sirjani | On time actors[END_REF] is given in Figure 1. Each Rebeca model contains reactive classes definition and main part. Main part contains instances of reactive classes. These instances are actors that are called rebecs. Reactive classes have three parts: known rebecs, state variables and message servers. Each rebec can communicate with its known rebecs or itself. Local state of a rebec is indicated by its state variables and received messages which are in the rebec's mailbox. Rebecs are reactive, there is no explicit receive and the messages trigger the execution of the message servers when they are taken from the message mailbox. The timing features are computation time, message delivery time and message expiration. These three primitives are supported by the statements delay, after and deadline.

State-space of Rebeca models

The state-space of Rebeca models are generated as a state transition system to show the behavior in a formal way. The global states change due to the handling of messages by rebecs. Each rebec takes a message from its mailbox, modeled by a bag, and execute its message server, and hence, the value of state variables may update. Due to the encapsulation of rebec variables, intermediate values of each rebec during execution of message servers are not observable to other rebecs. Thus, semantics of Rebeca models are defined coarsely; each state transition shows the effect of handling of a message by a rebec. Floating Time Transition System (FTTS), a variation of state transition systems introduced in [START_REF] Khamespanah | Floating time transition system: More efficient analysis of timed actors[END_REF], gives a natural event-based semantics for timed actors, providing a significant amount of reduction in the state space. For efficient analysis of Rebeca models, different approaches are proposed for generating the semantic models [START_REF] Sirjani | Reactive actors: Isolation for efficient analysis of distributed systems[END_REF][START_REF] Jaghoori | Symmetry and partial order reduction techniques in model checking rebeca[END_REF][START_REF] Sirjani | Ten years of analyzing actors: Rebeca experience[END_REF]. FTTS uses isolation of actors, i.e., no coupling among the actors [START_REF] Sirjani | Reactive actors: Isolation for efficient analysis of distributed systems[END_REF]. The states of FTTS are defined by the local states of rebecs. The local states of rebecs are defined by the triple v, q, t , where v defines the value of state variables, q the message bag, and t the local time. In each state, different actors do not necessarily have the same local time and the time floats across the actors in the state space [START_REF] Khamespanah | Floating time transition system: More efficient analysis of timed actors[END_REF]. Note that at the level of Timed Rebeca models, actors have synchronized local clocks (as opposed to the semantic level) which gives the modeler a notion of global time.

Let ID denote the set of Rebeca identifiers, and S the set of global states. Each global state s ∈ S is a mapping from the Rebeca identifier to its local state. Assume Var , Value, and Msg be the set of variables, values, and messages, respectively. We use the notation bag(Msg) to represent the bag of messages and N to denote the local time of actors. So, the set of global states is defined by mapping each rebec identifier to its local state, S = ID → (Var → Value)×bag(Msg)×N. Each message m ∈ Msg constituted of three parts, namely m = (msgsig, arrival , deadline), where msgsig is the message content, arrival is the arrival time of the message, and deadline is the deadline of the message. We use msgsig(m), arrival (m), and deadline(m) to indicate the corresponding part. The message content constitutes of the name of message and its parameter values. We use Type(msgsig(m)) to show the name of the message content. Let statevars(s(x)), bag(s(x)), and now (s(x)) denote the state variable valuation, message bag, and the local time of the rebec with the identifier x ∈ ID. The reduction introduced by FTTS merges the states s and s that the local time of their rebecs has a fixed delay with each other, called shift equivalent.

Definition 1 (shift-equivalent). Two states s and s are called shift equivalent, denoted by s δ s , if for all the rebecs with identifier x ∈ ID there exists δ such that:

1. Condition on state variables: statevars(s(x)) = statevars(s (x)), 2. Condition on local time: now (s(x)) = now (s (x)) + δ, 3. Condition on bag content:

∀m ∈ bag(s(x)) ⇔ (msgsig(m), arrival (m) + δ, deadline(m) + δ) ∈ bag(s (x)).
Intuitively, the local time of rebecs in s has the fixed shift value δ with respect to the local time of rebecs in s. In other words, it can be considered s as a state occurred in future of s, but with the same behavior. We remark that the first and third conditions force the state variables of rebecs and the message contents (including message parameters) of corresponding rebecs in the two states be equivalent [START_REF] Khamespanah | Timed rebeca schedulability and deadlock freedom analysis using bounded floating time transition system[END_REF].

The bounded floating-time transition systems (BFTTS) S f , s 0 f , → of a rebeca model is achieved by merging those states of its FTTS S, s 0 , → that are shift equivalent. Formally speaking, if (s, m, s ) ∈ → in BFTTS as a consequence of processing the message m, then there exists s ∈ S such that (s, m, s ) ∈→ and s δ s for some δ. BFTTS preserve the timed properties of FTTS specified by weak modal µ-calculus where the actions are taking messages from the bag [START_REF] Khamespanah | Floating time transition system: More efficient analysis of timed actors[END_REF].

Modeling Patterns in Rebeca

We use the architecture proposed in [START_REF] Ranganath | Communication patterns for interconnecting and composing medical systems (extended version)[END_REF] for implementing communication patterns. We will explain the main components of publisher-subscriber pattern as the others are almost the same. This architecture specifies two interfaces between its constituent roles, e. g., publisher and subscriber, and the communication substrate. These interfaces encapsulate details of patterns from low-level details of various substrate layers. As illustrated in Figure 2, the client and service are devices/apps which aim to communicate with each other. The components Pub-lisherRequester and SubscriberInvoker are interfaces that check the local QoS properties related to the client or service side, respectively, and the communication substrate component is responsible for transmitting data.

We model each component of this architecture as a distinct actor or rebec in Rebeca. We explain the model of the Publisher-Subscriber pattern in detail. Other patterns are modeled with the same discussion. The parameters of Lm and life are updated in lines 12 and 13 regarding to clientDelay. This interface is responsible for checking N pub and L pub properties as specified in lines 15-23. To check N pub , the interval between two consecutive publish messages should be computed by subtracting the current local time of rebec from lastPub. The reserved word now represents the local time of the rebec. As this reserved word can not be used directly in expressions, we first assign it to the local variable time in line 14. If both properties are satisfied, it sends a transmitPublish message to the communication substrate and an accepted message to the client. These messages are delivered to their respective receivers with a non-deterministic delay, modeled by clientDelay, using the statement after . It means that the message is delivered to the client after passing this time. In case that the N pub property is violated, it sends a message fastPublicationFailure to the client. If the L pub property is violated, it sends a message timeOutFailure.

Communication substrate abstracts a network like Ethernet, wireless networks, Controller Area Network (CAN) bus [START_REF] Pfeiffer | Embedded Networking with CAN and CANopen[END_REF] by specifying the effects of the The SubscriberInvoker reactive class, given in Figure 5, is an interface between the communication substrate and the service (device/app). It has only one known rebec that is the destination for the messages of its instances. We define a state variable lastPub in line 5 to save the time of the last publication message that arrived in this rebec. This reactive class is responsible for checking N sub , X sub , R pub , R sub , and L pub properties (see Subsection 2.1). Message servers in this rebec are RcvPublish and consume. It checks N sub , X sub , R pub , and R sub properties in the message server RcvPublish. To model the communication de-lay between the interface and the service, we define the variable serviceDelay (in line 11) with non-deterministic values. It computes the interval between two consecutive RcvPublish messages in line 13 to inspect N sub in line 14 and X sub in line 16. It checks R sub and R pub properties using life and Lm parameters in line 19. Any violation of these properties will result in sending a failure message to the service or dropping the message. With satisfying the properties, it saves the local time of the actor in lastPub and sends a consume message to the service using after statement. The message server consumed checks L sub property in line 31 and sends a failure to the service.

State-space Reduction

A medical system is composed of several devices/apps that communicate with each other by using any of communication patterns. With the aim of verifying the QoS requirements of medical systems at the early stage of development, we use model checking technique by using Rebeca framework. As we explained in Section 3, each communication pattern is at least modeled by five rebecs. It is well-known that as the number of rebecs increases in a model, the state space grows exponentially. For a simple medical system composed of two devices that communicate with an app, there exist nine rebecs (as communication substrate in common) in the model. In a more complex system, adding more devices may result in state-space explosion, and model checking cannot be applied. We propose a partial reduction technique at the semantic level FTTS which merges those states with regard to the local QoS properties of communication patterns. In other words, such states not only satisfy the same local QoS properties but also preserve the same class of timed properties specified by weak modal µ-calculus where the actions are taking messages from the bag [START_REF] Khamespanah | Floating time transition system: More efficient analysis of timed actors[END_REF].

We relax those conditions of shift-equivalent relation that are applied on state variables and the message contents in the bags. We consider those state variables that are used for measuring the interval between two consecutive messages like lastPub. Such variables grow as the local time of rebecs proceeds. However, always now -lastPub are used to check local QoS properties like N sub , N pub , and X sub and the value of lastPub is not used anymore. Intuitively, two semantic states are shift-equivalent if their instances of PubliserRequester have the same value for all state variables except lastPub. As the behaviors of such instances depend on now -lastPub, the value of their lastPub variable can be shift-equivalent similar to their local time (see Section 2.3). This idea can be generalized for such variables (measuring interval) in other types of classes.

Assume two states with an instance of SubscriberInvoker. This instance has a RcvPublish message in its bag. The value of its life parameter is used by its message server to check the local QoS property R sub . This variable is not used anymore and hence, the value of this variable has no effect on the future behavior of the rebec. Intuitively, if the value of this parameter in the message in these assumed states leads to the same satisfaction of R sub , these messages can be considered equivalent.

Definition 2 (relaxed shift-equivalent). Two semantic states s and s , denoted by s ∼ δ s , are relaxed shift-equivalent if for all the rebecs with identifier x ∈ ID there exists δ such that:

1. Condition on state variables:

∀v ∈ Var \ {lastPub, lastReq} • statevars(s(x))(v) = statevars(s (x))(v), lastPub ∈ Dom(s(x)) ⇒ statevars(s(x))(lastPub) = statevars(s (x))(lastPub) + δ, lastReq ∈ Dom(s(x)) ⇒ statevars(s(x))(lastReq) = statevars(s (x))(lastReq) + δ.

Condition on local time: now

(s(x)) = now (s (x)) + δ.

Condition on bag content:

∀m ∈ bag(s(x)) ∧ Type(msgsig(m)) ∈ {RcvPublish, RcvResponse} ⇔ (msgsig(m), arrival (m) + δ, deadline(m) + δ) ∈ bag(s (x)), ∀(RcvPublish(Lm1, life 1 ), t, d) ∈ bag(s(x)) ⇔ (RcvPublish(Lm2, life 2 ), t + δ, d + δ) ∈ bag(s (x)) ∧ Lm1 = Lm2 ∧ (life 1 > R sub ⇔ life 2 > R sub ), ∀(RcvResponse(Lm1, life 1 ), t, d) ∈ bag(s(x)) ⇔ (RcvResponse(Lm2, life 2 ), t + δ, d + δ) ∈ bag(s (x)) ∧ (Lm1 = Lm2 ∧ life 1 > Rres ⇔ life 2 > Rres).
We merge states that are relaxed shift-equivalent. The following theorem shows that the FTTS modulo relaxed shift equivalency preserves the properties of the original one.

Theorem 1. For the given FTTS S, s 0 , → , assume the states s, s ∈ S such that s ∼ δ s . If (s, m, s * ) ∈→, then there exists s * * such that (s , m, s * * ) ∈→ and s * ∼ δ s * * .

Proof. Assume that (s, m, s * ) ∈→ by handling the message m by the rebec i. Regarding the third condition of Definition 2, there is also a message m such that Type(msgsig(m )) = Type(msgsig(m)) in the bag of Rebec i in the state s . Assume s * * is the resulting state as the consequence of handling m in the state s . We show that s * ∼ δ s * * . Regarding Type(msgsig(m)), three cases can be distinguished:

-Type(msgsig(m)) ∈ {RcvPublish, RcvResponse}: The message m handled by the rebec i is (msgsig(m), arrival (m) + δ, deadline(m) + δ) ∈ bag(s (x)). The assumption s ∼ δ s implies that all the variables except {lastPub, lastReq} have the same values while the value of variables {lastPub, lastReq} have δ-difference. We remark that all variables except {lastPub, lastReq} may be accessed/updated during execution of the message handler. So, all variables except {lastPub, lastReq} are updated by the message handler m and m similarly. As rebec i has only access to its own variables, the variables of other rebecs do not change. Thus the state s * * and s * satisfy the first condition. Furthermore, the local time of rebec i in the both states s * and s * * are progressed by the message handler m and m similarly and hence, their local timers have still δ-difference. So, the second condition is satisfied. The messages sent to other rebecs during handling m and m are sent at the same point. As their local timers have δ-difference, the arrival and deadline of sent messages have δ-difference. So, the third condition is also satisfied. -Type(msgsig(m)) = RcvPublish and m ≡ (RcvPublish(Lm 1 , life 1 ), t, d): By the third condition, the message m ≡ (RcvPublish(Lm 2 , life 2 ), t + δ, d + δ).

As Lm 1 = Lm 2 ∧ (life 1 > R sub ⇔ life 2 > R sub ) holds, the same statements, as shown in Figure 5, are executed by the rebec i during handling m and m . We remark that the value of interval is the same for both as statevars(s(x))(lastPub) = statevars(s (x))(lastPub) + δ. As no variable is updated, the states s * and s * * satisfy the first condition. As no delay statement is executed, still the second condition holds for s * and s * * . The messages sent by handling m and m are all parametrized by Lm 1 and Lm 2 which are equal. So, the third condition is also satisfied. -Type(msgsig(m)) = RcvResponse: This case is discussed in the same way of the previous case.

The relaxed shift equivalency preserves the conditions of shift equivalency on all variables except the variables defined for checking local QoS properties, i.e., {lastPub, lastReq}. Furthermore, it preserves the conditions of shift equivalency on all message content in the bag except for messages of type {RcvPublish, RcvResponse}. But the relaxed condition of the value of life ensures that the same statements will be executed. Therefore, by Theorem 1 FTTS modulo relaxed shift equivalency not only preserve the local QoS properties of the original one but also preserves the Timed properties defined on events (taking messages from the bag).

Case Study

Reduction technique is more applicable when using several patterns and devices in a medical system. For recovering a patient from an operation, he is controlled by a fixed dose of analgesia connected to an infusion pump. In addition, he is hooked up to a pulse oximeter to measure his pulse rate and oxygen saturation (SPO2) and to a capnometer to measure the concentration of carbon dioxide in his respiratory gases (end-tidal co2[ETCO2]) and respiratory rate. A monitoring application is composed of the pulse oximeter, capnometer, and infusion pump as shown in Figure 6 to control the activation of the infusion pump based on the measurements of the devices. If the application detects any deterioration in the patient's condition, it will deactivate the infusion pump and alert the nurses. Capnometer and oximeter publish data through the publisher-subscriber pattern, and monitoring application detects if data stray outside of the valid range and sends the appropriate command to pump infusion. There are two instances of the publisher-subscriber pattern and one of the requester-responder pattern in the resulting Timed Rebeca model of the application. To avoid modeling some components like communication substrate that is common in the patterns, we use the inheritance concept in Rebeca. We implement a base reactive class for the communication substrate of patterns as shown in Figure 7 named Base inspired by the approach of [START_REF] Yousefi | Verivanca: An actor-based framework for formal verification of warning message dissemination schemes in vanets[END_REF]. We define the state variable id in line 2 to uniquely identify rebecs. This class has a method named find to get the rebec with the given identifier. In this method we define an array of reactive classes and initiate it with all actors specified in the model (in line 4) then we get ids of all actors that are derived from the Base (in line 6) actor and search through them for finding the specified one (line 7).

The communication substrate reactive class extends Base class. As illustrated in Figure 8, this class has a parameter id in its constructor for assigning the id variable of the parent class (in line 2). This class has no known rebecs as opposed to the one specified at Figure 4. Instead, rebecs append their identifier to their messages during their communication with the substrate. The communication substrate uses the find method for finding the rebec that wants to send data based on their ids (lines 6 and 11). As the communication substrate class is commonly used by the components of publisher-subscriber and requester-responder patterns, it has two message handlers transmitPublish and transmitRequest to transmit their messages, respectively. In this paper, we formally modeled the four communication patterns proposed for interconnecting medical devices in Timed Rebeca modeling language and then analyzed the configuration of their parameters separately by Afra tool using the model checking technique. Since modeling many devices using several patterns resulted in state-space explosion, we proposed a reduction technique by extending FTTS merging technique with regard to the local QoS properties. We inspected a medical system which used three devices and one app communicating by two patterns and we applied our reduction technique on this system. We used inheritance concept in Rebeca for modeling this system in order to have a common communication substrate between patterns. Our results show that there are possible reductions regarding the behavior of message handlers.

Elaborating our approach on more case studies or non-trivial orchestration patterns of communication [START_REF] Ranganath | Communication patterns for interconnecting and composing medical systems (extended version)[END_REF] are among of our future work. We aim to generalize this approach by automatically deriving constraints on state variables like the one for lastPub or message contents to relax shift-equivalence relation in other domains. To this aim, we can use the techniques of static analysis.

Figure 1 .

 1 Figure 1. Abstract syntax of Timed Rebeca. Angle brackets denotes meta parenthesis, superscripts + and * respectively are used for repetition of one or more and repetition of zero or more times. Combination of with repetition is used for comma separated list. Brackets [ ] are used for optional syntax. IdentifiersC, T , m, v, c, e, and r respectively denote class, type, method name, variable, constant, expressions, and rebec name, respectively.

Figure 2 .

 2 Figure 2. Publisher-Subscriber Pattern Sequence Diagram

Figure 3 illustrates

 3 Figure3illustrates PublisherRequester reactive class, which is an interface between the client (device/app) and the communication substrate. As we see in lines 3 and 4, it has two known rebecs. The instances of this reactive class can send messages to them. We define the state variable lastPub in line 5 for saving the time of last publication message. We use this time for computing the interval between two consecutive messages. This rebec has a message server named publish. We pass Lm and life parameters through all message servers in the model to compute the delivery time and remaining lifetime of each message. To model the communication delay between the interface and the communication substrate, we define the variable clientDelay (in line 11) with non-deterministic values. The parameters of Lm and life are updated in lines 12 and 13 regarding to clientDelay. This interface is responsible for checking N pub and L pub properties as specified in lines 15-23. To check N pub , the interval between two consecutive publish messages should be computed by subtracting the current local time of rebec from lastPub. The reserved word now represents the local time of the rebec. As this reserved word can not be used directly in expressions, we first assign it to the local variable time in line 14. If both properties are satisfied, it sends a transmitPublish message to the communication substrate and an accepted message to the client. These messages are delivered to their respective receivers with a non-deterministic delay, modeled by clientDelay, using the statement after . It means that the message is delivered to the client after passing this time. In case that the N pub property is violated, it sends a message fastPublicationFailure to the client. If the L pub property is violated, it sends a message timeOutFailure.Communication substrate abstracts a network like Ethernet, wireless networks, Controller Area Network (CAN) bus[START_REF] Pfeiffer | Embedded Networking with CAN and CANopen[END_REF] by specifying the effects of the

Figure 6 .

 6 Figure 6. Communication between entities in the clinical scenario.

  Modeling Publisher Interface in Timed Rebeca network on transmitting messages. To this aim, it may consider priorities among received messages to transmit or assign specific or non-deterministic latency for sending messages. A specification of communication substrate reactive class is shown in Figure4. It handles transmitPublish messages by sending a RcvPublish message to its known rebec, a rebec of SubscriberInvoker class in line 11. It considers a non-deterministic communication delay for each message, modeled by the local variable netDelay in line 8. We remark that this rebec updates the parameters Lm and lifetime based on netDelay before sending RcvPublish in lines 9 and 10.

	1 reactiveclass	13	life = life -clientDelay ;
		PublisherRequester (20) {	14	int time = now ;
	2 knownrebecs {	15	if ( time -lastPub < NPUB ) {
	3 Co mm un ica ti on Sub st ra te cs ;	16	c . fa st Pub li ca tio nF ai lu re ()
	4 Client c ;}		;}
	5 statevars { int lastPub ;}	17	if ( clientDelay > LPUB ) {
	6		18	c . timeOutFailure () ;}
	7 PublishRequester () {	19	else {
	8	lastPub = 0;}	20	lastPub = now ;
	9		21	cs . transmitPublish ( Lm , life )
	10 msgsrv publish ( int Lm , int		after ( clientDelay ) ;
		life ) {	22	c . accepted () after (
	11	int clientDelay =?(1 ,2) ;		clientDelay ) ;
	12	Lm = Lm + clientDelay ;	23 }}}
	Figure 3. 1 reactiveclass	7	msgsrv transmitPublish ( int
	2	Co mm un ica ti on Sub st ra te (20)		Lm , int life ) {
	3 {		8	int netDelay =?(1 ,2) ;
	4	knownrebecs {	9	Lm = Lm + netDelay ;
		SubscriberInvoker si ;}	10	life = life -netDelay ;
	5	statevars {}	11	si . RcvPublish ( Lm , life )
	6	Co mm un ica ti on Sub st ra te () {}		after ( netDelay ) ;}}
		Figure 4. Modeling Communication Substrate in Timed Rebeca

  1 reactiveclass Co mm uni ca ti on Sub st ra te extends Base (20) { 2 Co mm un ica ti on Sub st ra te ( int _id ) { id = _id ;} 3 msgsrv trasmitPublish ( boolean data , int topic , int Lm , Figure 8. Modeling Communication Substrate using Inheritance in Rebeca 6 Conclusion and Future Work

	4	int life , int subscriberId ) {
	5	int csDelay = ?(1 , 2) ;
	6	SubscribeInvoker si =( SubscribeInvoker ) find ( subscriberId
		) ;
	7	si . publish ( data , topic , Lm + csDelay , life -csDelay )
	8	after ( csDelay ) ;}
	9	msgsrv transmitRequest ( boolean data , int Lm , int
		responderInvokerId ) {
	10	int cs1Delay = ?(1 , 2) ;
	11	ResponderInvoker ri =( ResponderInvoker ) find (
		responderInvokerId ) ;
	12	ri . request ( data , Lm + cs1Delay ) after ( cs1Delay ) ;}
	13	msgsrv transmitResponse ( boolean data , int Lm , int life ,
		int requesterId ) {
	14	int cs2Delay = ?(1 , 2) ;
	15	RequestRequester rr = ( RequestRequester ) find (
		requesterId ) ;
	16	rr . response ( data , ( Lm + cs2Delay ) , ( life -cs2Delay ) )
		after ( cs2Delay ) ;
	17	}
	18	...
	19 }

http://www.rebeca-lang.org/alltools/Afra

The Rebeca models and the Java code for the reduction of semantic models are available at fghassemi.adhoc.ir/shared/MedicalCodes.zip

Acknowledgment

We would like to thank Ehsan Khamespanh for his kind supports in resolving the problems in using Afra tool. The research of the third author is partially supported by the KKS Synergy project, SACSys, the SSF project Serendipity, and the KKS Profile project DPAC.

All interfaces that communicate through communication substrate should extend the Base class. As two devices (capnometer and oximeter) send data by using the publisher-subscriber pattern, we define two instances of PublisherRequester and SubscriberInvoker interfaces in main, as shown in Figure 9. The instance of CommunicationSubstrate, called cs, is used by all the components which send message to Communication Substrate in the patterns.

Experiment Results

We applied our reduction technique on the three cases we have modeled in Timed Rebeca. We developed a code in Java which automatically reduces the resulting FTTSs of these models generated by Afra 4 . We got 23% and 32% reduction in the model of requester-responder and publisher-subscriber patterns, respectively. In the clinical scenario which is a medical system using several patterns as explained in Section 5 we have 29% reduction in the state space.


Agustín E Martinez Suñé

Carlos G Lopez Pombo

Quality of Service ranking by quantifying partial compliance of requirements

While there is not much discussion on the importance of formally describing and analysing quantitative requirements in the process of software construction; in the paradigm of API-based software systems it could be vital. Quantitative attributes can be thought as attributes determining the Quality of Service -QoS provided by a software component published as a service. In this sense, they play a determinant role in classifying software artifacts according to specific needs stated as requirements. In previous works we presented an efficient, and fully automatic, analysis technique for establishing Service Level Agreements -SLA. Such a proposal relays on describing QoS contracts as convex specifications, and compliance checking is performed by the application of an analysis algorithm based on state of the art techniques used in hybrid system verification. Such a technique succeeds in offering a procedure for determining SLA but fails in the more realistic scenario where, potentially, no service fully satisfies the requirements. In this scenario the running application may still prefer to invoke the service that offers the best chances of successfully executing with values for QoS attributes meeting the requirements satisfactorily.

In this work we propose and implement a metric for automatically quantifying partial satisfaction of QoS requirements, leading to a way of ranking services according to such notion of partial compliance.

Introduction

Distributed software resulting from paradigms such as Service-Oriented Computing (SOC) or the API's economy is based on the idea of constructing software artifacts by composing services provided by third parties and registered in repositories. This envisages a generation of applications which, at run-time, are transparently reconfigured by the intervention of a dedicated middleware with the capability to bind a running application that has certain requirements to a service capable of fulfilling them, subject to the negotiation of a Service Level Agreement -SLA; in this way, services can collectively fulfill certain business goals [START_REF] Fiadeiro | An abstract model of service discovery and binding[END_REF].

Requirements can be formalised as contracts between software components, and satisfaction of such contracts is usually dealt with by checking whether a judgment of the form Pr Rq holds or not, where Pr is the provision contract and Rq is the requirements contract. In the literature, functional requirements have been identified as those describing what the system has to do, while non-functional ones are assumed to characterise how the system develops the behaviour described by the functional ones.

In this work we focus on Quantitative requirements as a proper subclass of non-functional requirements of a software system. From our perspective, quantitative requirements formalise the admissible values of specific attributes that can be interpreted over a metric space [START_REF] Bryant | Metric spaces: iteration and application[END_REF]. Such attributes are referred to as Quantitative attributes. For practical reasons, the real numbers constitute a good candidate over which these can be interpreted, formalised and analysed.

In this sense, quantitative requirements might be used to characterise the Quality of Service -QoS provided by a software component available as service. While services may have the same functional behaviour, they might differ on their non-functional one (for example, a service may offer low-speed computation at a very low cost while another, functionally equivalent one, might be faster but more onerous); a motivation shared with other works like [START_REF] Strunk | QoS-aware service composition: A survey[END_REF]. Therefore, quantitative requirements might be considered as a way to classify functionally equivalent services by their QoS.

In [START_REF] Martinez Suñé | Automatic quality-of-service evaluation in service-oriented computing[END_REF] we presented an efficient, and fully automatic, analysis procedure for checking a judgment of the shape Pr Rq where Pr is the provision contract and Rq is the requirements contract, thus serving the purpose of establishing SLA. Such an approach guarantees the selection of a service satisfying the requirements of the executing application but it does not provide any insight when there is no service whose provision contract is fully compliant with the requirement contract. A geometrical interpretation of the judgment Pr Rq expresses that all the satisfying values of real attributes of Pr also satisfy Rq. Thus, a negative answer just means that there is at least one value satisfying Pr and not satisfying Rq pushing the application to abort its execution because there is no possible SLA on the required QoS.

In this paper we propose an automatic procedure3 for evaluating partial compliance of QoS contracts by estimating what we call the inclusion ratio: the intersection of the set of satisfying values of the provision and requirement contracts interpreted relative to the size of the set of values satisfying the provision contract. This metric leads to a natural way of ranking services. While the problem of raking services according to their QoS has been studied and different approaches to tackle the problem have been proposed, in general, these are based on monitoring run-time behavior of specific attributes [START_REF] Liu | Qos computation and policing in dynamic web service selection[END_REF][START_REF] Al-Masri | QoS-based discovery and ranking of web services[END_REF] or by socially sharing the users' opinion [START_REF] Zheng | Qos ranking prediction for cloud services[END_REF][START_REF] Mao | Search-based qos ranking prediction for web services in cloud environments[END_REF] but, to the best of our knowledge, there is none focussing on QoS ranking where the QoS is formally specified and SLA is guaranteed through an automated procedure.

Formalisation and analysis of quantitative attributes

The selection of a service requires establishing an SLA, part of which is the QoS agreement. Given a formal QoS requirement contract Rq; a service that declares a formal QoS provision contract Pr will be a good candidate only if Pr =⇒ Rq holds. In [START_REF] Martinez Suñé | Automatic quality-of-service evaluation in service-oriented computing[END_REF] we adopted monotone Satisfiability Modulo Convex (SMC) formulae [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF] as specification language and proposed a method to check QoS compliance. SMC formulae are defined as quantifier-free formulae in conjunctive normal form, with atomic propositions ranging over a subset of the propositional variables and convex constraints 4 . Then, given two SMC formulas Pr and Rq, the proposed method to check whether Pr Rq holds or not is done by determining if the formula Pr ∧ ¬Rq is not satisfiable. Such a procedure does not provide any hint on what to do when no service registered in the repository fully satisfies the requirements. That is, no QoS provision contract satisfies the QoS requirements contract.

A different way of formalising QoS contracts is as a set of real values satisfying the specification. Next we present this alternative formalisation of quantitative non-functional requirements. Throughout the rest of the paper, letters I, J and K will be used to denote index sets. Definition 1. Let X be a set of real variables. We define a QoS specification on quantitative attributes X to be X , α , with α being a formula with shape i∈I P i .

Each P i is a convex polytope expressed as k∈Ki f i,k ( → x ) R 0, where R ∈ {<, ≤} such that each f i,k ( → x ) R 0 is a convex constraint.
The set of QoS specifications over the set of quantitative attributes X will be referred to as QoS spec(X ).

Let X , α ∈ QoS spec(X ). We define a valuation for α as v :

X → R. Satisfaction is a relation |=⊆ [X → R] × QoS spec(X ) defined as → x |= α if and only if there exists i ∈ I, such that for all k ∈ K i , f i,k ( → x ) R 0. The set of values satisfying α is defined as [[α]] = → x | → x |= α .
Essentially, the set of admissible values of the quantitative attributes X in a QoS spec is characterised by a set of convex polytopes over X . Notice that, under some reasonable assumptions, SMC formulae can be translated to specifications in QoS spec(X ) by simply iterating the satisfying valuations of the boolean abstraction of the formulae, and collecting the polytopes determined by the positive literals.

A specification like this can capture many quantitative aspects of a software system. For example, the formulae below show a specification of an APIbased software application requiring a service to be paid exclusively for the time it is used. Consider as relevant quantitative attributes a) perSec: the cost per second of the session, and b) maxWait: the maximum waiting time. Then, such attributes can be formalised by a QoS specification X , α where X = {perSec, maxWait}. To characterise a service that is more expensive when it is faster a possible α would be the disjunction of the following formulae:

0 < maxWait ≤ 100 ∧ 0.1 ≤ perSec < 0.3, 100 < maxWait ≤ 1000 ∧ 0.0 ≤ perSec ≤ 0.1
A geometrical interpretation of the formula Pr =⇒ Rq leads to the possibility of measuring different degrees of partial compliance, which range between total compliance (all values allowed by Pr are accepted by Rq) and no compliance at all (no value allowed by Pr is accepted by Rq).

Based on the previous definitions, proving the formula Pr Rq is to check whether

[[Pr ]] ⊆ [[Rq]].

We propose to compute the volume of the intersection between [[Pr ]] and [[Rq]] relative to the volume of [[Pr ]], referred to as inclusion ratio.

This indicator quantifies what is the percentage of the QoS values allowed by the provision contract that is actually accepted by the requirements contract. For us, this indicator serves the purpose of quantifying the partial compliance of Rq by Pr ; therefore, functionally compliant services can be chosen from a ranking built by using inclusion ratio as the ordering criterion.

On the complexity of the volume computation

In the literature, the volume of a polytope is invariably defined in terms of the sum of the volumes of a certain decomposition of such polytope into a family of convex ones [START_REF] Gritzmann | On the complexity of some basic problems in computational convexity: Ii. volume and mixed volumes[END_REF]. Fortunately, Def. 1 assists us by already expressing the set of values in a QoS contract as the union of the sets of values of each member of a family of convex polytopes, expressed as Pr = i∈I P i and Rq = j∈J R j . As neither family is guaranteed to be a partition, volumes must be computed following the Principle of inclusion-exclusion [START_REF] Liu | Introduction to Combinatorial Mathematics[END_REF]Chap. 4]. Then, the inclusion ratio is calculated as follows: First: Compute the volume (denoted as #) of intersection between Pr and Rq:

#   i∈I [[Pi]] ∩ j∈J [[Rj ]]   = ∅ =K⊆I×J (-1) |K|-1 #   (i,j)∈K ([[Pi]] ∩ [[Rj ]])   (1)
Second: Compute the volume of P :

#   i∈I [[Pi]]   = ∅ =K⊆I (-1) |K|-1 #   k∈K [[P k ]]   (2)
Third: Compute the inclusion ratio of Pr in Rq as:

#([[Pr ]]∩[[Rq]]) #([[Pr ]])
.

In the late 80's Dyer et. al. [START_REF] Dyer | On the complexity of computing the volume of a polyhedron[END_REF] and Khachiyan [START_REF] Khachiyan | The problem of calculating the volume of a polyhedron is enumerably hard[END_REF] proved the complexity of computing the volume of a convex polytope to be #P-Hard. The first estimation algorithm was presented by Kannan et. al. in [START_REF] Kannan | Random walks and an o * (n 5 ) volume algorithm for convex bodies[END_REF]. Later in [START_REF] Ge | A fast and practical method to estimate volumes of convex polytopes[END_REF], an estimation algorithm based on the Multiphase Monte-Carlo algorithm is proposed and the authors show that it can efficiently handle instances of dozens of dimensions with high accuracy. The complexity is shown to be O * (m • n 3 ), where n is the dimensions, m is the number of constraints, and the Soft-O notation (O * ) omits logarithmic factors. The estimation method tool is distributed under the name PolyVest.

The implementation of the algorithm presented above for computing the inclusion ratio requires 2 |I|•|J | + 2 |I| invocations to the function computing the volume of a convex polytope. Such complexity forces us to consider a further dimension of approximation in order to make the calculation of the inclusion ratio viable in practice. In the next section we study the appropriateness of considering only some of the intersections involved in the calculation as an estimation of the volume.

Experimental results

Our first research question is related to the complexity of the exact computation of the volume of a polytope P. For the sake of understanding the limits imposed by such complexity, the research question will be stated in terms of a single polytope decomposed as a family of convex polytopes.

RQ1: How does the complexity of # i∈I P i impacts in practice?

From our experiments5 it is possible to identify the exponential nature of the computation and that the majority of cases could not be completed within the time budget, hence the method cannot be applied to more realistic casestudies. The applicability of the technique, therefore, rests on the possibility of computing a good and efficient approximation of the volume operator. A natural way of doing this is by considering only a limited number of terms of the sum in Eq. 2.1. The next proposition formalises the intuition that subsequent partial sums represent an upper, and a lower, bound for the exact value of the volume.

Proposition 1. Let P = {P i } i∈I and 0 < n < |I|, with n ≡ 0 (mod 2) then

∅ = K ⊆ I 0 < |K| ≤ n (-1) |K|-1 #   k∈K [[P k ]]   ≤ #(P ) ≤ ∅ = K ⊆ I 0 < |K| ≤ n + 1 (-1) |K|-1 #   k∈K [[P k ]]   .
Computing an approximation of a magnitude requires the introduction of a metric for measuring the effectiveness of such estimation. As usual, the relative error between the magnitude x and an approximate value x 0 is defined to be |x0-x| |x| . The next proposition provides upper bounds for the relative error that do not depend on the exact value v of the volume but on two consecutive approximations:

{v k-1 , v k } or {v k , v k+1 }. Proposition 2. Let v, v k-1 , v k , v k+1 ∈ R, then: -if 0 < v k-1 < v < v k , then v k -v v ≤ v k -v k-1 v k-1 (denoted ρ k ), -if v k > v > v k+1 > 0, then v k -v v ≤ v k -v k+1 v k+1 (denoted σ k ) -if v k-1 ≥ v k+1 > 0, then ρ k ≥ σ k .
Using these bounds, and considering Prop. 1, we can design an algorithm for computing the approximate volume of a polytope, by computing successive approximations until the desired value for the relative error is guaranteed. Notice that if we require a relative error equal to 0, the complexity of the algorithm is still O(2 n ), but when the bound is big enough to let the algorithm converge in the second approximation, the complexity drops to O(n 2 ). Our second research question analises the practical impact of approximating the volume of a polytope using these bounds.

RQ2: How do the partial sums of the terms in the sum of Eq. 2.1 converge to the value # i∈I P i with 1% and 5% tolerance?

Results 6 show that the number of succesive approximations needed for a calculation with an error within 1% tolerance is between 2 and 5, while for an error within 5% tolerance is between 2 and 3. In both scenarios the estimated computation greatly outperformed the exact one, being able to compute the mayority of cases within the time budget.

A natural follow-up from these results is to explore the scalability of the procedure for volume estimation. Table 1 show the maximum size of the family of polytopes whose approximate volume can be computed in one hour, considering relative errors with bounds set to 1% and 5%. Size denotes the number of polytopes in the family and App the number of succesive approximations needed in each case. As we mentioned in Sec. 2, efficiently computing the volume of these types of polytopes is just a means for quantifying partial compliance of QoS contracts. RQ3: how does the performance gain obtained by approximating the volume impacts the computation of the inclusion ratio?

Our results 7 show that as the size of the contracts increases the efficiency gain between 0%, 1% and 5% tolerance is dramatically better. There are cases where the approximate volume computation is performed in 4% of the time required by the exact volume computation, and several cases for which the exact inclusion ratio fails to be computed within the 10 hours time budget but becomes feasible when a bound for the relative error is introduced.

Inclusion ratio provides a way of ranking services according to partial satisfaction. Thus, it is worth knowing how an approximate computation of the volume propagates the relative error to the computation of the inclusion ratio. In the end, this will impact the actual selection of a service candidate. The next proposition establishes lower and upper bounds for the distance between approximate inclusion ratio and exact inclusion ratio.

1. (1 -e) • v ≤ v k ≤ (1 + e) • v (respectively (1 -e) • w ≤ w k ≤ (1 + e) • w), and 2. (1-e)•v (1+e)•w ≤ v k w k ≤ (1+e)•v (1-e)•w (equivalently 1-e 1+e • v w ≤ v k w k ≤ 1+e 1-e • v w ).
Consider, as an example, the bounds obtained from Prop. 3 for the approximate inclusion ratio, when approximate volumes are computed with relative error bound to be smaller than 5% and 1%, as we did in the previous experiments. Let eir be the exact inclusion ratio, ir 5 the inclusion ratio computed with a relative error below 5% and ir 1 the inclusion ratio computed with a relative error below 1%; then, we obtain that 0.905 • eir ≈ 0.95 1.05 • eir ≤ ir 5 ≤ 1.05 0.95 • eir ≈ 1.105 • eir and 0.98 • eir ≈ 0.99 1.01 • eir ≤ ir 1 ≤ 1.01 0.99 • eir ≈ 1.02 • eir , respectively. Our final research question focuses on effectively ranking different provision contracts using the inclusion ratio as a metric for quantifying partial satisfaction. RQ4: What is the impact of the proposed approximation in the construction of a ranking of a set of services?

For this experiment we performed 3 examples of ranking 20 provision contracts by partial satisfaction of a single requirements contract. The datasets were synthetically generated following the guidelines used for generating the case-studies used in RQ3. Each ranking correspond to a different size of the families of polytopes as follows: a

) |Pr | = 2, |Rq| = 4, b) |Pr | = 3, |Rq| = 3, c) |Pr | = 4, |Rq| = 2 .
For each dataset we performed the ranking order using the exact inclusion ratio, and also using 1% and 5% bounds for the relative error. The results of the experiment show that in all of the examples the ranking obtained by using the exact volume computation is preserved when resorting to approximate volume computations.

We extended previous work where we proposed a formalisation of QoS contract as convex specifications [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF]. Under a geometrical interpretation, a contract can be seen as a family of convex polytopes characterising the admissible values for the quantitative attributes and a judgement of the shape Pr Rq as polytope inclusion. From this perspective, we proposed a way of QoS ranking services by quantifying the volume of the intersection between [[Pr ]] and [[Rq]], under the name inclusion ratio. Since this indicator quantifies the percentage of values allowed by the provision contract that are actually accepted by the requirement contract we sustain that it serves the purpose of quantifying partial compliance. The exponential nature of computing the volume of a family of convex polytopes forced us to propose a volume approximation technique based on imposing an upper bound to the relative error.

We evaluated the performance of the approximated volume computation against the exact volume computation, the scalability of the approximate volume computation and the performance of computing the inclusion ratio with respect to the exact computation. Finally, we showed examples of the impact of approximate inclusion ratio in ranking services by comparing the ideal ranking, obtained by resorting to the exact inclusion ratio, and the one obtained by resorting to approximate inclusion ratio, for different bounds to the relative error.

This technique for evaluating partial satisfaction of QoS contracts triggers what we believe is one of the most important questions regarding the automation of service broking. Under partial satisfaction of QoS contracts, we would like to establish preferences among different quantitative attributes of the different candidates. For example, if we consider two services with the same inclusion ratio, a low budget application would like to express it's preference for cheaper services, even at the cost of degraded performance, over a more expensive and efficient one. This problem will be addressed in the near future aiming at a more realistic view of an automatic procedure for checking QoS compliance for determining SLA in a service-based architecture.

Proposition 3 .

 3 Given two volume approximations v k , w k , where the exact volumes are v, k, respectively. Let e be the bound for the relative error (i. e., |v-v k | |v| ≤ e and |w-w k | |w| ≤ e) then:

Table 1 :

 1 Upper limit for computation of approximated volume.

		Number of quantitative attributes
	10			15	20
	Size App.	Time Size App.	Time Size App.	Time
	1% 11 4.95 1452.42		15	3 3067.82 22	2 3320.67
	5% 15 3.72 1857.42 24.92	2 1218.55 22	2 3320.67
		Number of quantitative attributes
		25		30
	Size App.	Time Size App.	Time
	1% 14	2 3481.29	9	2 3120.49
	5% 14	2 3481.29	9	2 3120.49

A demonstration video of the tool can be found on http://bit.do/QoS-Rank

Synthetic case-studies were generated automatically consisting of families of 5 -11 convex polytopes over 10 -35 quantitative attributes. For each case the procedure was run over 20 different instances, with a 1 hour time budget.

The experiment was conducted over the same dataset as for RQ1.

Case studies were generated following the same guidelines as for RQ2. A time budget of 10 hours is considered.

Research partly supported by the European Unions Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 778233. Carlos G. Lopez Pombo's research is supported by Universidad de Buenos Aires through grant UBACyT 20020170100544BA, and Consejo Nacional de Investigaciones Científicas y Técnicas through grant PIP 11220130100148CO.


Xiyue Zhang
email: zhangxiyue@pku.edu.cn

Yi Li

Meng Sun
email: sunm@pku.edu.cn

Towards a Formally Verified EVM in Production Environment

Keywords: EVM, Why3, Verification, Testing

Among dozens of decentralized computing platforms, Ethereum attracts widespread attention for its native support of smart contracts by means of a virtual machine called Ethereum Virtual Machine (EVM). Programs can be developed in various front-end languages. For example, Solidity can be deployed to the blockchain in the form of compiled EVM opcodes. However, such flexibility leads to critical safety challenges. In this paper, we formally define the behavior of EVM in Why3, a platform for deductive program verification, which facilitates the verification of different properties. The extracted implementation in OCaml can be directly integrated into the production environment and tested against the standard test suite. The combination of proofs and testing in our framework serves as a powerful analysis basis for EVM and smart contracts.

Introduction

Ever since the inception of the Bitcoin blockchain system [START_REF] Nakamoto | Bitcoin: A peer-to-peer electronic cash system[END_REF], cryptocurrencies have become a well-known global revolutionary phenomenon. Meanwhile, the decentralized blockchain system with no server or central authority, which emerges as a side product of Bitcoin and provides a continuously growing ledger of transactions being represented as a chained list of blocks distributed and maintained over a peer-to-peer network [START_REF] Zheng | Blockchain challenges and opportunities: a survey[END_REF], shows great potential in carrying out secure online transactions. From then on, there have been a lot of changes and growth on the blockchain technology. Ethereum [5] extends Bitcoin's design, which can process not only transactions but also complex programs and smart contracts. Smart contracts running on the blockchain make it possible to use blockchain techniques in many other application domains besides cryptocurrencies, and have attracted a lot of attention from government, finance, health, entertainment and industry. This feature makes Ethereum a popular ecosystem for building blockchain-applications, which gains much more interest to innovate the options to utilize blockchain.

Smart contracts are often written in a Turing-complete programming language called Solidity [START_REF]Solidity Documentation[END_REF] and then compiled into EVM bytecode, which can be mapped into a list of machine instructions (opcodes). EVM is a quasi-Turing complete machine. It provides a runtime environment for smart contracts to be executed. Given a sequence of bytecode instructions, which are compiled from smart contracts by an EVM compiler, and the environment data, this execution model specifies how the blockchain transits from one state to another.

However, EVM and smart contracts are faced with several security vulnerabilities. A taxonomy of vulnerabilities and related attacks against Solidity, the EVM, and the blockchain is presented in [START_REF] Atzei | A survey of attacks on ethereum smart contracts[END_REF]. To deal with the security challenges against EVM, we propose a formal framework of generating verified EVM for production environment in this paper. The contributions of this work are:

-A formal definition of EVM specified in WhyML, the programming and specification language used in Why3 [START_REF] Filliâtre | Why3-where programs meet provers[END_REF]. -An implementation of EVM in OCaml generated through an extraction mechanism based on a series of customized drivers. -The verification of sample properties and testing of the OCaml implementation for EVM against a standard test suite for Ethereum.

This paper is organized as follows: We outline the framework for formalizing, property verifying and testing of EVM in Section 2. Section 3 presents some related work. Finally, we summarize this paper in Section 4.

The Framework of Generating Verified EVM for Production Environment

In this section, we present the framework of generating verified EVM for production environment in detail. The framework is as shown in Fig. 1 and the main idea is to combine verification and testing techniques towards developing more secure EVM implementations. It also provides a platform to verify the functionality properties of smart contracts. This framework is mainly comprised of two parts: (1) EVM specification and property verification in Why3; (2) experimental testing based on OCaml extraction and Rust connection. This approach leverages formal methods and engineering approaches, allowing us to perform both rigorous verification and efficient testing for EVM implementations and smart contracts.

EVM in Why3

The first phase of the framework is to define a formal specification of EVM in Why3 and provide a platform for rigorous verification. We develop the EVM specification, following the Ethereum project yellow paper [START_REF] Wood | Ethereum: A secure decentralised generalised transaction ledger[END_REF]. More specifically, the EVM implementation is translated into WhyML, the programming and specification language of Why3. Verification conditions can be further generated based on the pre-and post-condition specification. Generated verification goals are solved directly through the supported solvers or go through a sequence of transformations first. In cases when the automatic SMT solvers cannot deal with, users can resort to interactive theorem provers for the remaining unsolved proof goals. EVM is essentially a stack-based machine. The memory model of EVM is a word-addressed byte array and the storage model is a word-addressed word array. These three components form the infrastructure of EVM. Based on the formalization of the infrastructure, the most important aspect in this framework is to capture the execution result of the EVM instructions. The perspective from which we deal with the execution process of a sequence of opcodes (instructions) is as a state transition process. This process starts with an initial state and leads to a series of changes in the stack, memory etc. The formalization of base infrastructure and the instruction set are specified through Type Definition and Instruction Definition, respectively. The main function Interpreter provides the specification of transition results for the instructions.

Type Definition To formalize the infrastructure of EVM, we need to first provide the formalization of commonly-used types in EVM, such as the types of machine words and the addresses in the EVM. Hence, we developed a series of type modules such as UInt256 and UInt160 to ease the representation of corresponding types in EVM. Type alias supported by Why3 are also used to make the basic formalization more readable and consistent with the original definition.

To this end, the components of the base infrastructure can be specified. Stack is defined as a list of elements whose type is uint256, aliased by machine word. Memory is defined as a function that maps machine word to an option type option memory_content. Similarly, storage is defined as a function that maps machine word to machine word. To reflect the implicit change of the machine state, we defined more miscellaneous types. For example, we use vmstatus, error and return_type to capture the virtual machine status, the operation error, and the view of the returned result. Furthermore, the record type machine_state is defined to represent the overall machine state which consists of stack, memory, storage, program counter, vmstatus, the instruction list, etc.

Instruction Definition

The infrastructure has been built above to specify the state of the virtual machine. Inspired by the instruction formalization in Lem [START_REF] Hirai | Defining the ethereum virtual machine for interactive theorem provers[END_REF], the instruction set is defined in multiple groups, such as arithmetic operations and stack operations, then these groups are integrated into a summarized type definition instruction. Different subsets of instructions are wrapped up to form the complete specification in the definition of instruction.

The organization of the instruction category is a bit different from the yellow paper [START_REF] Wood | Ethereum: A secure decentralised generalised transaction ledger[END_REF]. The information related instructions including environmental and block information are defined in type info_inst, except CALL and CODE instructions, such as CALLDATACOPY, CODECOPY and CALLDATALOAD. These instructions are more closely related to memory and stack status. Therefore, they are added to the memory and stack instruction groups. In case when some illegal command occurs, the instruction Invalid is included in the instruction definition. The specification of the remaining instruction groups are basically the same as the corresponding instruction subsets in [START_REF] Wood | Ethereum: A secure decentralised generalised transaction ledger[END_REF].

Interpreter Definition The specification of interpreter formalizes the state transition result of different instructions. For a specific instruction, the interpreter determines the result machine state developing from the current state. Some auxiliary functions are defined to make the definition of the interpreter more concise and compact. In the above code snippet, get_inst is used to obtain the next instruction to be executed. It is obtained from the instruction list following the program counter. In the case of Arith ADD instrcution, the numbers to perform the add operation on are popped out of the stack first and the result is pushed into the stack after the calculation. As a result, the stack state is updated as a component of the machine state. In this process, functions push_stack and pop_stack are defined to control the push and pop manipulations for the state transition of stack. With the support of pre-defined auxiliary functions, the definition of the interpreter function is essentially comprised of machine state update with regard to the instructions.

Running EVM in Production Environment

Fig. 2 shows the second phase of the framework: deploy the extracted OCaml implementation from Why3 in production environments. The deployment is essentially based on a co-compilation framework between OCaml and Rust.

OCaml is a functional programming language that shares a highly identical language definition and formal semantics with Why3. Through the official OCaml code generator equipped with Why3, we extract the verified specification of EVM into an executable OCaml module. A JSON-based protocol is developed as a bridge between the OCaml implementation and the EVM host in Rust.

Rust is a multi-paradigm system programming language which is designed to provide better memory safety while maintaining high performance [START_REF] Lin | Rust as a language for high performance GC implementation[END_REF]. The framework provides the interaction mechanism between Rust and Why3. By gluing them together, verified models can be directly executed in production environments for further testing. The coupling between Rust and extracted OCaml implementation enables us to perform VM tests to test the basic workings of the verified VM. Information of the overarching environment is obtained through the interface of Rust implementation, and the test can be performed on the execution of the OCaml implementations to check the operations in different transactions.

Examples of Property Verification and Tests

We now show some examples of property verification towards smart contracts and tests against Ethereum test suites. Specifically, we present the specification and verification of SafeMath library and SimpleAuction contract. For the tests, we perform the testing of arithmatic operations against the Ethereum test suite.

Overflow/Underflow property verification. We first take the example of Safe-Math from Solidity library. Overflow/Underflow problems often occur when we deal with number operations. For EVM, the unsigned integer type we perform arithmatic operations on range from 0 to 2 256 , which is specified as uint256 in the WhyML specification. The properties we verify are to guarantee that overflow and underflow problems would not occur in the number operations. Besides, the correctness of the operation results is also specified in the postconditions and further verified, for example, the last postcondition in the function div_safe.

As can be seen from the following definition of div_safe, the function body is comprised of three parts, as a Hoare triple, preconditions, program expressions and postconditions. The first precondition specifies that the divisor should be greater than zero. The first postcondition states that the returned value should satisfy the required property with no underflow issues. The other two postconditions are to guarantee the correctness of the operation result. We now proceed to the verification of the properties. The verification conditions can be obtained through running why3 prove on the WhyML file. The proving goals for div_safe are derived as follows: To prove the goals, we first apply the split VC transformation and then call theorem provers alt-ergo and cvc4 to prove the subgoals automatically. The proof session state will be stored in an XML file, which includes the proved WhyML file, the applied transformations, the used provers and the proof results. Complete proving goals derived from the functions and proof sessions can be found at [6].

Open Auction contract verification. The open auction contract is mainly comprised of three functions: (1) Everyone can send their bids through the bid function when the bidding period is not finished. When the bid sent by one bidder exceeds the current recorded highest bid, the auction state including the highestBidder and highestBid would be updated. Then the withdrawal amount of the previous highest bidder should be increased by the previous highest bid.

(2) When one bid is beaten by another higher raised bid, the previous bid should be returned back to the corresponding bidder. Bidders can call the withdraw function to get the money/Ether back. (3) The auction is ended by the auctionEnd function. If current time is already greater than the auctionEnd-Time, then the auction end_state should be set to True. As the bidding ended, the beneficiary would receive the final highest Bid.

In the WhyML specification, auction_status records the current state of the auction including the current highest bidder, the highest bid and the auction ended state. auction_constant records the beneficiary and the auctio-nEndTime and auction_ended records the final bidder, bid and the beneficiary claimed money/Ether amount. The properties to be verified are to guarantee the correctness of the functionality. For example, in the auctionEnd definition, the postcondition specifies the constraints of auction ended state and beneficiary claimed amount that the returned result should satisfy. Complete specification of the functions can be found at [6]. The generated verification conditions can be discharged through alt-ergo and cvc4 automatically. From the official EVM Consensus Tests [START_REF]Common tests for all Ethereum implementations[END_REF], we select the vmArithmeticTest set and run the test cases. The OCaml EVM implementation passes all the selected test cases and proves its capability in the production environment. A guide of reproducing the test result can be found at [6].

Related Work

Research interest of blockchain technology has exploded since the inception of Bitcoin. As the popularity of the second generation of blockchain, Ethereum, grows, a series of vulnerabilities have also appeared. Since EVM and smart contracts deal directly with the transactions of valuable cryptocurrency units among multiple parties, the safety of smart contracts and EVM implementations is of paramount importance. To address these challenges, researchers resorted to the techniques of formal methods and program analysis. Specification and Verification. An executable formal semantics of EVM has been created in the K framework by Everett et al. [START_REF] Hildenbrandt | KEVM: A complete formal semantics of the ethereum virtual machine[END_REF]. Compared with KEVM with the support of matching logic for verification, we use Hoare logic, which serves as a good framework for verification condition specification, to avoid the complex definitions of the operational semantics. A framework to analyze and verify the safety and the correctness of Solidity smart contracts in F* was presented in [START_REF] Bhargavan | Formal verification of smart contracts: Short paper[END_REF]. Hirai [START_REF] Hirai | Defining the ethereum virtual machine for interactive theorem provers[END_REF] proposed an EVM implementation in Lem, a language that can be compiled for a few interactive theorem provers. Then, safety properties of smart contracts can be proved in proof assistants like Isabelle/HOL. While in our work, we use WhyML for specification and programming, which supports both logical theories and programming data structures. Moreover, both automated and interactive external theorem provers can be relied on to discharge verification conditions. Testing and Debugging. The hevm project [15] is implemented in Haskell for unit testing and debugging of smart contracts. Sergey et al. [START_REF] Sergey | A concurrent perspective on smart contracts[END_REF] provided a new perspective between smart contracts and concurrent objects, based on which existing tools for understanding and debugging concurrent objects can be used on smart contract behaviors. In [START_REF] Luu | Making smart contracts smarter[END_REF], several new security problems were pointed out and a way to enhance the operational semantics of Ethereum was proposed to make smart contracts less vulnerable. Due to the difficulty of correcting the semantics of Ethereum, Luu et al. [START_REF] Luu | Making smart contracts smarter[END_REF] also implemented a symbolic execution tool OYENTE to find security bugs. While in our work, executable OCaml programs can be directly extracted from WhyML programs for further tests with the support of customized drivers and extraction mechanism.

Conclusion

We propose a framework to enable formal specification, verification and testing towards EVM. In this framework, the formalization of EVM is specified in WhyML, based on which, automatic SMT solvers and interactive theorem provers can be employed for verification. The OCaml implementation of EVM is extracted from the WhyML specification and then glued with Rust implementation based on the coupling framework. The coupling framework provides the interaction mechanism between OCaml and Rust, which allows us to perform tests on the new implementation without additional interface implementation.

Fig. 1 .

 1 Fig. 1. the Framework of Generating Verified EVM for Production Environment

  let interpreter (m: machine_state): machine_state = let inst = get_inst m in match inst with | Some (Arith ADD) -> let (st', a) = (pop_stack (m.mac_stack)) in let (st'', b) = (pop_stack st') in ... {m with mac_stack = push_stack st'' (a' + b'); ...}

Fig. 2 .

 2 Fig. 2. Running EVM in Production Environment

  let div_safe (a:uint256) (b:uint256): uint256 requires {to_int b > 0} ensures {to_int result >= 0} ensures {to_int a = 0 -> to_int result = 0} ensures {to_int a <> 0 -> to_int a = (to_int result) * (to_int b) + mod (to_int a) (to_int b)} = a / b

  goal VC div_safe : forall a:uint256, b:uint256. to_int b > 0 -> (not b = 0 && in_bounds (div a b)) /\ (forall result:uint256. result = div a b -> to_int result >= 0 && (to_int a = 0 -> to_int result = 0) && (not to_int a = 0 -> to_int a = (to_int result * to_int b + mod (to_int a) (to_int b))))

  let auctionEnd (current_time: uint) (auc_st: auction_status) (auc_const: auction_constant) (auc_end: auction_ended): (auction_status, auction_ended) ... ensures {let (_auc_st, _auc_end) = result in _auc_st.end_state = True && _auc_end.finalBidder = auc_st.highestBidder && _auc_end.finalBid = auc_st.highestBid && _auc_end.bene_amount.benefici = auc_const.beneficiary && _auc_end.bene_amount.benefit_amount = _auc_end.finalBid} = ... Testing of arithmatic operations. CITA-VM [3] is a Rust implementation of the EVM developed by the CITAHub team. In a forked version of CITA-VM, we patched the EVM interpreter by redirecting it to the OCaml implementation.

Acknowledgement

This work has been supported by the National Natural Science Foundation of China under grant no. 61772038 and 61532019, and the Guangdong Science and Technology Department (Grant no.2018B010107004). Thanks to members of Cryptape, especially Jan and Zhiwei, for the helpful discussions during the development of this framework.