Ananda Basu

Saddek Bensalem

Marius Bozga

Benoît Caillaud

Benoît Delahaye

Axel Legay

Benoit Caillaud

Benoit Delahaye

Statistical Abstraction and Model-Checking of Large Heterogeneous Systems

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Systems integrating multiple heterogeneous distributed applications communicating over a shared network are typical in various sensitive domains such as aeronautic or automotive embedded systems. Verifying the correctness of a particular application inside such a system is known to be a challenging task, which is often beyond the scope of existing exhaustive validation techniques. The main difficulty comes from network communication which makes all applications interfering and therefore forces exploration of the full state-space of the system.

Statistical Model Checking [START_REF] Hérault | Approximate probabilistic model checking[END_REF][START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF][START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] has recently been proposed as an alternative to avoid an exhaustive exploration of the state-space of the model. The core idea of the approach is to conduct some simulations of the system and then use statistical results in order to decide whether the system satisfies the property or not. Statistical model checking techniques can also be used to estimate the probability that a system satisfies a given property [START_REF] Hérault | Approximate probabilistic model checking[END_REF][START_REF] Grosu | Monte carlo model checking[END_REF]. Of course, in contrast with an exhaustive approach, a simulation-based solution does not guarantee a correct result. However, it is possible to bound the probability of making an error. Simulation-based methods are known to be far less memory and time intensive than exhaustive ones, and are sometimes the only option [START_REF] Younes | Numerical vs. statistical probabilistic model checking[END_REF][START_REF] Jansen | How fast and fat is your probabilistic model checker? an experimental performance comparison[END_REF]. Statistical model checking is widely accepted in various research areas such as systems ⋆ This work has been supported by the Combest EU project.

biology [START_REF] Clarke | Statistical model checking in biolab: Applications to the automated analysis of tcell receptor signaling pathway[END_REF][START_REF] Jha | A bayesian approach to model checking biological systems[END_REF] or software engineering, in particular for industrial applications. There are several reasons for this success. First, it is very simple to implement, understand and use. Second, it does not require extra modeling or specification effort, but simply an operational model of the system, that can be simulated and checked against state-based properties. Third, it allows model-checking of properties [START_REF] Clarke | Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator[END_REF] that cannot be expressed in classical temporal logics. Nevertheless, statistical-model checking still suffers from the system's complexity. In particular, for the case of heterogeneous systems, the number of components and their interactions are limiting factors on the number and length of simulations that can be conducted and hence on the accuracy of the statistical estimates.

We propose to exploit the structure of the system in order to increase the efficiency of the verification process. The idea is conceptually simple: instead of performing an analysis of the entire system, we propose to analyze each application separately, but under some particular context/execution environment. This context is a stochastic abstraction that represents the interactions with other applications running within the system and sharing the computation and communication resources. We propose to build such a context automatically by simulating the system and learning the probability distributions of key characteristics impacting the functionality of the given application.

The overall contribution of this paper is an application of the above method on an industrial case study, the heterogeneous communication system (HCS for short) deployed for cabin communication in a civil airplane. HCS is a heterogeneous system providing entertainment services (e.g., audio/video on passengers demand) as well as administrative services (e.g., cabin illumination, control, audio announcements), which are implemented as distributed applications running in parallel, across various devices within the plane and communicating through a common Ethernet-based network. The HCS system has to guarantee stringent requirements, such as reliable data transmission, fault tolerance, timing and synchronization constraints. An important requirement, which will be studied in this paper, is the accuracy of clock synchronization between different devices. This latter property states that the difference between the clocks of any two devices should be bounded by a small constant, which is provided by the user and depends on his needs. Hence, one must be capable of computing the smallest bound for which synchronization occurs and compare it with the bound expected by the user. Unfortunately, due to the large number of heterogeneous components that constitute the system, deriving such a bound manually from the textual specification is an unfeasible task. In this paper, we propose a formal approach that consists in building a formal model of the HCS, then applying simulation-based algorithms to this model in order to deduce the smallest value of the bound for which synchronization occurs. We start with a fixed value of the bound and check whether synchronization occurs. If yes, then we make sure that this is the best one. If no, we restart the experiment with a new value.

At the top of our approach, there should be a tool that is capable of modeling heterogeneous systems as well as simulating their executions and the interactions between components. In this paper, we propose to use the BIP toolset [START_REF] Basu | Modeling Heterogeneous Real-time Systems in BIP[END_REF] for doing so. BIP (Behaviour-Interaction-Priority) supports a methodology for building systems from atomic components encapsulating behavior, that communicate through interactions, and coordinate through priorities. BIP also offers a powerful engine to simulate the system and can thus be combined with a statistical model checking algorithm in order to verify properties. Our first contribution is to study all the requirements for the HCS to work properly and then derive a model in BIP. Our second contribution is to study the accuracy of clock synchronization between several devices of the HCS. In HCS the clock synchronization is ensured by the Precision Time Protocol (PTP for short) [START_REF] Delahaye | Precision clock synchronization protocol for networked measurement and control systems[END_REF], and the challenge is to guarantee that PTP maintains the difference between a master clock (running on a designated server within the system) and all the slave clocks (running on other devices) under some bound. Since this bound cannot be pre-computed, we have to verify the system for various values of the bound until we find a suitable one. Unfortunately, the full system is too big to be analyzed with classical exhaustive verification techniques. A solution could be to remove all the information that is not related to the devices under consideration. This is in fact not correct as the behavior of the PTP protocol is influenced by the other applications running in parallel within the heterogeneous system. Our solution to this state-space explosion problem is in two steps (1) we will build a stochastic abstraction for a part of the PTP application between the server and a given device; the stochastic part will be used to model the general context in which PTP is used, (2) we will apply statistical model checking on the resulting model.

Thanks to this approach, we have been able to derive precise bounds that guarantee proper synchronization for all the devices of the system. We also computed the probability of satisfying the property for smaller values of the bound, i.e., bounds that do not satisfy the synchronization property with probability 1. Being able to provide such information is of clear importance, especially when the best bound is too high with respect to the user's requirements. We have observed that the values we obtained strongly depend on the position of the device in the network. We also estimated the average and worst proportion of failures per simulation for bounds that are smaller than the one that guarantees synchronization. Checking this latter property has been made easy because BIP allows us to reason on one execution at a time. Finally, we have also considered the influence of clock drift on the synchronisation results. The experiments highlight the generality of our technique, which could be applied to other versions of the HCS as well as to other heterogeneous applications.

Due to space limitations, several constructions and algorithms are given in a technical report [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF].

An Overview of Statistical Model Checking

Consider a stochastic system S and a property φ. Statistical model checking refers to a series of simulation-based techniques that can be used to answer two questions: (1) Qualitative: Is the probability that S satisfies φ greater or equal to a certain threshold? and (2) Quantitative: What is the probability that S satisfies φ? Contrary to numerical approaches, the answer is given up to some correctness precision. In the rest of the section, we overview several statistical model checking techniques. Let B i be a discrete random variable with a Bernoulli distribution of parameter p. Such a variable can only take 2 values 0 and 1 with P r[B i = 1] = p and P r[B i = 0] = 1 -p. In our context, each variable B i is associated with one simulation of the system. The outcome for B i , denoted b i , is 1 if the simulation satisfies φ and 0 otherwise.

Qualitative Answer using Statistical Model Checking

The main approaches [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF][START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF] proposed to answer the qualitative question are based on hypothesis testing. Let p = P r(φ), to determine whether p ≥ θ, we can test H : p ≥ θ against K : p < θ. A test-based solution does not guarantee a correct result but it is possible to bound the probability of making an error. The strength (α, β) of a test is determined by two parameters, α and β, such that the probability of accepting K (respectively, H) when H (respectively, K) holds, called a Type-I error (respectively, a Type-II error ) is less or equal to α (respectively, β). A test has ideal performance if the probability of the Type-I error (respectively, Type-II error) is exactly α (respectively, β). However, these requirements make it impossible to ensure a low probability for both types of errors simultaneously (see [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] for details). A solution is to use an indifference region [p 1 , p 0 ] (with θ in [p 1 , p 0 ]) and to test H 0 : p ≥ p 0 against H 1 : p ≤ p 1 . We now sketch two hypothesis testing algorithms.

Single Sampling Plan. To test H 0 against H 1 , we specify a constant c. If n i=1 b i is larger than c, then H 0 is accepted, else H 1 is accepted. The difficult part in this approach is to find values for the pair (n, c), called a single sampling plan (SSP in short), such that the two error bounds α and β are respected. In practice, one tries to work with the smallest value of n possible so as to minimize the number of simulations performed. Clearly, this number has to be greater if α and β are smaller but also if the size of the indifference region is smaller. This results in an optimization problem, which generally does not have a closed-form solution except for a few special cases [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF]. In his thesis [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], Younes proposes a binary search based algorithm that, given p 0 , p 1 , α, β, computes an approximation of the minimal value for c and n.

Sequential probability ratio test. The sample size for a single sampling plan is fixed in advance and independent of the observations that are made. However, taking those observations into account can increase the performance of the test. As an example, if we use a single plan (n, c) and the m > c first simulations satisfy the property, then we could (depending on the error bounds) accept H 0 without observing the n -m other simulations. To overcome this problem, one can use the sequential probability ratio test (SPRT in short) proposed by Wald [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]. The approach is briefly described below.

In SPRT, one has to choose two values A and B (A > B) that ensure that the strength of the test is respected. Let m be the number of observations that have been made so far. The test is based on the following quotient:

p 1m p 0m = m i=1 P r(B i = b i | p = p 1 ) P r(B i = b i | p = p 0 ) = p dm 1 (1 -p 1 ) m-dm p dm 0 (1 -p 0 ) m-dm , (1)
where

d m = m i=1 b i . The idea behind the test is to accept H 0 if p1m p0m ≥ A, and H 1 if p1m p0m ≤ B.
The SPRT algorithm computes p1m p0m for successive values of m until either H 0 or H 1 is satisfied; the algorithm terminates with probability 1 [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]. This has the advantage of minimizing the number of simulations. In his thesis [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], Younes proposed a logarithmic based algorithm SPRT that given p 0 , p 1 , α and β implements the sequential ratio testing procedure.

Quantitative Answer using Statistical Model Checking

In [START_REF] Hérault | Approximate probabilistic model checking[END_REF][START_REF] Laplante | Probabilistic abstraction for model checking: An approach based on property testing[END_REF] Peyronnet et al. propose an estimation procedure to compute the probability p for S to satisfy φ. Given a precision δ, Peyronnet's procedure, which we call PESTIMATION, computes a value for p ′ such that |p ′ -p|≤δ with confidence 1 -α. The procedure is based on the Chernoff-Hoeffding bound [START_REF] Hoeffding | Probability inequalities[END_REF]. Let B 1 . . . B m be m discrete random variables with a Bernoulli distribution of parameter p associated with m simulations of the system. Recall that the outcome for each of the B i , denoted b i , is 1 if the simulation satisfies φ and 0 otherwise. Let p ′ = ( m i=1 b i )/m, then Chernoff-Hoeffding bound [START_REF] Hoeffding | Probability inequalities[END_REF] gives P r(|p ′ -p| > δ) < 2e -mδ 2 4 . As a consequence, if we take m≥ 4 δ 2 log( 2 α ), then P r(|p ′ -p|≤δ) ≥ 1 -α. Observe that if the value p ′ returned by PESTIMA-TION is such that p ′ ≥θ -δ, then S |= P r ≥θ with confidence 1 -α.

Playing with Statistical Model Checking Algorithms

The efficiency of the above algorithms is characterized by the number of simulations needed to obtain an answer. This number may change from executions to executions and can only be estimated (see [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] for an explanation). However, some generalities are known. For the qualitative case, it is known that, except for some situations, SPRT is always faster than SSP. When θ = 1 (resp. θ = 0) SPRT degenerates to SSP; this is not problematic since SSP is known to be optimal for such values. PESTIMATION can also be used to solve the qualitative problem, but it is always slower than SSP [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF]. If θ is unknown, then a good strategy is to estimate it using PESTIMATION with a low confidence and then validate the result with SPRT and a strong confidence.

Validation Method and the BIP Toolset

Consider a system consisting of a set of distributed applications running on several computers and exchanging messages on a shared network infrastructure.

Assume also that network communication is subject to given bandwidth restrictions as well as to routing and scheduling policies applied on network elements. Our method attempts to reduce the complexity of validation of a particular application of such system by decoupling the timing analysis of the network and functional analysis of each application.

We start by constructing a model of the whole system. This model must be executable, i.e., it should be possible to obtain execution traces, annotated with timing information. For a chosen application, we then learn the probability distribution laws of its message delays by simulating the entire system. The method then constructs a reduced stochastic model by combining the application model where the delays are defined according to the laws identified at the previous step. Finally, the method applies statistical model-checking on the resulting stochastic model.

Our models are specified within the BIP framework [START_REF] Basu | Modeling Heterogeneous Real-time Systems in BIP[END_REF]. BIP is a componentbased framework for construction, implementation and analysis of systems composed of heterogeneous components. In particular, BIP fulfills all the requirements of the method suggested above, that are, models constructed in BIP are operational and can be thoroughly simulated. BIP models can easily integrate timing constraints, which are represented with discrete clocks. Probabilistic behaviour can also be added by using external C functions.

The BIP framework is implemented within the BIP toolset [START_REF]The BIP Toolset[END_REF], which includes a rich set of tools for modeling, execution, analysis (both static and on-the-fly) and static transformations of BIP models. It provides a dedicated programming language for describing BIP models. The front-end tools allow editing and parsing of BIP programs, and generating an intermediate model, followed by code generation (in C) for execution and analysis on a dedicated middleware platform. The platform also offers connections to external analysis tools. A more complete description of BIP can be found in [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF].

Case Study: Heterogeneous Communication System

The case study concerns a distributed heterogeneous communication system (HCS) providing an all electronic communication infrastructure to be deployed, typically for cabin communication in airplanes or for building automation. The HCS system contains various devices such as sensors (video camera, smoke detector, temperature, pressure, etc.) and actuators (loudspeakers, light switches, temperature control, signs, etc.) connected through a wired communication network to a common server. The server runs a set of services to monitor the sensors and to control the actuators. The devices are connected to the server using network access controllers (NAC) as shown for an example architecture in Figure 1. An extended star-like HCS architecture with several daisy chains of NACs and devices is presented in [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF].

The system-wide HCS architecture is highly heterogeneous. It includes hardware components and software applications ensuring functions with different characteristics and degree of criticality e.g., audio streaming, device clock syn- SmokeSensor NAC (0, 0) (0, 1) (0, 2) (0, 3)

(3, 3) (3, 2) (3, 1) (3, 0) (1)
( chronisation, sensor monitoring, video surveillance. It also integrates different communication and management protocols between components. The HCS system has to guarantee stringent requirements, such as reliable data transmission, fault tolerance, timings and synchronization constraints. For example, the latency for delivering alarm signals from sensors, or for playing audio announcements should be smaller than certain predefined thresholds. Or, the accuracy of clock synchronization between different devices, should be guaranteed under the given physical implementation of the system. The HCS case study poses challenges that require component-based design techniques, since it involves heterogeneous components and communication mechanisms, e.g. streaming based on the data-flow paradigm as well as event driven computation and interaction. Its modeling needs combination of executable and analytic models especially for performance evaluation and analysis of non-functional properties.

We have modeled an instance of the HCS system in BIP. As shown in Figure 1, the system consists of one Server connected to a daisy chain of four NACs, addressed 0 • • • 3, and several devices. Devices are connected in daisy chains with the NACs, the length of each chain being limited to four in our example. For simplicity, devices are addressed (i, j), where i is the address of the NAC and j is the address of the device. The model contains three types of devices, namely Audio Player, Video Camera and Smoke Sensor. The devices connected to NAC(0) and NAC( 2) have similar topology. The first two daisy-chains consist of only Audio Player devices. The third daisy-chain ends with a Smoke Sensor, and the fourth daisy-chain consists of just one Video Camera. The devices connected to NAC(1) and NAC(3) have exactly the same topology, consisting of several Audio Player and one Smoke Sensor devices.

The system depicted in Figure 1 contains 58 devices in total. The BIP model contains 297 atomic components, 245 clocks, and its state-space is of order 2 3000 . The size of the BIP code for describing the system is 2468 lines, which is translated to 9018 lines in C. A description of the key components is given in [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF].

Experiments on the HCS

One of the core applications of the HCS case study is the PTP protocol, which allows the synchronization of the clocks of the various devices with the one of the server. It is important that this synchronization occurs properly, i.e., the difference between the clock of the server and the one of any device is bounded by a small constant. Studying this problem is the subject of this section. Since the BIP model for the HCS is extremely large (number of components, size of the state space, ...), there is no hope to analyse it with an exhaustive verification technique. Here, we propose to apply our stochastic abstraction. Given a specific device, we will proceed in two steps. First, we will conduct simulations on the entire system in order to learn the probability distribution on the communication delays between this device and the server. Second, we will use this information to build a stochastic abstraction of the application on which we will apply statistical model checking. We start with the stochastic abstraction for the PTP.

The Precision Time Protocol IEEE 1588

The Precision Time Protocol [START_REF] Delahaye | Precision clock synchronization protocol for networked measurement and control systems[END_REF] has been defined to synchronize clocks of several computers interconnected over a network. The protocol relies on multicast communication to distribute a reference time from an accurate clock (the master) to all other clocks in the network (the slaves) combined with individual offset correction, for each slave, according to its specific round-trip communication delay to the master. The accuracy of synchronization is negatively impacted by the jitter (i.e., the variation) and the asymmetry of the communication delay between the master and the slaves. Obviously, these delay characteristics are highly dependent on the network architecture as well as on the ongoing network traffic.

We present below the abstract stochastic model of the PTP protocol between a device and the server in the HCS case study. The model consists of two (deterministic) application components respectively, the master and the slave clocks, and two probabilistic components, the media, which are abstraction of the communication network between the master and the slave. The former represent the behaviour of the protocol and are described by extended timed i/o-automata. The latter represent a random transport delay and are simply described by probabilistic distributions. Recap that randomization is used to represent the context, i.e., behaviors of other devices and influence of these behaviors on those of the master and the device under consideration.

The time of the master process is represented by the clock variable θ m . This is considered the reference time and is used to synchronize the time of the slave clock, represented by the clock variable θ s . The synchronization works as follows. Periodically, the master broadcast a sync message and immediately after a fol-lowUp message containing the time t 1 at which the sync message has been sent. Time t 1 is observed on the master clock θ m . The slave records in t 2 the reception time of the sync message. Then, after the reception of the followUp, it sends a delay request message to the master and records its emission time t 3 . Both t 2 and t 3 are observed on the slave clock θ s . The master records on t 4 the reception time of the request message and sends it back to the slave on the reply message. Again, t 4 is observed on the master clock θ m . Finally, upon reception of reply, the slave computes the offset between its time and the master time based on (t i ) i=1,4 and updates its clock accordingly. In our model, the offset is computed differently in two different situations. In the first situation, which is depicted in Figure 2, the average delays from master to slave and back are supposed to be equal i.e., µ(ρ 1 ) = µ(ρ 2 ). In the second situation, delays are supposed to be asymmetric, i.e., µ(ρ 1 ) = µ(ρ 2 ). In this case, synchronization is improved by using an extra offset correction which compensate for the difference, more precisely, o := (t 2 + t 3 -t 1 -t 4 )/2 + (µ(ρ 2 ) -µ(ρ 1 ))/2. This offset computation is an extension of the PTP specification and has been considered since it ensures better precision when delays are not symmetric (see Section 5).

Encoding the abstract model of timed i/o-automata given in Figure 2 in BIP is quite straightforward and can be done with the method presented in [START_REF] Basu | Modeling Heterogeneous Real-time Systems in BIP[END_REF]. The distribution on the delay is implemented as a new C function in the BIP model. It is worth mentioning that, since the two i/o automata are deterministic, the full system depicted in Figure 2 is purely stochastic.

The accuracy of the synchronization is defined by the absolute value of the difference between the master and slave clocks |θ m -θ s |, during the time. Our aim is to check the (safety) property of bounded accuracy φ ∆ , that is, always |θ m -θ s | ≤ ∆ for arbitrary fixed non-negative real ∆.

Finally, a simpler version of this protocol has been considered (see [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF]) and analyzed. In that study, delay components have been modeled using non-deterministic timed i/o automata as well and represent arbitrary delays bounded in some intervals [L, U ]. It has been shown that, if the clock drift is negligible, the best accuracy ∆ ⋆ that can be obtained using PTP is respectively U-L 2 in the symmetric case, and U1+U2-L1-L2 4 in the asymmetric case. That is, the property of bounded accuracy holds trivially iff ∆ ≥ ∆ * .

Model Simulations

In this section, we describe our approach to learn the probability distribution over the delays. Consider the server and a given device. In a first step, we run simulations on the system and measure the end-to-end delays of all PTP messages between the selected device and the server. For example, consider the case of delay request messages and assume that we made 33 measures. The result will be a series of delay values and, for each value, the number of times it has been observed. As an example, delay 5 has been observed 3 times, delay 19 has been observed 30 times. The probability distribution is represented with a table of 33 cells. In our case, 3 cells of the table will contains the value 5 and 30 will contain the value 19. The BIP engine will select a value in the table following a uniform probability distribution.

According to our experiments, 2000 delay measurements are enough to obtain an accurate estimation of the probability distribution. However, for confidence reasons, we have conducted 4000 measurements. We have also observed that the value of the distribution clearly depends on the position of the device in the topology (see [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF] for an illustration). It is worth mentioning that running one single simulation allowing 4000 measurements of the delay of PTP frames requires running the PTP protocol with an increased frequency i.e., the default PTP period (2 minutes) being far too big compared with the period for sending audio/video packets (tens of milliseconds). Therefore, we run simulations where PTP is executed once every 2 milliseconds and, we obtain 4000 measurements by simulating approximately 8 seconds of the global system lifetime. Each simulation uses microsecond time granularity and takes around 40 minutes on a Pentium 4 running under a Linux distribution.

Experiments on Precision Estimation for PTP

Three sets of experiments are conducted. The first one is concerned with the bounded accuracy property (see Section 5.1). In the second one, we study average failure per execution for a given bound. Finally, we study the influence of drift on the results.

Property 1: Synchronization. Our objective is to compute the smallest bound ∆ under which synchronization occurs properly for any device. We start with an experiment that shows that the value of the bound depends on the place of the device in the topology. For doing so, we use ∆ = 50µs as a bound and then compute the probability for synchronization to occur properly for all the devices. In the paper, for the sake of presentation, we will only report on a sampled set of devices: (0, 0), (0, 3), (1, 0), (1, 10), (2, 0), (2, 3), (3, 0), [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF][START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF], but our global observations extend to any device. We use PESTIMATION with a confidence of 0.1. The results, which are reported in Figure 3a, show that the place in the topology plays a crucial role. Device [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF][START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF] has the best probability value and Device (2, 0) has the worst one. All the results in Figure 3a have been conducted on the model with asymmetric delays. For the symmetric case, the probability values are much smaller. As an example, for Device (0, 0), it decreases from 0.388 to 0.085. The above results have been obtained in less than 4 seconds. As a second experiment, we have used SPRT and SSP to validate the probability value found by PESTIMATION with a higher degree of confidence. The results, which are presented in Table 1 for Device (0, 0), show that SPRT is faster than SSP and PESTIMATION. Our second step was to estimate the best bound. For doing so, for each device we have repeated the previous experiments for values of ∆ between 10µs and 120µs. Figure 4a gives the results of the probability of satisfying the bounded accuracy property as a function of the bound ∆ for the asymmetric version of PTP. The figure shows that the smallest bound which ensure synchronization for any device is 105µs (for Device (3, 0)). However, devices (0, 3) and (3, 3) already satisfy the property with probability 1 for ∆ = 60µs. A comparison between SSP and PESTIMATION is given in [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF].

The above experiments have been conducted assuming simulations of 1000 BIP interactions and 66 rounds of the PTP protocol. Since each round of the PTP takes two minutes, this also corresponds to 132 minutes of the system's life time. We now check whether the results remain the sames if we lengthen the simulations and hence system's life time. Figure 5 shows, for Devices (0, 0) and (3, 0), the probability of synchronization for various values of ∆ and various length of simulations (1000, 4000, 8000 and 10000 (660 minutes of system's life time) steps). We used PESTIMATION with a precision and a confidence of 0.1. The best bounds do not change. However, the longer the simulations are, the more the probability tends to be either 0 or 1 depending on the bound. Property 2: Average failure. In the previous experiment, we have computed the best bound to guarantee the bounded accuracy property. It might be the case that the bound is too high regarding the user's requirements. In such case, using the above results, we can already report on the probability for synchronization to occur properly for smaller values of the bound. We now give a finer answer by quantifying the average and worst number of failures in synchronization that occur per simulation when working with smaller bounds. For a given simulation,

Fig. 1 :

 1 Fig. 1: HCS Example Model.

Fig. 2 :

 2 Fig.2: Abstract stochastic PTP between the server and a device.

  Average proportion of failures.

Fig. 3 :

 3 Fig. 3: Probability of satisfying the bounded accuracy property and average proportion of failures for a ∆ = 50µs and the asymmetric version of PTP.

  Average proportion of failures.

Fig. 4 :

 4 Fig. 4: Probability of satisfying the bounded accuracy property and average proportion of failures as functions of the bound ∆ for the asymmetric version of PTP.

Table 1 :

 1 Number of simulations / Amount of time required for PESTIMATION, SSP and SPRT.

	Precision	10 -1	10 -2	10 -3
	Confidence	10 -5 10 -10 10 -5 10 -10	10 -5	10 -10
	PESTIMATION	4883 9488 488243 948760 48824291 94875993 17s 34s 29m 56m > 3h > 3h
	SSP	1604 3579 161986 368633 16949867 32792577 10s 22s 13m 36m > 3h > 3h
	SPRT	316 1176 12211 22870 148264 2s 7s 53s 1m38s 11m	311368 31m

the proportion of failures is obtained by dividing the number of failures by the number of rounds of PTP. We will now estimate, for a simulation of 1000 steps (66 rounds of the PTP), the average and worst value for this proportion. To this purpose, we have measured (for each device) this proportion on 1199 simulations with a synchronization bound of ∆ = 50µs. As an example, we obtain average proportions of 0.036 and 0.014 for Device (0, 0) using the symmetric and asymmetric versions of PTP respectively. As a comparison, we obtain average proportions of 0.964 and 0.075 for Device [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF]0). The average proportion of failures with the bound ∆ = 50µs and the asymmetric version of PTP is given in Figure 3b. Figure 6a presents, for the sampled devices, the worst proportion of failures using the asymmetric version of PTP. The worst value is 0.25, which is obtained for Device (2, 0). On the other hand, the worst value is only 0.076 for Device (0, 0). The experiment, which takes about 6 seconds per device, was then generalized to other values of the bound. Figures 4b and6b give the average and worst proportion of failure as a function of the bound.

The above experiment gives, for several value of ∆ and each device, the worst failure proportion with respect to 1199 simulations. We have also used PESTI-MATION with confidence of 0.1 and precision of 0.1 to verify that this value remains the same whatever the number of simulations is. The result was then validated using SSP with precision of 10 -3 and confidence of 10 -10 . Each experiment took approximately two minutes. Finally, we have conducted experiments to check whether the results remain for longer simulations. Figure 7a shows that the average proportion does not change and Figure 7b shows that the worst proportion decreases when the length of the simulation increases. as the same rate. In our model, drift is incorporated as follows: each time the clock of the server is increased by 1 time unit, the clock of the device is increased by 1 + ε time units, with ε ∈ [-10 -3 , 10 -3 ]. Using this modified model, we have re-done the experiments of the previous sections and observed that the result remains almost the same. This is not surprising as the value of the drift is significantly smaller than the communication jitter, and therefore it has less influence on the synchronization. A drift of 1 time unit has a much higher impact on the probability. As an example, for Device (0, 0), it goes from a probability of 0.387 to a probability of 0.007. It is worth mentioning that exhaustive verification of a model with drifting clocks is not an easy task as it requires to deal with complex differential equations. When reasoning on one execution at a time, this problem is avoided.


Jan Smans
email: jan.smans@cs.kuleuven.be

Bart Jacobs
email: bart.jacobs@cs.kuleuven.be

Frank Piessens
email: frank.piessens@cs.kuleuven.be

Heap-dependent Expressions in Separation Logic

Separation logic is a popular specification language for imperative programs where the heap can only be mentioned through pointsto assertions. However, separation logic's take on assertions does not match well with the classical view of assertions as boolean, side effectfree, potentially heap-dependent expressions from the host programming language familiar to many developers. In this paper, we propose a variant of separation logic where side effectfree expressions from the host programming language, such as pointer dereferences and invocations of pure methods, can be used in assertions. We modify the symbolic execution-based verification algorithm used in Smallfoot to support mechanized checking of our variant of separation logic. We have implemented this algorithm in a tool and used the tool to verify some interesting programming patterns.

Introduction

The design of many specification languages centers around the idea that specifications should resemble the host programming language, in order to make it easy for developers to adopt and learn the specification language and to provide a straightforward semantics for run-time checking. Examples of such specification languages include the Java Modeling Language [START_REF] Gary | JML: A notation for detailed design[END_REF] and Spec# [START_REF] Barnett | The Spec# programming system: An overview[END_REF], where field dereferences and certain method calls can be used freely within contracts.

Over the past couple of years, separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] has proven to be a promising, powerful alternative to traditional specification formalisms. However, contrary to for instance JML and Spec#, separation logic assertions are quite different from the host programming language, in particular because the heap can only be mentioned through points-to assertions and expressions cannot mention field dereferences.

In this paper, we try to achieve the best of both worlds, by combining the power of separation logic with the programmer-friendly notation offered by traditional specification languages. In particular, we propose a variant of separation logic where side effect-free, potentially heap-dependent expressions from the host programming language can freely be mentioned inside specifications. In addition, we port the symbolic execution-based verification algorithm used in Smallfoot [START_REF] Berdine | Symbolic execution with separation logic[END_REF] to our variant of separation logic such that program correctness can be checked mechanically.

⋆ Bart Jacobs is a Postdoctoral Fellow of the Research Foundation -Flanders (FWO).

Supporting heap-dependent expressions in separation logic is challenging for a number of reasons. First of all, as pure methods can be used in specifications, the question arises of how to frame their return values. Secondly, assertions can be ill-defined, for example because the assertion dereferences a pointer while it does not have permission to do so. In this paper, we solve the former challenge by encoding the fact that a pure method's return value depends only on values stored in the heap covered by the precondition. We solve the latter challenge by performing additional checks when assuming and producing assertions.

In summary, the contributions of this paper are as follows:

-We propose a variant of separation logic where heap-dependent expressions from the host programming language, in particular pointer dereferences and invocations of pure methods, can be used in specifications. -We modify Smallfoot's symbolic execution-based verification algorithm to support mechanized checking of our variant of separation logic. -We implemented our algorithm in a tool and report on experience in verifying some interesting programming patterns.

The remainder of this paper is structured as follows. Section 2 introduces our variant of separation logic and applies it in an example. In Section 3, we propose a verification algorithm for the specification language introduced in Section 2. Finally, we discuss experience with a verifier prototype, compare with related work and conclude in Sections 4, 5 and 6.

Separation Logic with Side effect-free Expressions

We describe our variant of separation logic in the context of the imperative language of Figure 1. In this figure, overlining indicates repetition; annotations are highlighted by a gray background. A program consists of a number of declarations and a main routine s. A declaration is either a mutator function, a pure function or a predicate definition. Each mutator function has a corresponding contract, consisting of a preand postcondition, and a method body, consisting of a number of statements followed by a return statement. Each pure function has a corresponding precondition and a method body, returning a side effect-free expression (that can potentially call the pure function itself). A predicate definition assigns a name to an assertion. A statement is either a memory allocation, a variable update, a heap update, a mutator function call, a free statement, an assert statement, an if-then-else statement, or an open or close statement. Note that the last two statements are ghost statements: they have no runtime effect and are only needed to indicate to the program verifier when folding and unfolding of predicates is required (discussed in Section 3). An expression is a variable, a constant, a pointer dereference, a pure method call, an open expression, an operator expression or an old expression. Note that all expressions are side effect-free; however some of them depend on the heap. An assertion is either a predicate assertion, an access assertion, a separating conjunction, an equality between expressions or an untouched assertion. An access assertion acc(e) denotes the permission to dereference e. In classical separation logic, acc(e) would be denoted by e → . An untouched assertion untouched(A) is a two-state assertion that holds if the values in the heap covered by A are the same in both the pre-and post-state. In the remainder of this paper, we use true as syntactic sugar for the assertion 0 = 0, and false as syntactic sugar for 1 = 0. In the remainder of this paper, we consider only well-formed programs (Definition 1). In our implementation, well-formedness is checked using a simple syntactic analysis. Let us take a look at the example program of Figure 2. This program declares a predicate, a pure function and a number of mutator functions for dealing with cells, together with a main routine that uses the aforementioned functions to create and interact with cells. The pure function get returns the value of the cell referred to by c. Its precondition demands that c is a valid cell data structure. Note that pure functions do not have postconditions, as they cannot modify the program state. create cell creates a new cell data structure with value 0. create cell 's postcondition not only states that the result is a valid cell, but also expresses that resulting cell holds 0 via the pure function get. inc increments the value of a cell by one. Note that an old expression is used to relate the preand post-state. copy copies the value of cell d to cell c. The untouched assertion in its postcondition expresses that the heap covered by cell (d) is not modified by copy. Client code can use the latter information to frame pure methods that depend on cell (d). For example, clients can prove that get(d)'s return value is the same before and after calling copy. The main routine creates two cells, c 1 and c 2 , updates their values, checks that the value of c 1 is 1, and disposes both cells. Note that in order to prove that the assertion never fails, one must show that creating and modifying c 2 does not affect the return value of get(c 1 ).

The function bodies in Figure 2 contain open and close ghost statements. These statements instruct the program verifier to respectively unfold and fold predicates during symbolic execution. For example, the close statement in the body of create cell removes the body of the predicate cell from the symbolic heap and replaces it with the predicate itself, thereby establishing the postcondition. A more detailed description of symbolic execution and open and close statements will be given in Section 3.

Verification

In this section, we describe the symbolic execution-based verification algorithm for our variant of separation logic. After defining how we represent program states symbolically (section 3.1), we define symbolic evaluation and execution of expressions and statements (section 3.2). Based on these definitions, we define what it means for a program to be valid (section 3.3).

Symbolic State

A symbolic state is a four-tuple (h, g, γ, π) consisting of a symbolic heap h, a symbolic pre-state heap g, a symbolic store γ and a path condition π. A symbolic heap is a multiset of heap chunks, where each heap chunk q[s](t) consists of a predicate name q, a first-order term s and a list of first-order terms t. We refer to the term s as the snapshot of the heap chunk. A symbolic store is a partial function from variables to first-order terms. Finally, a path condition is a set of first-order formulas, describing the conditions that hold on the current execution path.

In the remainder of this section, we describe the symbolic execution algorithm itself. The core of this algorithm consists of 4 functions: eval, produce, consume and exec. These functions respectively represent symbolic evaluation of expressions, assuming and checking assertions and symbolic execution of statements. All aforementioned functions are written in continuation passing style. That is, each function takes a continuation parameter (typically called Q) that represents the work to be done on the current path. Their signatures are as follows:

eval : H × H × Γ × Π × e × (T × Π → B) → B produce : H × H × Γ × Π × T × A × (H × Π → B) → B consume : H × H × Γ × Π × A × (H × Π × T → B) → B exec : H × H × Γ × Π × s × (H × Γ × Π → B) → B
In the above signatures, H stands for the set of symbolic heaps, Γ for the set of symbolic stores, Π for the set of path conditions, T for the set of first-order terms and B for the set of booleans. Note that each of the aforementioned functions returns a boolean, indicating whether symbolic execution was successful.

Symbolic Execution

Preliminaries The symbolic state represents symbolic values as first-order terms and information about those values as first-order formulas. In the algorithm, we use a first-order logic with equality. The signature of the logic contains a number of built-in functions, including unit, pair , fst and snd , which are used to create snapshots. A snapshot uniquely determines the values in the heap covered by a predicate. unit is the empty snapshot, while pair (a, b) combines snapshots a and b. The functions are axiomatized as follows:

∀a, b • fst(pair (a, b)) = a ∀a, b • snd (pair (a, b)) = b
We do not explicitly mention these axioms in our algorithm. Instead, we write π ⊢ φ (denoting that formula φ is provable from π) as a shorthand for π ∪ T ⊢ φ, where T is the theory containing the two axioms described above. Our implementation relies on the Z3 SMT solver [START_REF] De | Z3: An efficient SMT solver[END_REF] to discharge such proof tasks.

A key question our approach has to answer is how to encode pure functions during verification in a way that allows us to frame their return values. Like other verification approaches [START_REF] Rudich | Checking well-formedness of pure-method specifications[END_REF][START_REF] K. Rustan | Practical reasoning about invocations and implementations of pure methods[END_REF][START_REF] Jacobs | Inspector methods for state abstraction[END_REF][START_REF] Darvas | Practical reasoning about invocations and implementations of pure methods[END_REF][START_REF] Smans | Automatic verification of java programs with dynamic frames[END_REF][START_REF] Darvas | Reasoning about method calls in interface specifications[END_REF], we encode a pure function as a first-order function in the verification logic and encode a call of a pure function as an application of the corresponding first-order function. The key to solving the issue of framing is the fact that a pure function's return value can only depend on memory locations covered by its precondition. This dependence on part of the heap is encoded as an additional function parameter. As we will show in Figure 3, this parameter is the snapshot of the function's precondition. For example, the signature of the function symbol for the pure function get of Figure 2 is get : T × T → T . The first parameter represents the values in the heap covered by the precondition, while the second parameter corresponds to the pure function's parameter c.

Note that the functions produce and consume do not contain cases for acc(e). Instead, the algorithm considers acc to be just another predicate with one parameter.

If at a certain point during symbolic execution the path condition is inconsistent, then that point is not reachable during a concrete execution of the program. In our implementation, we check consistency of the path condition whenever a new formula is added to it. If adding a new formula makes the path condition inconsistent, we simply stop symbolic execution and return true (indicating that symbolic execution succeeded). To avoid cluttering the rules, we do not explicitly show consistency checks in the definitions of eval, consume, produce and exec.

Symbolic evaluation of expressions eval(h, g, γ, π, e, Q) (defined in Figure 3) evaluates the expression e in symbolic state (h, g, γ, π) and passes both the resulting term and a potentially updated path condition to the continuation Q. More specifically, symbolic evaluation of a variable x corresponds to looking up x in the symbolic store and passing the resulting term to the continuation. A constant evaluates to itself. Dereferencing a pointer is allowed only if the thread has permission to do so. To check whether the thread has permission, the algorithm looks in the symbolic heap for a matching chunk. If a matching chunk is found, that chunk's snapshot is passed to the continuation; otherwise, eval(h, g, γ, π, [e], Q) fails.

eval(h, g, γ, π, x, Q) ≡ Q(γ(x), π) eval(h, g, γ, π, c, Q) ≡ Q(c, π) eval(h, g, γ, π, [e], Q) ≡ eval(h, g, γ, π, e, (λt, π ′ • let matches = { acc[ts](t1) ∈ h | π ⊢ t1 = t } in ∃acc[ts](t1) ∈ matches • Q(ts, π ′ ))) eval(h,
= t}))))) else Q(p(s, t1, . . . , tn), π ′ )))))))
eval(h, g, γ, π, open q(e1, . . . , en) in e, Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • . . . (λtn, πn• consume(h, g, γ, πn, q(e1, . . . , en), (λh ′ , π ′ , s• produce(h ′ , g, {(x1, t1), . . . , (xn, tn)}, π ′ , s, definition(q), (λh ′′ , π ′′ • eval(h ′ , g, γ, π ′′ , e, Q))))))))

eval(h, g, γ, π, e1 op e2, Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • eval(h, g, γ, π1, e2, (λt2, π2• Q(t1 op t2, π2)))))

eval(h, g, γ, π, old(e), Q) ≡ eval(g, g, γ, π, e, Q) Fig. 3. Symbolic evaluation of expressions.

Calling a pure function p(e 1 , . . . , e n ) is allowed only if its precondition holds. Our algorithm checks whether the precondition holds by consuming it. Note that consuming the precondition not only returns an updated heap and path condition, but also a snapshot s. This snapshot is used as the first parameter in the application of the corresponding first-order function. Note that the algorithm branches on the fact whether p's body is visible. That is, if the body is visible, an assumption stating that evaluation of p(e 1 , . . . , e n ) equals evaluation of its body is added to the path condition passed to the continuation. An opening expression open q(e 1 , . . . , e n ) in e evaluates the expression e in a context where the predicate q(e 1 , . . . , e n ) is replaced by its body. To symbolically evaluate an binary operation e 1 op e 2 , the algorithm applies the operation to the corresponding symbolic values, t 1 and t 2 . Evaluation of an old expression old(e) corresponds to evaluating e in the pre-state heap g. Symbolic production of assertions produce(h, g, γ, π, s, A, Q) assumes the assertion A in the symbolic state (h, g, γ, π) based on snapshot s and passes a potentially updated heap and path condition to its continuation Q. The parameter s is used to determine the snapshots of heap chunks created during production. The function produce is defined in terms of the helper function produce ′ as follows:

produce(h, g, γ, π, s, A, Q) ≡ produce ′ (∅, g, γ, π, s, A, (λh ′ , π ′ • Q(h ⊎ h ′ , π ′ )))
produce ′ starts with an empty heap to ensure that assertions are self-framing. That is, the assertion A should only dereference a pointer if A itself demands access to that pointer.

Figure 4 shows the definition of produce ′ . To produce a predicate assertion q(e 1 , . . . , e n ), we add a predicate chunk for q to the symbolic store with snapshot s. To produce a separating conjunction A 1 * A 2 , we must first produce A 1 and afterwards produce A 2 in the resulting symbolic state. Note that the snapshot s is split up into two pieces using the functions fst and snd . Producing an equality e 1 = e 2 comes down to adding the assumption that the values of both expressions are equal to the path condition. Finally, to produce untouched(A), we consume A in both the current symbolic heap h and the pre-state heap g, and assume that the resulting snapshots are equal.

produce ′ (h, g, γ, π, s, q(e1, . . . , en), Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • . . . eval(h, g, γ, πn-1, en, (λtn, πn• Q(h ⊎ {q[s](t1, . . . , tn)}, πn)))))

produce ′ (h, g, γ, π, s, A1 * A2, Q) ≡ produce ′ (h, g, γ, π, fst(s), A1, (λh ′ , π ′ • produce ′ (h ′ , g, γ, π ′ , snd (s), A2, Q))) produce ′ (h, g, γ, π, s, e1 = e2, Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • eval(h, g, γ, π1, e2, (λt2, π2• Q(h, π2 ∪ {t1 = t2}))))) produce ′ (h, g, γ, π, s, untouched(A), Q) ≡ consume(h, g, γ, π, A, (λ , , s1 • consume(g, g, γ, π, A, (λ , , s2• Q(h, π ∪ {s1 = s2})))))
Fig. 4. Production of assertions.

Symbolic consumption of assertions Consumption is the reverse of production. consume(h, g, γ, π, A, Q) checks if A holds in the symbolic state (h, g, γ, π) and passes a potentially updated heap, path condition and the snapshot of the consumed heap chunks to the continuation Q. Note that "checking" of spatial assertions causes heap chunks to be removed from the symbolic heap. consume is defined in terms of the helper function consume ′ as follows:

consume(h, g, γ, π, A, Q) ≡ consume ′ (h, h, g, γ, π, A, Q)
The first symbolic heap passed to consume ′ is used for evaluating expressions, while the second represents the remainder of the original heap which is not consumed yet by the assertion.

Figure 5 shows the definition of consume ′ . Consumption of a predicate assertion q(e 1 , . . . , e n ) succeeds only if a heap chunk matching q[ ](t 1 , . . . , t n ) exists. This heap chunk is removed from the symbolic heap and its snapshot is passed to the continuation. To consume A 1 * A 2 , one must first consume A 1 and afterwards consume A 2 . A pair containing the snapshots of A 1 and A 2 is passed to the continuation. Consumption of e 1 = e 2 succeeds only if both expressions are provably (from the path condition) equal and the continuation Q succeeds. Finally, consumption of untouched(A) succeeds only if the snapshots obtained by consuming A in both the pre-and post-state are provably equal.

consume ′ (h, h ′ , g, γ, π, q(e1, . . . , en), Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • . . . eval(h, g, γ, πn-1, en, (λtn, πn•

let matches = {q[s](t ′ 1 , . . . , t ′ 1 ) ∈ h ′ | πn ⊢ t1 = t ′ 1 ∧ . . . ∧ tn = t ′ n } in ∃q[s](t ′ 1 , . . . , t ′ 1 ) ∈ matches • Q(h ′ -{q[s](t ′ 1 , . . . , t ′ 1 )}, πn, s))))) consume ′ (h, h ′ , g, γ, π, A1 * A2, Q) ≡ consume ′ (h, h ′ , g, γ, π, A1, (λh ′′ , π ′ , s1• consume ′ (h, h ′′ , g, γ, π ′ , A2, (λh ′′′ , π ′′ , s2 • Q(h ′′′ , π ′′ , pair (s1, s2)))))) consume ′ (h, h ′ , g, γ, π, e1 = e2, Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • eval(h, g, γ, π1, e2, (λt2, π2• (π2 ⊢ t1 = t2) ∧ Q(h ′ , π2))))) consume ′ (h, h ′ , g, γ, π, s, untouched(A), Q) ≡ consume ′ (h, h, h, γ, π, A, (λ , , s1 • consume ′ (g, g, g, γ, π, A, (λ , , s2• (π ⊢ s1 = s2) ∧ Q(h ′ , π)))))
Fig. 5. Consumption of assertions.

Symbolic execution of statements exec(h, g, γ, π, s, Q) (Figure 6) symbolically executes statement s in symbolic state (h, g, γ, π) and passes a potentially updated heap, store and path condition to the continuation Q. More specifically, a memory allocation x := cons(e from the symbolic state and produces q's body with the snapshot of the removed chunk; if no such chunk exists, symbolic execution fails. Finally, a close statement close q(e 1 , . . . , e n ); consumes q's body and replaces the consumed chunks with a predicate chunk for q. The snapshot obtained by consuming q's body is used as the snapshot of this new heap chunk.

Valid Program

We say that a mutator function is valid (Definition 2) if after producing the precondition for arbitrary values of the parameters and executing the mutator's body in the resulting state, consumption of the postcondition succeeds and the symbolic heap is empty. A pure function is valid (Definition 3) if evaluation of its body does not fail in the symbolic state resulting from producing the precondition for arbitrary values of the parameters. A predicate is valid (Definition 4) if production of its body does not fail for arbitrary parameters. Finally, the main routine is valid (Definition 5) if its symbolic execution succeeds in an empty heap, pre-state heap, store and path condition and the resulting heap is empty. A program is valid if all functions and the main routine are valid. The program of Figure 2 is valid.

Definition 2. A mutator function func f (x 1 , . . . , x n ) requires A 1 ; ensures A 2 ; { s; return e; } is valid if the following holds: let (t 1 , . . . , t n ) = (fresh, . . . , fresh) in produce(∅, ∅, {(x 1 , t 1 ), . . . , (x n , t n )}, ∅, fresh, A 1 , (λh, π• exec(h, h, {(x 1 , t 1 ), . . . , (x n , t n )}, π, s, (λh ′ , γ, π ′ • eval(h ′ , h, γ, π ′ , e, (λt, π ′′ • consume(h ′ , h, {(x 1 , t 1 ), . . . , (x n , t n ), (result, t)}, π ′′ , A 2 , (λh ′′ , , • h ′′ = ∅))))))))
exec(h, g, γ, π, x := cons(e1, . . . , en); , Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • . . . eval(h, g, γ, πn-1, en, (λtn, πn

• let l = fresh in Q(h ⊎ {acc[t1](l), . . . acc[tn](l + n -1)}, γ[x → l], πn)))))
exec(h, g, γ, π, x := e; , Q) ≡ eval(h, g, γ, π, e, (λt, π1

• Q(h, γ[x → t], π1))) exec(h, g, γ, π, [e1] := e2; , Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • eval(h, g, γ, π1, e2, (λt2, π2• let matches = {acc[s](t ′ 1 ) | π2 ⊢ t1 = t ′ 1 } in ∃acc[s](t ′ 1 ) ∈ matches • Q(h -{acc[s](t ′ 1 )} ⊎ {acc[t2](t1)}, γ, π2)))))
exec(h, g, γ, π, x := f (e1, . . . , en), Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • . . . eval(h, g, γ, πn-1, en, (λtn, πn• consume(h, g, {(x1, t1), . . . , (xn, tn)}, πn, precondition(f ), (λh

′ , π ′ , • let (s, r) = (fresh, fresh) in produce(h ′ , h, {(x1, t1), . . . , (xn, tn), (result, r)}, π ′ , s, postcondition(f ), (λh ′′ , π ′′ • Q(h ′′ , γ[x → r], π ′′ ))))))))) exec(h, g, γ, π, free e; , Q) ≡ eval(h, g, γ, π, e, (λt, π ′
• let matches = {acc[s](t ′ ) | π ′ ⊢ t = t ′ } in ∃acc[s](t ′ ) ∈ matches • Q(h -{acc[s](t ′ )}, γ, π ′ )))
exec(h, g, γ, π, assert e1 = e2; , Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • eval(h, g, γ, π1, e2, (λt2, π2•

(π2 ⊢ t1 = t2) ∧ Q(h, γ, π2))))) exec(h, g, γ, π, if (e1 = e2) { s1 } else { s2 }, Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • eval(h, g, γ, π1, e2, (λt2, π2• exec(h, g, γ, π2 ∪ {t1 = t2}, s1, Q) ∧ exec(h, g, γ, π2 ∪ {t1 = t2}, s2, Q)
exec(h, g, γ, π, open q(e1, . . . , en); , Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • . . . eval(h, g, γ, πn-1, en, (λtn, πn• consume(h, g, γ, πn, q(e1, . . . , en), (λh ′ , π ′ , s• produce(h ′ , g, {(x1, t1), . . . , (xn, tn)}, π, s, definition(q), (λh

′′ , π ′′ • Q(h ′′ , γ, π ′′ )))))))))
exec(h, g, γ, π, close q(e1, . . . , en); , Q) ≡ eval(h, g, γ, π, e1, (λt1, π1 • . . . eval(h, g, γ, πn-1, en, (λtn, πn• consume(h, g, {(x1, t1), . . . , (xn, tn)}, πn, definition(q), (λh

′ , π ′ , s• Q(h ′ ⊎ {q[s](t1, . . . tn)}, γ, π ′ ))))))) exec(h, g, γ, π, s0 s, Q) ≡ exec(h, g, γ, π, s0, (λh ′ , γ ′ , π ′ • exec(h ′ , g, γ ′ , π ′ , s, Q)))
Fig. 6. Symbolic execution of statements.

exec(∅, ∅, ∅, ∅, s, (λh, , • h = ∅))
Pure Method Termination It is essential for the soundness of our approach that pure methods terminate. Verification therefore includes a phase that checks sufficient conditions for pure method termination. Specifically, it is checked for each pure method call in a pure method body that either (1) the callee is defined earlier in the program text, or (2) the call is in the body of an open expression, or

there is some symbolic heap chunk that is not consumed by the precondition of the call. This ensures that at each call, either the size of the symbolic heap decreases, or the derivation depth decreases (i.e. the number of close operations required to construct the heap from one that contains only field chunks), or the position in the program text decreases. Since the size and the derivation depth are always finite and a pure method cannot increase the size or the derivation depth of the symbolic heap, this ensures termination. Contrary to pure functions, mutator functions are not required to terminate.

Implementation and Experience

We have implemented the algorithm described in Section 3 in a tool. The source code (F#), binaries and a number of examples are available from the author's website http://www.cs.kuleuven.be/ ~jans/speccheck. Instead of the C-like language used in the paper, the tool supports a larger assertion language (e.g. conditional assertions) for a small subset of C#. To check whether a first-order formula is derivable from the path condition, we use the Z3 SMT solver [START_REF] De | Z3: An efficient SMT solver[END_REF]. Our verifier prototype has been used to verify a number of small programming patterns, including aggregate objects and iterator. These programs together with their verification times are shown in Table 1. To help developers diagnose verification errors, our verifier includes a symbolic debugger (shown in Figure 7). When verification fails, the developer can inspect the components of the symbolic states encountered during symbolic execution on the path to the failure.

Related Work

Separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] extends Hoare logic with three new assertions: emp, separating conjunction and points-to. Our assertion acc(e) is similar to separation logic's points-to assertion e → , which denotes that the current thread has permission to access the memory at address e (without constraining the value at that address). The key difference between classical separation logic and our variant is that we allow expressions that are used inside assertions to depend on the heap. Examples of heap-dependent expressions include pointer dereferences and function invocations. Note that we do not claim that our variant has additional expressive power. Instead, the difference leads to a different style of writing specifications. More specifically, where we use pure methods to express the state of an object, classical separation logic relies on predicate parameters. For example, the contract of inc of Figure 2 would be written in separation logic as: requires cell (c, X); ensures cell (c, X + 1);. Here, X is a logical variable.

Berdine et al. [START_REF] Berdine | Symbolic execution with separation logic[END_REF] have proposed a symbolic execution-based verification algorithm for programs annotated with separation logic specifications and have implemented this algorithm for a small imperative language in Smallfoot. The algorithm described in Section 3 is a variant of the aforementioned algorithm. In particular, the idea of dividing the symbolic state in spatial and pure assertions (the symbolic heap and the path condition respectively) and the rules dealing with heap access, non-heap-dependent expressions and assertions are largely similar to those in [START_REF] Berdine | Symbolic execution with separation logic[END_REF]. The novel aspect of our approach is the treatment of pure methods and pointer dereferences inside assertions via snapshots. Smallfoot only supports a limited number of predicates, but the developer does not need to write open and close statements as the tool has hard-coded, built-in rules for reasoning about those predicates. jStar [START_REF] Distefano | jStar: Towards practical verification for Java[END_REF] and VeriFast [START_REF] Jacobs | The VeriFast program verifier[END_REF] extend the basic ideas of Berdine et al. to fullfledged programming languages like Java and C. While loop invariants must be provided by the developer in our approach, jStar infers certain loop invariants automatically, provided the developer inputs the necessary abstraction rules. Using an SMT solver [START_REF] De | Z3: An efficient SMT solver[END_REF] for discharging pure queries and supporting symbolic debugging via an IDE that shows the components of the symbolic state are ideas taken from VeriFast.

As an alternative to the Smallfoot's symbolic execution-based verification algorithm, Leino and Müller [START_REF] K. Rustan | A basis for verifying multi-threaded programs[END_REF] and Smans et al. [START_REF] Smans | Implicit dynamic frames: Combining dynamic frames and separation logic[END_REF] have proposed an approach based on verification condition generation and automated theorem proving for a variant of separation logic. However, experience has shown that approaches based on verification condition generation and automated theorem proving in general, and [START_REF] K. Rustan | A basis for verifying multi-threaded programs[END_REF][START_REF] Smans | Implicit dynamic frames: Combining dynamic frames and separation logic[END_REF] in particular, have 3 disadvantages: (1) they are slow, (2) they are unpredictable, as small changes in the specification can have a significant impact on verification time and (3) verification errors are hard to diagnose, as it is hard to determine whether the specification is flawed or whether the theorem prover is unable to prove a particular part of the verification condition. As the experiments with our verifier prototype indicate, verification times are consistently low. For example, even if we increase the number of intermediate statements in the main routine of Figure 2, the verification time only increases marginally. The main reason why verification is fast is that we reason about the heap outside of the theorem prover, and hence do not need to send quantifier-heavy formulas (in particular quantifiers about the heap) to the automated prover. These experiments thus confirm earlier results with similar algorithms [START_REF] Berdine | Symbolic execution with separation logic[END_REF][START_REF] Distefano | jStar: Towards practical verification for Java[END_REF][START_REF] Jacobs | The VeriFast program verifier[END_REF]. Moreover, the developer can diagnose verification errors by inspecting the symbolic states on the path to the failure. A disadvantage of the approach presented in this paper with respect to [START_REF] K. Rustan | A basis for verifying multi-threaded programs[END_REF][START_REF] Smans | Implicit dynamic frames: Combining dynamic frames and separation logic[END_REF] is that non-separating conjunction is not supported.

Reasoning about method calls in specifications and framing their return values in particular was posed as a challenge for verification by Leavens, Leino and Müller [START_REF] Gary | Specification and verification challenges for sequential object-oriented programs[END_REF]. In the context of approaches based on verification condition generation and automated theorem proving, researchers have attacked well-formedness of pure method specifications [START_REF] Rudich | Checking well-formedness of pure-method specifications[END_REF][START_REF] K. Rustan | Practical reasoning about invocations and implementations of pure methods[END_REF], framing of return values [START_REF] Jacobs | Inspector methods for state abstraction[END_REF][START_REF] Darvas | Practical reasoning about invocations and implementations of pure methods[END_REF][START_REF] Smans | Automatic verification of java programs with dynamic frames[END_REF] and allowing certain side effects in pure methods [START_REF] Darvas | Reasoning about method calls in interface specifications[END_REF][START_REF] Darvas | Practical reasoning about invocations and implementations of pure methods[END_REF]. The approach proposed in this paper is similar to existing techniques in the sense that we also encode pure methods as functions and invocations of pure methods as function applications. Moreover, the idea of using snapshots is similar to the snapshots used in [START_REF] Jacobs | Inspector methods for state abstraction[END_REF][START_REF] Darvas | Practical reasoning about invocations and implementations of pure methods[END_REF]. However, to the best of our knowledge, this is the first paper that discusses the use of pure methods and framing of their return values in the context of separation logic (and in the context of its symbolic execution-based verification algorithm).

Conclusion

In this paper, we combined the expressive power of separation logic with the programmer-friendly notation of specification languages such as JML where heap-dependent expressions can be used in annotations. We proposed an algorithm to support mechanized checking for this variant of separation logic and implemented this algorithm in a tool.

Fig. 1 .

 1 Fig.1. A C-like language with side effect-free, heap-dependent expressions and separation logic annotations.

  predicate cell (c) = acc(c); pure func get(c) requires cell (c); { return open cell (c) in [c]; } func create cell () requires true; ensures cell (result) * get(result) = 0; { c := cons(0); close cell (c); return c; } func inc(c) requires cell (c); ensures cell (c) * get(c) = old(get(c)) + 1; { open cell (c); [c] := [c] + 1; close cell (c); return 0; } func copy(c, d) requires cell (c) * cell (d); ensures cell (c) * cell (d) * get(c) = get(d) * untouched(cell (d)); { open cell (c); [c] := get(d); close cell (c); return 0; } func dispose(c) requires cell (c); ensures true; { open cell (c); free(c); } c1 := create cell (); inc(c1); c2 := create cell (); inc(c2); assert get(c1) = 1; dispose(c1); dispose(c2);

Fig. 2 .

 2 Fig. 2. An annotated program written in the language of Figure 1. Annotations are highlighted by a gray background.

Table 1 .

 1 Programs verified using the verifier prototype together with the verification time (seconds). The experiments were executed on a standard desktop machine with a 2.66 Ghz processor and 4 GB of RAM running Windows Vista. cell50 is the similar to the main routine of Figure2, except that 50 intermediate cells are created and updated instead of 1.

Fig. 7 .

 7 Fig. 7. A screenshot of the verifier prototype. Developers can use the symbolic debugger in the IDE to diagnose verification errors and inspect the symbolic state at each program point. The box on the right of the screen contains a list of symbolic states encountered during symbolic execution. The boxes at the bottom of the screen show the symbolic state (from left to right: the symbolic heap, the path condition and the symbolic store) at a particular program point.

  Definition 1. A program is well-formed if all of the following hold:

	-Predicate, mutator function and pure function names are unique within the
	program. Parameter names are unique within a declaration.
	-The free variables of a function's body and contract are the function pa-
	rameters. Postconditions can additionally mention the variable result. The
	free variables of a predicate's body are the predicate's parameters. The main
	routine has no free variables.
	-The program only mentions functions and predicates declared in the program
	text. The number of actual arguments in a function call or predicate assertion
	is equal to the number of formal parameters in the corresponding declaration.
	-Old expressions and untouched assertions only appear in postconditions.

  1 , . . . , e n ); is modeled by creating a fresh term representing the address of the newly allocated memory. The heap is extended with n new memory locations starting at address l containing the terms t 1 to t n . The variable x is modified to l. A variable update x := e; modifies the value of the variable x in the symbolic store γ to the symbolic value of e. A heap update [e 1 ] = e 2 ; is allowed only if the symbolic heap contains a chunk that matches acc[ ](t 1 ). If such a match exists, that heap chunk's snapshot is changed to t 2 ; otherwise, symbolic execution fails. Symbolic execution of a mutator call x := f (e 1 , . . . , e n ); consists of consuming f 's precondition and producing f 's postcondition afterwards. Note that a fresh term is used as the snapshot for producing the postcondition. A free statement free e; is allowed only if the heap contains a chunk matching acc[ ](t). If it does, then that chunk is removed from the heap; otherwise, symbolic execution fails. Note that the chunks produced by cons(e 1 , . . . , e n ) need to be freed separately. As assert statement assert e 1 = e 2 ; fails if the values of e 1 and e 2 are not provably equal; otherwise, the assert statement is equivalent to skip. An if-then-else statement if (e 1 = e 2 ) { s 1 } else { s 2 } splits symbolic execution into two branches. An open statement open q(e 1 , . . . , e

n ); removes a chunk matching q[ ](t 1 , . . . , t n )

  Definition 3. A pure function pure func p(x 1 , . . . , x n ) requires A; { return e; } is valid if the following holds: let (t 1 , . . . , t n ) = (fresh, . . . , fresh) in produce(∅, ∅, {(x 1 , t 1 ), . . . , (x n , t n )}, ∅, fresh, A, (λh, π• eval(h, h, {(x 1 , t 1 ), . . . , (x n , t n )}, π, e, (λ , • true)))) ∅, {(x 1 , fresh), . . . , (x n , fresh)}, ∅, fresh, A, (λh, π • true)) Definition 5. A main routine s is valid if the following holds:

	Definition 4. A predicate
	predicate q(x 1 , . . . , x n ) = A;
	is valid if the following holds:
	produce(∅,


Jean Bresson
email: jean.bresson@ircam.fr

Reactive Visual Programs for Computer-Aided Music Composition

We present a new framework for reactive programming in OpenMusic, a visual programming language dedicated to computer-aided music composition. We highlight some characteristics of the programming and computation paradigms, and describe the implementation of a hybrid system merging demanddriven and event-driven evaluation models in this environment.

I. INTRODUCTION

Numerous computer systems for music composition have been designed as end-user programming languages. Computeraided composition environments today integrate flexible tools that allow composers to create music and to develop creative processes embedding algorithmic approaches, musical notation, graphical representations, i/o devices and communication in (visual) programs and programming languages [1].

In this paper we present a new framework for reactive programming in the OpenMusic computer-aided composition environment. After a brief presentation of OpenMusic (Section II), we will single out some specific aspects of this environment that bear important comparisons with other musical systems (Section III). We describe the implementation of a model merging demand-driven and event-driven evaluations in OpenMusic (Section IV), and discuss a number of possible applications (Section V). II. OPENMUSIC OpenMusic (OM) is a visual programming environment dedicated to music composition. The visual language is based on Lisp and extended with musical tools, data structures and editors [2][3]. This environment is used by composers worldwide and has contributed to numerous compositional projects and pieces from the contemporary music repertoire [4].

Visual programs in OM are made of boxes and connections: the user/programmer incrementally builds and evaluates directed acyclic graphs representing functional expressions.

Fig. 1 shows and example of an OM visual program. Each box in this program represents a function,1 a value or an object generator/container. [START_REF] Bresson | Visual Lisp/CLOS Programming in OpenMusic[END_REF] Inlets, at the top of the boxes, represent the inputs or arguments of the functions, and outlets, at the bottom of the boxes, correspond to returned value(s).

OM implements a demand-driven evaluation model: the nodes in the visual program graph are computed on user request, depending on the values he/she wishes to calculate or update (see Fig. 2a). Typically in Fig. 1, the user would evaluate the boxes RHYTHM, PITCHES SEQ or other downstream Evaluations, data input and rendering are generally interleaved as part of the composers' programming work-flow. Intermediate values can be edited using graphical editors, and locked in order to prevent reinitializations on future updates (locked boxes behave as terminal nodes in the call graph).

III. COMPUTATION MODELS IN MUSIC PROGRAMMING

SYSTEMS Among the different computer tools proposed to musicians today, an important distinction exists between "deferred-time" and "real-time" systems. These two approaches correspond to different ways of using computer systems for music: on the one hand, the symbolic manipulation of complex and structured musical data involved in the composition of a piece of music (scores, but also sounds or other types of data), and on the other hand, real-time audio processing and live interaction in concerts or performance contexts.

Executions in real-time musical systems are reactive processes driven by internal clocks, external events, data streams or signals that are processed through data-flow graphs. [START_REF] Assayag | Computer Assisted Composition at IRCAM: From PatchWork to OpenMusic[END_REF] In these systems music is produced "on the fly" by the program (each step of the program run generates a bit of music: an event, a sequence of audio samples, etc.). Therefore, the temporal dimension in the musical structures is practically merged with the "run-time" that flows during computation, which limits the possibility to "compose" with musical time. [START_REF] Agon | The OM Composer's Book (2 volumes)[END_REF] In contrast, compositional systems like OpenMusic generate "off-line" musical data in a deferred time context. If these systems are interactive (in the sense that they include user interactions), the programs created by the user are transformational: they process inputs, produce an output and terminate. [START_REF] Puckette | Combining Event and Signal Processing in the Max Graphical Programming Environment[END_REF] The output musical structures (scores, sounds, etc.) are played, read or interpreted by a performer or sequenced/rendered at a later stage. Such systems therefore make a distinction between computation time and musical time: the musical result is produced when the overall process is over, and its temporal structure is independent from the "run time" of the program. This paradigm allows for the formalization and generation of more sophisticated musical structures, without time-related restrictions or constraints (e.g. limitations of the accessible time domain, or constraints on complexity when results are required within strict time delays).

The deferred-time paradigm also have a number of drawbacks. While advantageous in its full and precise control over program execution, it can be impractical in that it forces frequent explicit updates after modifications or data input. The transformational paradigm of OM's model also has the disadvantage that it tends to isolate compositional processes from interactions with the external environment.

IV. REACTIVE VISUAL PROGRAMS IN OM

In a recent paper [8], we have proposed an extended semantics of OM merging off-line/demand-driven and reactive/eventdriven evaluation models (see Fig. 2). In this new situation, events or changes that occur in specific boxes in the visual programs propagate and update downstream branches and boxes, thus introducing more interactive aspects in compositional processes. At the moment, we consider the first-order functional graph only, that is, the "top-level" graphical elements of the visual programs. The implementation of this system can be relatively straightforward but needs to respect a number of constraints. Most importantly, we view reactivity as an optional and local feature and so this new functionality must not interfere with the environment's pre-existing semantics and behaviour. A number of features and concepts are added to the visual language for this purpose, that we list in this section.

A G E F B D C (a) A G E F B D C (b)
1) Active Boxes: In order to define reactive chains in the functional graphs, there is a new attribute of the OM boxes that determines their reactive status. Reactivity can be switched on and off by the user with a keyboard short-cut (the frame of the box is highlighted so that reactive objects are easily distinguishable from non-reactive ones). A reactive box systematically registers boxes downstream from it, i.e. following boxes that would use its value as an argument, and eventually propagate updates.

2) Events: Events are actions or changes on a box that are likely to require an update of other boxes in order to restore the consistency of functional relations in the program. Events can occur for instance with user actions such as the re-evaluation of a box yielding a new value (as in the standard evaluation model), the modification of a "value" box or of a box input, or specific editing actions in object editors that are validated and applied to the associated box. Events can also come from external processes or interruptions caught by the system.

3) Updates: Events are propagated and update the box descendants through a notification mechanism. A notification starts at an event (that is, a modification of a reactive box value), and is propagated to its descendants by a depth-first traversal of the visual program graph following the output connections. Every reactive descendant in turn propagates the notification. When a terminal box is reached (a box with no direct reactive descendent), this box is evaluated following the standard OM demand-driven model, hence respecting the existing scheduling strategy and semantics for program executions.

The box at the origin of the event is temporarily "locked" during the process, so that it is not re-evaluated as part of the update. Notified boxes in this process are also marked during the propagation, in order to avoid multiple visits to the same sections of the graph.

In this system, events are ordered upon occurrence and are handled asynchronously in a single thread. Every incoming event triggers an update and the next one is processed when the previous update terminates. This choice in event-handling simplifies the update process and is acceptable in both compositional contexts and applications.

This process successfully implements first-order reactive visual programs in OM. It has the advantages that it does not overload programming tasks and is completely transparent and conservative with respect to the initial language design.

V. EXTENSIONS AND APPLICATIONS

The reactive mechanism implemented in OM performs automatic computations and provides direct feedback for the different user/programmer actions. In so doing, it alters programming practices and needs in the environment and enables a variety of new applications. We provide a number of examples below.

A. Interactive Widgets and Components

The reactive mechanism facilitates experimentation with input values and, in certain situations, can be useful when combined with OM programs' special interface components such as buttons, list/menu selectors, sliders, etc. The insertion of an event after the standard activation procedure of an interactive component makes it handy to use at setting the values for the inputs of a visual program. Fig. 3 shows an example of a melody calculated from a curve, whose values are scaled in a pitch range determined by two sliders. The reactive chain between the sliders and the score box makes this value range controllable interactively with immediate feedback. It is important to note that immediate reactivity is not always desirable, hence the importance of local and optional control of the reactive mechanism. OM fosters an experimental approach, allowing for visual programs to be constructed incrementally through a process of trial and error. Sometimes boxes can be temporarily connected in a certain way by mistake, or for different purposes than immediate evaluation. Additionally, evaluations can sometimes take a long time to complete (e.g. in complex optimization problems, or in programs involving large data structures or high precision signal processing). In these cases of computationally-intensive processes, the visual program is usually run only once at the end of its construction, and the use of reactive sliders such as shown in the previous example is not an adequate means for triggering executions.

B. Communication with External Systems

The reactive framework creates new possibilities for communication between the computer-aided composition environment and other applications, and more generally with its external context. Networked inter-application communication is supported via MIDI or UDP/OSC [START_REF] Agostini | Bach: An Environment for Computer-Aided Composition in Max[END_REF] and available in the visual programs respectively through the MIDI-in/out and OSC-receive/send boxes.

When activated, MIDI or OSC "receive boxes" run a server thread receiving incoming messages on a specified port. A reactive behaviour (event) is added to these boxes, which updates their value and triggers a notification when a message is received. Visual programs containing active receive boxes hence become reactive to such events or messages sent by external applications, input devices or instruments that communicate with these protocols.

C. Data Collection

Reactive boxes and notifications handle "instantaneous" data and events. In order to integrate compositional processes, these data generally need to be gathered in more complex data sets and mapped to time structures. A specific box (coll) has been created for this purpose, which instantiates a local storage for dynamic data collection in OM visual programs.

The coll box constitutes a special case in the update mechanism. It behaves as an intermediate step where notification temporarily stops and inputs are evaluated. The box has three inputs: when the first one (labelled data-in) collects some data, this data is added into a list that constitutes the coll "memory". The second input (push), makes coll behaving as a standard reactive box, propagating the notification through its descendants. The third input (init) reinitializes the memory. When it is evaluated (typically, after the propagation has triggered an evaluation), coll returns the current contents of its memory as a list of all previous collected data.

Coll can be associated to OSC or MIDI receive boxes to create reactive programs in OM that structure and process live inputs from real-time systems, players or instruments. Fig. 4 shows an OM program collecting and processing data from the Max software using OSC-receive and coll. In contrast to Fig. 1, evaluations here are driven by incoming messages in OSCreceive. The growing contents of the coll memory is converted into a data structure (a score) that can be further processed in the visual programming environment.

D. Handling Groups and Time in Data Collection

It is frequent in communication frameworks that several messages need to be considered as being simultaneous or otherwise "grouped" together. (If the messages are musical notes then this idea would correspond to the concept of a chord.) However, it is very unlikely that two events belonging to the same group would be sent and received at exactly the same time (and even so, they would not be handled simultaneously by the system). Time-tagging and/or structuring events provides a solution for sender applications to deal with this situation [10], but all events are not necessarily formatted so.

When no bundle or time-tagging is present in the communication protocol (e.g at receiving simple UDP or MIDI messages), internal timing can be used to gather the collected data according to specified time intervals. The group-in box implements this behaviour: it has one input collecting data (similar to the coll input) and a second input setting a time frame during which events are gathered and considered as part of the same data set. This box generates a slight delay and propagates collected data at once after this delay is over. The timed-coll object also extends coll with the groupin behaviour and gathers the items collected during a time frame into separate data chunks. Depending on the timing of incoming events, the result in Fig. 4 using timed-coll would be a list of pitch lists, corresponding to a sequence of chords in the score (see Fig. 5).

E. Event-Driven Conception of the Visual Programs

Reactive applications such as the one in Fig. 4 tend to emulate and orient the conception of the visual programs towards the data-driven paradigm (Fig. 2b), where the propagation of notifications needs to be controlled in the same way as evaluation. (The coll mechanism, for instance, can be seen as the data-driven counterpart to the collect primitive in standard Lisp or OM loops).

Several tools inspired by reactive systems like Max are being added to the OM reactive framework to help it expand beyond its original paradigm. One such tool is route, a utility that filters notifications using on a set of tests performed on its input. Route is also a particular case in the update mechanism as it requires stopping the notification and evaluating inputs before selecting where to propagate an update.

Other "data-driven" utilities include for instance an internal send/receive mechanism, also inspired from the Max send and receive tools, allowing to propagate notifications and updates in the visual programs without passing through the whole path of intermediate connections.

VI. CONCLUSION

In this paper we have summarized the significance of deferred-time computation in computer-aided composition systems and outlined a reactive framework in OM where this characteristic is combined with interactive processes. The reactive extension of OM introduces a new conception of the computer-aided composition framework and of its connection to the external context. Visual programs and compositional processes are built and run interactively, but also "live" on their own and can be driven by external processes and interactions. The generated musical structures can in turn be re-injected into a "real" time flow, either via networking or direct rendering, as a response to an event in the reactive system. This kind of reactive loop, in which real-time processing leaves space for advanced formal/compositional computation, opens interesting perspectives for enhanced musical expressiveness in interactive situations.

Our first experiments with the system show that OM users can easily shift to the reactive paradigm and reuse their tools and libraries in this new computational framework.

The main questions raised by this project are now related to the notions of time involved in reactive musical systems: how to deal with the asynchronous occurrence of events; with the relations between the duration of computations, the real time of interactions, and the duration of the computed time structures. We have only briefly touched on these questions in this paper, and plan to address them in more detail in future works.

OpenMusic is a free and open-source software. [START_REF] Harel | On the Development of Reactive Systems[END_REF] The reactive extension can be loaded dynamically as an external library, and shall be included as a native feature in future versions.

Fig. 1 :

 1 Fig. 1: Example of an OpenMusic visual program.

Fig. 2 :

 2 Fig. 2: Control flow in demand-driven vs. data/event-driven evaluation. (a) Demand-driven: the evaluation of C propagates up in the graph to request input values. (b) Data-driven: G activates an execution that propagates down to C.

Fig. 3 :

 3 Fig. 3: Interactive control of input values in a reactive visual program using slider boxes. The two sliders (MIN, MAX), omscale and SEQUENCE are reactive boxes.

Fig. 4 :

 4 Fig. 4: Reception, collection and processing of incoming data. The Max program (window on the left) sends a "note" message via UDP every time the user clicks on the piano keyboard widget. The OM program (at the right) collects information from the messages into the coll box. At every received data the push (second input of coll) also receives a notification and triggers an update of the downstream part of the program.

Fig. 5 :

 5 Fig. 5: Grouping incoming data. A delay of 100ms is set to gather and transmit or collect notes as chords.

Functions can written in Lisp or graphically as internal visual programs.

Object boxes are actually class constructors or factories, as usually found in object-oriented systems.

Max[START_REF] Puckette | Combining Event and Signal Processing in the Max Graphical Programming Environment[END_REF] is a popular visual language in this category. We will use it to illustrate inter-application communication processes in Section V (Fig.

4).

Recent works in real-time musical environments such as bach[START_REF] Agostini | Bach: An Environment for Computer-Aided Composition in Max[END_REF] shall be mentioned here, for they bring higher-level musical constructs and processes in this constrained temporal paradigm. bach can be seen as a symmetrical counterpart to the present work, for it aims at bridging computer-aided composition and real-time/reactive visual programming frameworks, from the real-time systems perspective.

See[START_REF] Harel | On the Development of Reactive Systems[END_REF] for a discussion about transformational vs. reactive systems.

OSC is a format for UDP packets created for musical applications[START_REF] Wright | Open Sound Control: an enabling technology for musical networking[END_REF].

http://repmus.ircam.fr/openmusic/

ACKNOWLEDGEMENTS

This work is done with the support of the French National Research Agency projects with reference ANR-13-JS02-0004-01 and ANR-12-CORD-0009.