C Langrée
email: langreec@coria.fr

E Franquet

J Reveillon

G Lecocq

F X Demoulin

CFD Simulation of an Unconfined Vapor Cloud Explosion through obstacles using OpenFoam R

Keywords: hazards, industrial explosions, CFD, premixed combustion

In this work, numerical simulations are carried out to characterize the impact of obstacles on flame propagation velocity to properly assess the consequences of Unconfined Vapor Cloud Explosions (UVCE). Within this scope, an UVCE within a congested environment is simulated using RANS modeling of the turbulence. Combustion phenomena are characterized through the progress variable transport equation. The simulation is done with the open source library OpenFoam R . Numerical results are compared with data from the INERIS and GDF-SUEZ experimental campaign EXJET (hydrogen-air and methane-air explosions).

Introduction

Unconfined Vapor Cloud Explosion (UVCE) is one of the most devastating industrial accidents possible (J. [START_REF] Holzmann | Formalisation du savoir et des outils dans le domaine des risques majeurs (eat-dra-76) les explosions non confinées de gaz et de vapeursω uvce[END_REF]). The loss of containment of a flammable product (e.g. methane or hydrogen) can lead to the formation of a flammable cloud all across the plant. The resulting mixture can be lit by any energy source within the cloud (e.g. sparkles, hot surfaces). The propagation of the flame front within the cloud can cause damaging pressure effects in close and long range. In order to assess these damages, CFD can be used, in parallel with widely used phenomenological tools. The open source code OpenFoam R has already been used for such purpose [START_REF] Bauwens | Vented explosion overpressures from combustion of hydrogen and hydrocarbon mixtures[END_REF], [START_REF] Ghasemi | Rans simulation of methane-air burner using local extinction approach within eddy dissipation concept by openfoam[END_REF], [START_REF] Rao | Effects of congestion and confining walls on turbulent deflagrations in a hydrogen storage facility-part 2: Numerical study[END_REF]). The global aim of this study is to improve numerical methods for CFD simulation of industrial UVCE.

Hazardous consequences of UVCE are mainly caused by the over-pressure generated by the propagation of the flame front. In deflagration cases, this over-pressure is directly linked to the flame front propagation speed (J. [START_REF] Holzmann | Formalisation du savoir et des outils dans le domaine des risques majeurs (eat-dra-76) les explosions non confinées de gaz et de vapeursω uvce[END_REF]). In an industrial configuration, the flame front is impacted by the various obstacles in its way (e.g. pipes, walls). One of the consequences of the presence of obstacles is an acceleration of the flame front [START_REF] Moen | Flame acceleration due to turbulence produced by obstacles[END_REF], [START_REF] Moen | Pressure development due to turbulent flame propagation in large-scale methaneair explosions[END_REF]) and, consequently, many experiments has been conducted to evaluate this effect. The EXJET campaign (INERIS, GDF-SUEZ) has been set to study experimentally the effect of an obstacle module on the propagation of a flame front in many configurations (steady flammable mix, methane-air jet, hydrogen-air jet).

Description of the experimental work

The experimental work considered here has been carried out by INERIS and GDF-SUEZ [START_REF] Sail | Review of knowledge and recent works on the influence of initial turbulence in methane explosion[END_REF]). The aim of the experiment was to study methane jet explosion in a congested environment. The congestion module was a medium size (3m×1m×0.45m) obstacle module, consisting of 296 steel tubes of 2cm diameter. In the framework of the EXJET experimental setup, several experiments have been carried out : methane jet dispersion within the module (without ignition), methane jet ignition within the module, and ignition of a steady methane-air mix. The steady methane-air mix ignition configuration has been simulated with OpenFoam R in this study.

To assess the pressure variations, several pressure probes are positioned in and around the obstacle module as in Fig. 1. The pressure signals from those probes will be compared to the pressures signals from virtual probes of the numerical simulation. Moreover, pictures of the experiment will be post-process to obtained experimental flame position data. In the configuration that interests us, a homogeneous stoichiometric methane-air mixture is spread within the obstacle module. The mixture is kept in the obstacle area by a plastic sheet supported by steel frames. Those plastic sheets will come off with the explosion. The flammable mix is ignited by an electrical ignition device (location 1 on Fig. 1) located inside an aluminium box (19cm×15cm×13cm) with an opening toward the congestion module.

3 Numerical study

Equations solved

With the solver XiFoam of OpenFoam R v7.0, the Weller b-Xi model [START_REF] Weller | Application of a flame-wrinkling les combustion model to a turbulent mixing layer[END_REF]) is used to model partially premixed combustion. Navier-Stokes equations (eqs. 1, 2) are solved as well as the energy equation (eq. 3).

∂ ρ ∂t + ∇.(ρ U) = 0 (1) ∂ ρ U ∂t + ∇.(ρ U U) = -∇.(ρ U U ) -∇p + ∇.(τ) (2) ∂ ρ h t ∂t + ∇.(ρ U h t ) + ∂ ρK ∂t + ∇.(ρ UK) + ∂ p ∂t + ∇.(α∇ h t ) = Q (3)
With K being the kinetic energy, α the thermal diffusivity, τ the viscous stress tensor and Q an external energy source term (in our case, Q = 0).

In order to model the combustion, a combustion regress variable "b" is defined (4).

b = T b -T T b -T u (4)
With T b the burnt gases temperature, and T u the unburnt temperature. A transport equation is solved for this regress variable ( 5) in order to model the propagation of the flame front.

∂ ρb ∂t + ∇.(ρ Ub) -∇.(α∇b) = -ρ u S u Ξ | ∇b | (5)
With Su the laminar flame speed, ρ u the unburnt gases density, and Ξ the flame wrinkling factor (turbulent and laminar flame speed ratio). This ratio is obtained algebraically (6).

Ξ = 1 + 2(1 -b)Ξ coe f f u Su R η (6)
With R η the Kolmogorov Reynolds number, u the sub-grid turbulence intensity and Ξ coe f f a model constant equal, in our case, to 0.62. And finally, to take into account the inhomogeneity of the mix, an equation for a mix variable f t is solved (7).

∂ ρ f t ∂t + ∇.(ρ U f t ) = ∇.(µ∇ f t ) (7)
With µ the dynamic viscosity. The effects of equivalence ratio inhomogeneity on the flame front propagation speed is taken into account by the S u term in the b equation with the Gulder flame speed correlation (8) [START_REF] Gulder | Correlations of laminar combustion data for alternative si engine fuels[END_REF]).

Su(T, p, φ ) = W φ η e -ξ (φ -σ ) ( T T 0 ) α ( p p 0 ) β (8)
With W , η, σ , α, β Weller model constant and φ , the equivalence ratio, being recovered from f t and ( Y air Y f uel ) sto , the stoichiometric air-fuel ratio .

φ = ( Y air Y f uel ) sto f t 1 -f t (9)
The ignition is managed via an OpenFoam R integrated module which generate, in a given duration, a spherical volume of burnt gases of a given radius, at a given location. The duration and radius of this ignition kernel has been tuned to the laminar flame speed of the mix.

The PIMPLE algorithm is used to solve the pressure-velocity coupling in XiFoam [START_REF] Holzmann | Formalisation du savoir et des outils dans le domaine des risques majeurs (eat-dra-76) les explosions non confinées de gaz et de vapeursω uvce[END_REF]). The equations modeling the effect of the combustion are included in the PIMLE loop.

Mesh, boundary condition and numerical schemes

The meshing process has been conducted with both SALOME and the OpenFoam R utilities blockMesh and snappyHexMesh. The domain consists of 836 296 cells and the minimum dx of a cell is 6.25 mm. The boundary of the numerical domain surrounding the obstacle module is at 2.5m distance of the module in the x and y direction and at 1.5m distance of the module in the z direction.

The boundary conditions to take into account for this simulation are : • the obstacle module • the ground • the ambiant air

The obstacle module and ground will be considered "wall" boundary condition whereas ambient air will be considered free outlet boundary condition. The boundary conditions used are given in Table 1. The different numerical schemes available in OpenFoam R are detailed in [START_REF] Moukalled | The Finite Volume Method in Computational Fluid Dynamics: An Advanced Introduction with OpenFOAM R and Matlab R[END_REF]). The schemes used in this simulation are given in Table 2.

Results and discussion

As we are willing to assess for the over-pressure effects of the UVCE, we will look at two aspects of it : the propagation speed of the flame front and the resulting over-pressure.

Flame speed

A first simulation has been done to check that the solver take into account the accelerating effect of the obstacles on the flame front. A flame front has been propagated in two cases, with and without an obstacle module. The same mesh and numerical schemes has been used for the two simulation.

Fig. 3: Flame front position in time with and without obstacles

Here we can see that the flame front positions diverged. An accelerating effect of the obstacle can be observed with XiFoam. We can explain that effect by the turbulent kinetic energy generated by the obstacles. In fact, the flame front propagation, by pushing the fresh gases in front of it, generate a velocity flow normal to the flame surface. This flow, in presence of obstacles, will increase turbulent kinetic energy around those obstacles. This turbulent kinetic energy will, as we can see in (eq .6), increase the wrinkling factor and hence the flame propagation speed, as we can see in (eq. 5). The turbulent kinetic energy generation by the obstacles is illustrated in Fig. 4. There we can see that turbulent kinetic energy is generated around the obstacles crossed by the flame front. Finally, we can compare the experimental and numerical flame speed. We observe an acceleration of the experimental flame front during the whole experiment, starting propagating at 9 m/s until it attained a speed of roughly 25 m/s. In the numerical case however, we observe a constant flame speed of approximately 12 m/s. As we are in the same magnitude in term of flame propagation speed, we fail to reconstruct the accelerating behavior of the flame front within the obstacle module. The usage of a transport equation for Ξ in further work can be a lead toward reproducing this accelerating behavior. But when comparing the signals from two pressure probes (positioned along the y axis from the ignition point) Fig. 7, both experimental and numerical, we couldn't reproduce with precision the over-pressure wave. There we can see that at 0.28 cm from the ignition point, a 4.5 mmBar overpressure is obtained but the peak is obtained numerically at approximately 0.03sec in the numerical case, versus 0.1sec for the experimental case. However, with the over-pressure being "pushed" by the flame front, the phase between the two signal is likely to be induced by the different position of the experimental and numerical flame front. Now at 1.96m from the ignition point, the two over-pressure peaks are occurring approximately at the same time (0.16 sec), but the magnitude is not accurately reproduced. The numerical overpressure peak value is 1.75 mmBar and the experimental one being 6 mmBar. This difference may be explained by the flame speed difference when crossing the probe. In fact, at the moment where the flame crosses the probe at 1.96m from the ignition point, the experimental has already attained its max velocity of 25 m/s whereas the numerical one is still at the same speed of 12 m/s Fig. 5. The magnitude of the peak over-pressure is roughly the same (severals mBar), although the over-pressure is attenuated between the two probes for the numerical simulation(from 4.7 mBar to 1.8 mBar), and is enhanced in the experiment(from 4.5mBar to 6.0 mBar). This is probably explained by the acceleration of the experimental flame front Fig. 5 between the two probes, effectively generating more over-pressure in front of it. In this study, a methane-air explosion in a confined environment has been simulated. The explosion "at rest" case of the EXJET (INERIS GDF-SUEZ) as been taken to assess for the fidelity of the simulation with OpenFoam R . So far, several aspects of the simulation have shown good agreement with the experiment : The accelerating effect of the obstacles can be reproduced, and magnitude of both flame speed and over-pressure peaks are conserved. But the study fails to reproduce the accelerating behavior of the flame front and hence the over-pressure signals obtained numerically are not accurately reproducing the experimental ones.

The key to reproduce with fidelity the over-pressure signals (and more specifically, the over pressure peak values) is to capture with fidelity the flame propagation speed. Current works on the transport equation for Ξ are carried out to take care of that aspects. Results will be updated accordingly.

Fig. 1 :

 1 Fig. 1: Locations of the release orifice, pipes, igniter and pressure sensors used by INERIS and GDF SUEZ for methane jets within a 3D array of 20 mm diameter tubes (Sail et al. (2014)). Up : top view of the obstacle module ; Bottom : side view of the obstacle module.

Fig. 2 :

 2 Fig. 2: View of the calculation mesh (ParaView)

Fig. 4 :

 4 Fig. 4: Sectional view (z axis) of the flame front propagation (Paraview). Left : temperature (K), right : turbulent kinetic energy (m 2 .s -2 )

Fig. 5 :

 5 Fig. 5: Experimental and numerical flame front position from the ignition point in time

Fig. 6 :

 6 Fig. 6: Sectional view (x axis) of the flame front propagation at t = 0.2 sec (Paraview). Up : temperature (K), down : pressure (Pa)

  (a) Relative pressure at 0.28m from the ignition point (b) Relative pressure at 1.96m from the ignition point

Fig. 7 :

 7 Fig. 7: Relative pressure signal in time at 2 point on the y axis

Table 1 :

 1 Numerical simulation boundary conditions

	Variable	WallBC	AirBC
	U	fixedValue (0 0 0)	fluxCorrectedVelocity
	p	zeroGradient	totalPressure
	*	zeroGradient	zeroGradient

Table 2 :

 2 Simulation numerical schemes

	Variable	ddt	div	laplacian
	U/p/k	Euler backward	Upwind	Gauss linear corrected
	b/ft	Euler backward	Gauss linearlimited01	Gauss linear corrected
	*	Euler backward	Gauss linearlimited	Gauss linear corrected


Duncan Paul Attard
email: duncan.attard.01@um.edu.mt

Luca Aceto
email: luca.aceto@gssi.it

Antonis Achilleos
email: antonios@ru.is

Adrian Francalanza

Anna Ingólfsdóttir
email: annai@ru.is

Karoliina Lehtinen
email: lehtinen@lis-lab.fr

Antonis Id

Achilleos

Better Late Than Never or: Verifying Asynchronous Components at Runtime

Keywords: Runtime Verification, Instrumentation, Monitoring

come

Do You Want To Know A Secret

In the Cockaigne of software development, programs are verified using a smorgasbord of pre-deployment techniques, and executed only when their correctness is ascertained. Reality, however, tells a different story. Mainstream verification practices, including testing [START_REF] Myers | The Art of Software Testing[END_REF], only reveal the presence of errors [START_REF] Dijkstra | Chapter I: Notes on Structured Programming[END_REF]. Exhaustive approaches like model checking [START_REF] Jr | Model Checking[END_REF] are laborious to use, e.g. building effective program models is non-trivial, and known to suffer from state explosion problems [START_REF] Clarke | Model Checking and the State Explosion Problem[END_REF]. Other methods such as type systems [START_REF] Pierce | Types and Programming Languages[END_REF] are intentionally lightweight to prevent disrupting the software development lifecycle; this, in turn, limits their precision since type-based analyses occasionally rule out well-behaved programs. Present-day software poses even more challenges. Static verification often relies on having access to the program source code, which is not necessarily available when software is constructed from libraries or components subject to third-party restrictions. Moreover, modern applications are increasingly developed in decentralised fashion, where the constituent parts are not always known pre-deployment. This tends to increase both the complexity of software and the resources required to verify it, while at the same time, decreasing the time available to conduct its verification. Lately, with the availability of large data volumes, cutting-edge software components rely on machine learning to adapt their behaviour without the need to be explicitly programmed. Analysing these types of software artifacts statically is difficult, not least because their internal representation is notoriously hard to understand.

Although the proverbial correctness cake cannot be had and eaten, slices of it may still be savoured after the program has been deployed. In certain cases, post-deployment techniques such as Runtime Verification (RV) [START_REF] Bartocci | Introduction to Runtime Verification[END_REF][START_REF] Francalanza | A Foundation for Runtime Monitoring[END_REF] can be used instead of, or in tandem with, static techniques to increase correctness assurances about a program or System under Scrutiny (SuS). RV uses monitors-computational entities consisting of logically-distinct instrumentation and analysis units-to observe the execution of the SuS. Analysers, i.e., sequence recognisers [START_REF] Alpern | Recognizing Safety and Liveness[END_REF], are typically synthesised automatically from formal descriptions of correctness properties expressed in a specification logic.

When devising a RV tool, substantial effort is focussed on the specification language that is used to describe correctness properties, and the synthesis procedure which generates the analysis that runtime checks these properties [START_REF] Aceto | An Operational Guide to Monitorability with Applications to Regular Properties[END_REF][START_REF] Leucker | A Brief Account of Runtime Verification[END_REF][START_REF] Bartocci | Introduction to Runtime Verification[END_REF]. Arguably, less attention is given to the instrumentation aspect, particularly, how the SuS is equipped to run with monitors, and the manner in which the computation of the SuS is extracted and reported for analysis. There is no one-sizefits-all solution to these challenges. For instance, inline instrumentation-the de facto technique employed by state-of-the-art RV [START_REF] Bartocci | Introduction to Runtime Verification[END_REF][START_REF] Falcone | A Taxonomy for Classifying Runtime Verification Tools[END_REF]-relies on access to the program source or unobfuscated binary, thus obliging the RV monitors to be expressed in the same language as that of the SuS. The hallmark of a flexible RV tool is, therefore, its ability to support various instrumentation techniques to cater for the different scenarios where RV is used. The RV tool should also provide a common interface for describing what properties should be verified, agnostic of the underlying instrumentation mechanism dealing with the technicalities of how the verification is performed. This contributes to lowering the learning curve of the tool and facilitate its adoption.

This paper presents the RV tool detectEr that addresses the analysis and instrumentation aspects of runtime monitoring. Our tool targets asynchronous component systems. It automatically synthesises correct analyser code from properties expressed in terms of the monitorable safety fragment of the modal µ-calculus. Since the correctness of the synthesised analysers is studied in prior work (see [START_REF] Francalanza | Monitorability for the Hennessy-Milner Logic with Recursion[END_REF][START_REF] Aceto | Monitoring for silent actions[END_REF][START_REF] Aceto | Adventures in Monitorability: From Branching to Linear Time and Back Again[END_REF][START_REF] Attard | A Monitoring Tool for a Branching-Time Logic[END_REF]), our account elaborates on the usability and instrumentation aspects of the tool. detectEr, developed on top of the Erlang [START_REF] Armstrong | Programming Erlang: Software for a Concurrent World[END_REF][START_REF] Cesarini | Erlang Programming: A Concurrent Approach to Software Development[END_REF] ecosystem, supports three instrumentation methods to cater for different SuS set-ups:

Inline: targets programs written in the Erlang language; Outline: accommodates program binaries that are compiled for and run on the Erlang Virtual Machine (EVM), but whose source code is unavailable; (a) calc_server implementation in Erlang

Q0 Q1 Q2 Q3 Q4 S r v ? C lt , a d d , A 1 , A 2 S r v :C lt ! o k , A 1 + A 2 S r v ? C lt , m u l, A 1 , A 2 S r v :C lt ! o k , A 1 * A 2 Srv ? Clt ,stp Srv:Clt ! bye,Tot (b) Server-client interaction model
Fig. 1: Our calculator server and its abstraction in terms of symbolic actions

Offline: analyses recorded runs of programs that may execute outside the EVM.

We show how, from the same correctness specifications, detectEr is able to runtime monitor system components using these different instrumentation methods. The paper is structured as follows. Sec. 2 introduces our running example that captures the typical interaction between concurrent processes, along with useful properties one may wish to runtime check on such systems. Secs. 3 and 4 focus on the specification logic used by detectEr and how this is synthesised into executable analysis code. Sec. 5 summarises the role the instrumentation has with respect to the runtime analysis, and the mechanism detectEr employs to identify the SuS components in need of monitoring. Secs. 6-8 overview the three instrumentation methods mentioned above, while sec. 9 concludes.

A Day in the Life

We consider an idiomatic calculator server that handles client requests for arithmetic computation. Our server can be naturally expressed as an actor (process) [START_REF] Agha | A Foundation for Actor Computation[END_REF] that blocks, and waits for client requests sent as asynchronous messages. These messages are addressed to the server using its unique process ID (PID), and deposited in its mailbox that buffers multiple client requests. The server unblocks upon consuming a message from the mailbox. In our client-server protocol, messages contain the type of operation to be executed on the server, its arguments (if applicable), and the client PID to whom the corresponding server reply is addressed.

Our calculator server is implemented as the Erlang module, calc_server, in fig. 1a. The server logic is encapsulated in the function loop(Tot) that is forked to execute as an independent process by the launcher invoking start(), line 1. Processes in Erlang are forked via the built-in function spawn(), parametrised on line 1 by the module name, calc_server, the name of the function to spawn, loop, and the list of arguments accepted by loop, [0]. The server process reads messages from its mailbox (line 3), and pattern-matches against the three types of operations requested by clients, Clt: (i) addition (add) and multiplication (mul) requests carry the operands A 1 and A 2 , lines 4 and 8, and, (ii) stop (stp) requests that carry no arguments, line 12. Pattern variables Clt, A 1 and A 2 in fig. 1a are instantiated to concrete data in client request messages via pattern matching. Every request fulfilled by the server results in a corresponding reply that is sent to the PID of the client instantiated in variable Clt, lines 5, 9 and 13. Server replies carry the status tag, ok or bye, and the result of the requested operation. Parameter Tot of loop() is used by the server to track the number of client requests serviced, and is returned in reply to a stp request. The server loops on add and mul requests, incrementing Tot before recursing, lines 6 and 10; a stp request does not loop and terminates the server computation.

In the sequel, we focus on a system set-up consisting of one server and client to facilitate our exposition. The forked loop(Tot) function for some initial service count Tot induces a server runtime behaviour that can be abstractly described by the state transition model in fig. 1b. Transitions between the states of fig. 1b denote the computational steps that produce (visible) program events (e.g. event Srv:Clt !{bye , Tot} that carries the concrete payload values Srv , Clt and Tot). There are a number of correctness properties we would like such behaviour to observe. For instance, we do not control the value Tot that the server loop is launched with and, therefore, could require the invariant "The service request count returned on shutdown is never negative."

(P 1 )
Similarly, one would expect the safety properties "Replies are always sent to the client indicated in the request" (P 2 )

and "A request for adding two numbers always returns their sum" to hold, amongst others. The properties are data-dependent, which makes them hard to ascertain using static techniques such as type systems. Besides properties that reason on data, the implementation in fig. 1a is expected to comply with control properties, such as, "Client requests are never serviced more than once", (P 3 ) that describe the message exchanges between the server and client processes. All these properties are hard to ascertain without access to the source code.

I Want to Tell You

We overview the detectEr specification syntax, sHML [START_REF] Francalanza | On Verifying Hennessy-Milner Logic with Recursion at Runtime[END_REF][START_REF] Aceto | Determinizing Monitors for HML with Recursion[END_REF][START_REF] Aceto | On Runtime Enforcement via Suppressions[END_REF], which is the safety logical fragment of the modal µ-calculus [START_REF] Kozen | Results on the Propositional µ-Calculus[END_REF][START_REF] Larsen | Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion[END_REF], and show how a selection of the properties in sec. 2 can be formally specified in this logic.

The logic. Specifications in sHML are defined over the states of transition models (such as the one of fig. 1b), and are generated from the following grammar:

ϕ ∈ sHML ::= tt (truth) | ff (falsehood) | x (fix-point variable) | i∈I [pi,ci ]ϕi (conj. necessities) | max x.ϕ (max. fix-point)
sHML expresses recursive properties as maximal fix-point formulae maxx.ϕ, that bind free occurrences of x in ϕ. A central construct to sHML is the universal modal operator, [p,c]ϕ. To handle reasoning over event data, sHML modalities are augmented with symbolic actions [START_REF] Aceto | On Runtime Enforcement via Suppressions[END_REF], consisting of event patterns p ∈ Pat, and decidable constraints, c ∈ BExp. This is similar to how sets of actions are expressed in tools such as CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] and mCRL 2 [START_REF] Bunte | The mCRL2 Toolset for Analysing Concurrent Systems -Improvements in Expressivity and Usability[END_REF]. The pattern p contains data variables, A,B,... ∈ Var, that bind free data variables in c, along with any other free variables in constraints of the continuation ϕ. The pair (p,c) describes a concrete set of actions, a ∈ Act (i.e., program events). An action a is in this set when: (i) p matches the shape of a, and maps the variables in p to the payload data in a as the substitution σ, and (ii) the instantiated constraint cσ of p also holds. A state Q of the SuS (model) satisfies [p,c]ϕ if the following holds: whenever Q transitions to state Q with action a that is included in the set described by (p,c) with σ, then Q must satisfy the instantiated continuation formula ϕσ.

The logical variant [START_REF] Aceto | Determinizing Monitors for HML with Recursion[END_REF][START_REF] Aceto | On Runtime Enforcement via Suppressions[END_REF] we use for detectEr combines necessities and con-

junctions into one construct, i∈I [p i ,c i ]ϕ i , to denote [p 1 ,c 1 ]ϕ 1 ∧...∧[p n ,c n ]ϕ n , I ={1,.
..,n} being a finite index set. Conjunctions assume that every pair (p i ,c i ) describes a disjoint set of actions to facilitate the generation of deterministic monitors [START_REF] Francalanza | Consistently-Detecting Monitors[END_REF][START_REF] Francalanza | A Theory of Monitors[END_REF]. detectEr supports the five action patterns of tbl. 1 that capture the lifecycle of, and interactions between the processes of the SuS. A fork action is exhibited by a process when it creates a child process; its dual, init, is exhibited by the corresponding child upon initialisation. Process exit actions signal termination, while send and recv describe interaction. The labelled state transition model of fig. 1b uses the actions send and recv from tbl. 1.

Example 1. Recall the SuS behaviour in fig. 1b. Formula ϕ 0 with symbolic action (p,c) describes a property requiring that a state does not exhibit an output event that consists of Ack ,Tot , acknowledged with bye and a negative total, Tot.

[ pattern p Srv:Clt ! Ack ,Tot , constraint c Ack = bye ∧ Tot < 0 ] ff (ϕ0)
The universal modality states that, for any event satisfying the symbolic action (p,c) from a state Q, the state Q it transitions to must then satisfy the continuation formula. No state can satisfy the continuation ff, and formula ϕ 0 can only be satisfied when Q does not exhibit the event described by (p,c). All the states in fig. 1b trivially satisfy this property (as there are no outgoing state transitions on (p,c) of formula ϕ 0 ) with the exception of Q 3 . If this state exhibits the concrete event pid 1 :pid 2 ! bye,-1 , it matches the pattern p, yielding Tbl. 1: Trace event actions capturing the behaviour exhibited by the SuS the substitution σ = {Srv → pid 1 ,Clt → pid 2 ,Ack → bye,Tot → -1}. As cσ also holds, then we can conclude that Q 3 violates formula ϕ 0 . The formula ϕ 1 below extends ϕ 0 to one that is invariant for any state reachable from the current state; this formalises property P 1 from sec. 2.

max x. 1 [Srv ?Req, ]x, 2 [Srv:Clt ! Ack ,Tot , Ack = bye ∧ Tot < 0]ff, [Srv:Clt ! Ack ,Ans , Ack = ok ∨ (Ack = bye ∧ Ans ≥ 0)] 3 x (ϕ1)
Whereas 2 corresponds to formula ϕ 0 , 1 and 3 cover the other possible actions produced in fig. 1b, recursing on the fix-point variable x.

Note that the formula variables Srv , Clt, Tot, etc. in eg. 1 are different to the program variables of fig. 1a bearing the same name. In our setting, program behaviour is observed as events, and formulae variables are used to patternmatch and reason about data in these events. We adopt the convention of naming formulae and program variables identically, merely to indicate the link between program and event data to readers.

The tool. The syntax used by detectEr deviates minimally from sHML. Concretely, the comma symbol delimiting patterns and constraints is dropped in favour of the when keyword, whereas vacuous constraints, i.e., when , may be omitted. The tool also supports a shorthand notation for patterns to specify atomic values directly; these are implicitly matched against action data, e.g. subformula 2 from eg. 1 can be abbreviated to [Srv:Clt ! bye,Tot when Tot < 0]. Moreover, redundant data variables can be replaced by the 'don't care' pattern, ( _ ), that matches arbitrary data values. This sugaring enables us to rewrite ϕ 1 from eg. 1 as:

max x. [ _ ? _ ]x, [ _ : _ ! bye,Tot when Tot < 0]ff, [ _ : _ ! Ack ,Ans when Ack = ok ∨ (Ack = bye ∧ Ans ≥ 0)]x
Example 2. Property P 2 from sec. 2 describes a fragment of the client-server interaction, asserting that server replies are always addressed to the clients issuing them. Unlike ϕ 1 , this property induces data dependency across nested formulae.

max x.     1 [Srv 1 ? Clt1 , _ ] 2 [Srv 2:Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt1 = Clt2 ]ff, [Srv 2:Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt1 = Clt2 ] 3 x     (ϕ2)
P 2 can be formalised as the formula ϕ 2 , where the data dependency is expressed via the binders Srv 1 and Clt 1 in 1 , which are then used in the constraint of sub-formulae 2 and 3 . The constraint Srv 1 = Srv 2 scopes our reasoning to a single server instance. Formula ϕ 2 is violated when Clt 1 = Clt 2 (since the continuation would need to satisfy ff), and recurs on x otherwise. Recall that the aforementioned comparisons between variable instantiations is possible since the substitution σ obtained from matching the symbolic action of modality 1 extends to the context of sub-formulae 2 and 3 .

Example 3. Property P 3 specifies a control aspect of the client-server interaction, demanding that requests issued by clients are never serviced more than once. Formula ϕ 3 expresses this requirement via a guarded fix-point that recurs on x for sequences of send-recv actions; this captures normal server operation that corresponds to sub-formulae 1 followed by 2 , and then 4 followed by 2 .

1

[ _ ? _ ] max x. [Srv 1:Clt 1 ! _ ] 2 3 [Srv 2:Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt1 = Clt2 ]ff, [ _ ? _ ] 4 x (ϕ3)
Formula ϕ 3 is violated when a send action matched by 2 is followed by a second send action that is matched by 3 . The constraint Clt 1 = Clt 2 in sub-formula 3 ensures that duplicate send actions concern the same recipient.

Our earlier formula ϕ 2 of eg. 2 does not account for the case where the server interacts with more than one client. It disregards the possibility of other interleaved events, that are inherent to concurrent settings where processes are unable to control when messages are received. For instance, while sub-formula 1 matches an initial recv action, a second recv action (e.g. due to a second client C 2 that interacts with the server) matches neither 2 nor 3 . This does not reflect the requirement of our original property P 2 . The problem can be addressed by augmenting formulae with clauses that 'eat up' non-relevant actions.

max x.       [Srv 1 ? Clt1 , _ ] 1 max y.    [Srv 2:Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt1 = Clt2 ]ff, [Srv 2:Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt1 = Clt2 ]x, [ _ ? _ ]y 2         
As the refinement of ϕ 2 above shows however, this bloats specifications, which is why we chose to scope our exposition to a single client-server set-up for the benefit of readers. Introducing the nested maximal fix-point 1 and sub-formula 2 filters recv actions by recursing on variable y; the rest of ϕ 2 is unaltered.

What Goes On

Often, post-deployment verification techniques such as RV, do not have access to the entire execution graph of a SuS, e.g. the transition model in fig. 1b. Instead, these are limited to the trace of (program) events that is generated by the current execution of the SuS. For instance, an execution might generate the trace of events 'pid 1 ? pid 2 ,stp .pid 1 :pid 2 ! bye,-1 ', that corresponds to the (finite) path traversal

Q 0 → Srv ? Clt ,stp → Q 3 → Srv:Clt ! bye,Tot → Q 4 in the transi- tion model of fig. 1b.
In traces, events consist of concrete values instead of variable placeholders, e.g. pid 1 instead of Srv , etc. This limitation can be problematic when verifying specifications that reason about entire SuS transition models, e.g. properties expressed in the µ-calculus [START_REF] Kozen | Results on the Propositional µ-Calculus[END_REF][START_REF] Larsen | Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion[END_REF][START_REF] Aceto | Testing Hennessy-Milner Logic with Recursion[END_REF], CTL [START_REF] Jr | Model Checking[END_REF][START_REF] Baier | Principles of Model Checking[END_REF], and other branching-time logics. Recent studies show that finite traces suffice to adequately verify a practically-useful subset of these properties, as long as the verification is confined to either determining satisfaction or violation [START_REF] Francalanza | On Verifying Hennessy-Milner Logic with Recursion at Runtime[END_REF][START_REF] Francalanza | Monitorability for the Hennessy-Milner Logic with Recursion[END_REF][START_REF] Aceto | Monitoring for silent actions[END_REF][START_REF] Aceto | Adventures in Monitorability: From Branching to Linear Time and Back Again[END_REF][START_REF] Aceto | The Best a Monitor Can Do[END_REF] (not both). This is more commonly referred to as specification monitorability [START_REF] Francalanza | Monitorability for the Hennessy-Milner Logic with Recursion[END_REF]. sHML, used in sec. 3 to encode properties P 1 -P 3 , has been shown to be a maximallyexpressive subset of the µ-calculus for the runtime analysis of violations. This means that (i) any program that violates a property expressed as a sHML formula can be detected at runtime, (ii) any µ-calculus property whose violations can be detected at runtime can be expressed as a sHML formula.

From specification to analysis. detectEr synthesises automata-like analysers in Erlang from sHML; these inspect trace events incrementally and reach irrevocable verdicts. An analyser flags a rejection verdict when it processes a trace exhibiting the program behaviour that violates a property of interest-crucially, it never flags verdicts associated with the satisfaction of the property [START_REF] Francalanza | Monitorability for the Hennessy-Milner Logic with Recursion[END_REF][START_REF] Aceto | Monitoring for silent actions[END_REF][START_REF] Aceto | The Best a Monitor Can Do[END_REF]. Intuitively, this is because the trace observed at runtime can never provide enough information to rule out the existence of violating behaviour in other execution branches of the program. The synthesised analyser code embeds this reasoning: when a trace event is not included in the set of actions denoted by the symbolic action of a necessity modality, an inconclusive verdict is flagged.

Our synthesis translates a sHML specification to Erlang code encoded as a higher-order function, tasked with the analysis of trace events. This function accepts an event as input, and returns a new function of the same kind that performs the residual analysis following the event just processed. The synthesis, -, that maps sHML constructs to Erlang syntax is as follows:

ff (fun (_) → io:format("Rejection") end) () max x. ϕ (fun x() → ϕ end) () x x() i∈I [pi,ci ]ϕi                  fun(p1) when c1 → ϕ1 . . . (pn) when cn → ϕn (_) → (fun (_) → io:format("Stopped") end) () end
In -, ff is translated into an anonymous function that flags rejection, modelling formula violations; tt is not synthesised into analysis code since it can never be violated. Maximal fix-point formulae are translated to named functions that can be referenced by x . The conjunction of necessities, i∈I [p i ,c i ]ϕ i , maps naturally to a sequence of function clauses, where the pattern p i matches the shape of the trace event, and the constraint c i -expressed as an Erlang guard [START_REF] Cesarini | Erlang Programming: A Concurrent Approach to Software Development[END_REF]operates on variables bound in p i and those instantiated in the parent function scope. Inconclusive verdicts are modelled via the catch-all clause (_) that matches any events other than those described by the clauses, fun(p i ) when c i . The order of clauses in Erlang does matter, and affects our synthesis in two ways: (i) it conveniently allows us to handle the inconclusive verdict case using a catch-all clause at the end of function definitions; (ii) the mutually-exclusive symbolic actions in a necessity conjunction allows us to synthesise them in the order specified, without affecting the commutativity of conjunctions. Note that the synthesis applies the generated functions, i.e., (), to unfold them once. Fig. 2 depicts the behaviour of the analyser that is synthesised from formula ϕ 2 of eg. 2. It consists of two states, Q 0 , Q 1 , the rejection verdict state , and the inconclusive verdict state ? . The transition from Q 0 to Q 1 in fig. 2 corresponds to the modality [Srv 1 ? Clt 1 , _ ], 1 in formula ϕ 2 , while the transitions between Q 1 and , Q 1 and Q 0 express sub-formulae 2 and 3 . The auxiliary transitions from states leading to ? correspond to the catch-all (_) clause inserted by the synthesis for conjuncted necessities. Fig. 2 illustratively labels these transitions by the complement of the set of actions from a given state. For example, the symbolic action set Pat\{ _ ? _ , _ } from Q 0 to ? matches anything but recv events; recv events are, in turn, matched by Srv 1 ? Clt 1 , _ labelling the transition between Q 0 and Q 1 . Verdict irrevocability, a prevalent RV require-

Q 0 Q 1 ? Srv 1 ? Clt 1 , _ Srv 2 :Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt 1 = Clt 2 Srv 2 :Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt 1 = Clt 2 Pat \ Srv 2 : _ ! _ when Srv 1 = Srv 2 Pat \ _ ? _ , _
Fig. 2: Abstract model of the analyser synthesised from formula ϕ 2 ment [START_REF] Aceto | An Operational Guide to Monitorability with Applications to Regular Properties[END_REF], is modelled by the detectEr synthesis in terms of final states ( and ? in fig. 2). The analysis stops when a final state is reached.

Specification, in practice. detectEr processes sHML formulae specified in plain text files. The syntax follows the one given in sec. 3, albeit with two adaptations: (i) the keyword and is used in lieu of , and, (ii) we adopt the Erlang operators for writing boolean constraint expressions, e.g. =:= instead of =, andalso instead of ∧, orelse instead of ∨, etc. Analysers resulting from the synthesis, -, are compiled to binaries to be packaged with the SuS executables.

The Magical Mystery Tour

Instrumentation is central to RV. It refers to the extraction of the computation of interest in the form of a sequence of trace events from an executing program, and its reporting to the runtime analysis discussed in sec. 3. Formulae can be rendered unverifiable at runtime when the program events they assume cannot be extracted and reported by the instrumentation. The instrumentation also plays a role in dropping extraneous events that can infiltrate the trace being observed and potentially, interfere with the analysis.

What to monitor. We provide the meta keywords with and monitor to target the SuS component of interest for a particular specification. The with keyword picks out the signature of the function that is forked whereas the monitor keyword defines the property to be analysed. For example, to runtime verify the behaviour of the calculator server of fig. 1a against formula ϕ 2 , we write: From an instrumentation standpoint, with establishes the set of trace events corresponding to the SuS component it targets, thus enabling the specification to abstract from the events generated by other components. This helps to keep the size of specifications compact whenever possible. In using with, formula ϕ 2 need not account for superfluous events (e.g. those of another server component) that tend to make the specification exercise tedious and error-prone.

with calc_server : loop( _ ) monitor max x.    [Srv 1 ? Clt1 , _ ] [Srv 2:Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt1 = Clt2 ]ff, [Srv 2:Clt 2 ! _ when Srv 1 = Srv 2 ∧ Clt1 = Clt2 ]x    (ϕ 2 ) L S AS
How to monitor. detectEr offers three instrumentation methods, inline (sec. 6), outline (sec. 7), and offline (sec. 8), to cater for different situations where the RV is conducted. These methods are depicted by the three set-ups of fig. 3 that are instantiated with our calculator server, labelled by S, and its parent launcher process, labelled by L. Inlining statically instruments system components with the analyser, A S , which then executes as part of the SuS. Outline instrumentation decouples the SuS components from the extraction and analysis of trace events by way of the tracing infrastructure provided by the EVM. The offline set-up extends the latter notion to a SuS that (possibly) executes outside the EVM, mirroring the same architecture of fig. 3b to enjoy the same outline arrangement (elided from fig. 3c). The with keyword directs detectEr to instrument the analyser code over the relevant SuS components regardless of the instrumentation method used, to ensure that the same set of trace events is reported to the runtime analysis. This makes the analysers generated by our synthesis of sec. 4 agnostic of the underlying instrumentation.

Come Together

Inlining [START_REF] Falcone | A Taxonomy for Classifying Runtime Verification Tools[END_REF] is the most efficient instrumentation method detectEr offers. While it assumes access to the source code of the SuS, it carries advantages such as Fig. 4: Instrumentation pipeline for inlined program monitoring via weaving low runtime overhead [START_REF] Erlingsson | SASI Enforcement of Security Policies: A Retrospective[END_REF][START_REF] Erlingsson | The Inlined Reference Monitor Approach to Security Policy Enforcement[END_REF] and immediate detections [START_REF] Bartocci | Introduction to Runtime Verification[END_REF]. detectEr instruments invocations to synthesised analysers via code injection by manipulating the program abstract syntax tree (AST). This procedure is depicted in fig. 4.

In step 1 , the Erlang program source code is preprocessed and parsed into the corresponding AST, step 2 . The Erlang compilation pipeline includes a parse transformation phase [START_REF] Cesarini | Erlang Programming: A Concurrent Approach to Software Development[END_REF], step 3 , that offers an optional hook to allow the AST to be processed externally, prior to code generation. Our custom-built weaver leverages this mechanism to transform the program AST in step 4 and produce the modified AST in step 5 ; this is subsequently compiled by the Erlang compiler into the program binary, step 6 . The compilation phase depends on the detectEr core modules and analyser binaries, as does the SuS, once it executes.

Instrumentation, in one go.

Step 4 in fig. 4 performs two transformations on the program AST. The first transformation initialises an analyser. It weaves code instructions that store the function encoding of the synthesised analyser (refer to sec. 4) in the process dictionary (PD) of the instrumented process (PDs are process-local, mutable key-value stores with which Erlang actors are initialised).

The weaver identifies spawn() calls that carry the function signature to be executed as a process. It then replaces the spawn() call with a counterpart which accepts an anonymous wrapper function that (i) stores the analyser function in the PD, and, (ii) applies the function specified inside the original spawn() call. Fig. 5a recalls the function start() that forks our calculator server loop, line 1. The corresponding weaved version of its AST-given as Erlang code for illustration in fig. 5a-performs the initialisation of (i) and (ii). Line 3 contains (omitted) boilerplate logic that determines whether a particular spawn() call should be instrumented. The meta keyword with from sec. 5 is used to this end: it results in the synthesis of auxiliary code that enables the weaver to effect this judgement. For example, the specification 'with calc_server:loop(_). . . ' of formula ϕ 2 informs the weaver to initialise the analyser only for the function name loop forked by the invocation of spawn() on line 1 in fig. 5a. In line 8, the encoding of the analyser function, AnlFun0, is stored in the PD. The signature 1 start() → spawn(calc_server, loop, [0]). The second transformation decorates the program AST with calls at points of interest: these correspond to the actions catalogued in tbl. 1. Each call constructs an intermediate trace event description that is dispatched to the analyser. Lines 9 and 12 in fig. 5a construct events init and fork, and dispatch them to the analyser using the function anl:dsp() exposed by the core detectEr modules. The events recv and send are analogously handled on lines 4 and 6 in fig. 5b.

Our weaver performs the two transformations outlined above regardless of whether monitoring is required by the SuS. This induces a modular design where the SuS is weaved once, while the analyser binaries may be independently regenerated, e.g. to refine or add sHML specifications. Updates in these binaries can afterwards be put into effect by restarting the weaved SuS. To determine whether to analyse a trace event, the dispatcher implementation anl:dsp() internally checks against the PD whether an analyser function has been initialised for the instrumented process. When the analyser function is initialised, anl:dsp() applies the function to the event, and saves the resulting unfolded analyser function back to the PD; otherwise, anl:dsp() discards the event. An irrevocable verdict is reached by the analyser function once its application to an event returns the internal value that encodes or ? .

Weaving makes it difficult to extract exit trace events, since abnormal termination due to crashes cannot be easily anticipated. This limits the ability to runtime check correctness properties concerning process termination. An instrumentation approach via external observation easily sidesteps this restriction.

Tell Me What You See

Outlining externalises the acquisition and analysis of SuS trace events. It relies on the tracing infrastructure provided by the EVM [START_REF] Cesarini | Erlang Programming: A Concurrent Approach to Software Development[END_REF], and supports any software component that is developed for the EVM ecosystem, e.g. Erlang, Elixir [START_REF] Jurić | Elixir in Action[END_REF] and Clojerl [START_REF] Facorro | Clojerl language[END_REF]. Fig. 3b in sec. 5 shows the outlined set-up for our calculator server example. Outlining uses tracers, actor processes tasked with the handling of trace events exhibited by the SuS. Tracers register with the EVM tracing infrastructure to be notified of process events in connection to the actions of tbl. 1. Our outlining algorithm instruments tracers on-demand, depending on what processes need to be analysed. This approach departs considerably from inline instrumentation in sec. 6, and rather than weaving the SuS statically, outlining defers the decision of what to instrument until runtime.

While outline instrumentation tends to induce higher runtime overhead, it offers a number of benefits over inlining. It takes a non-invasive approach that leverages the EVM to trace components without modification, making it easy to enable and disable the runtime analysis without the need of restarts or redeployments. By decoupling the SuS and tracer components, outlining induces a degree of partial failure-a faulty analyser does not compromise the running system, nor does a crashed system component affect the external tracer. As a result of this arrangement, exit trace events can be detected, giving us the full expressiveness with respect to the system actions of tbl. 1. The implementation of an adequate outline monitoring set-up comes with its own set of challenges. For example, the instrumentation should be engineered to scale in line with the SuS, while the runtime analysis of trace events is underway. It has to contend with the race conditions (e.g. trace event reordering) that arise from the asynchronous execution of the SuS and tracer components. Scalability requires the instrumentation to explicitly manage garbage collection, where redundant tracer processes are discarded to minimise resource consumption. Inline instrumentation is spared these complications since the analysis logic is weaved directly in SuS processes. Although our outline instrumentation algorithm handles these aspects, we refrain from providing further detail in this presentation. Interested readers are encouraged to consult [START_REF] Aceto | A Choreographed Outline Instrumentation Algorithm for Asynchronous Components[END_REF] for more details.

Instrumentation, as we go. The EVM tracing infrastructure enables processes to register their interest in receiving trace event messages from other processes. Erlang provides the built-in function trace(), that processes may invoke to enable and disable process tracing dynamically at runtime. Our tracers from fig. 3b leverage this functionality to fork other tracers, and scale the RV set-up as the SuS executes. We configure the EVM tracing to automatically assign the tracer of an already-traced SuS process to the children it forks [START_REF] Cesarini | Erlang Programming: A Concurrent Approach to Software Development[END_REF]. Using this as a default setting allows us to analyse groups of processes as one component. The with keyword guides the targeting of which processes tracers need to track and analyse. By contrast to inlining-where the set of trace events of a component is implicitly determined as a byproduct of weaving-outlining must actively isolate processes from a group to assign dedicated tracers. Recall the specification 'with calc_server:loop(_). . . ' of formula ϕ 2 . This instructs our outline instrumentation to set up an independent tracer process for the calculator server loop forked by spawn() on line 1 in fig. 5a.

Tracers are programmed to react to fork and exit events in the trace. Fig. 6 illustrates how the process creation sequence of the SuS is exploited to instrument a dedicated tracer for our calculator server. A tracer instruments other tracers whenever it encounters fork events. The initial RV configuration is shown in fig. 6a, where the root tracer, T L , is assigned to the launcher process, L, in step 1 . L forks the server function loop() to execute as the process S which is automatically assigned the same tracer T L , as steps 2 both indicate. Subsequently, T L instruments a new tracer, T S , when it processes the fork trace event due to L in step 3 . The data carried by fork contains the PID of the forked process (see tbl. 1) that designates the SuS process to be instrumented, S, in this case. At this point, T S takes over the tracing of S from the root tracer T L by invoking trace() to handle S independently of T L , steps 4 and 5 . T S resumes its analysis of S, receiving the init event in step 7 ; this is followed by recv in step 9 as a result of the service request issued by the client, C, in step 8 . In a similar way, the service reply sent by the server to C in step 10 results in send being exhibited by S and received by T S in step 11 . Process L eventually exits after the fork completes, step 12 . The ensuing exit event in step 13 is interpreted by the root tracer T L as the cue to self-terminate in step 14 . This garbage collection measure maintains the lowest possible runtime overhead.

I'm Only Sleeping

We extend the notion of outline instrumentation to the offline case where the SuS may potentially run outside the EVM. To support offline instrumentation, de-tectEr implements a middleware that emulates the EVM tracing infrastructure, while preserving the configuration mentioned in sec. 7, i.e., where forked system processes automatically inherit the tracer assigned to their parent. This enables detectEr to employ the same outline instrumentation algorithm for offline monitoring. Offline set-ups are generally the slowest in terms of verdict detection, by comparison to the inline and outline forms of instrumentation. This stems from the dependence outline instrumentation has on the timely availability of pre-recorded runtime traces that are subject to external software entities such as files, databases, and the SuS itself. However, the outline set-up and SuS can reside on different hardware since they are mutually detached. Such an arrangement makes overhead issues secondary.

Fig. 3c from sec. 5 overviews our offline arrangement. It mirrors the setup in fig. 3b: the only difference lies in how the offline tracing infrastructure obtains events. Our Log Tracer component in fig. 3c exposes a trace() function, providing the same EVM feature subset relevant to outlining. The implementation relies on log files as the medium through which the SuS can communicate trace events to the offline set-up. It can process log files with complete system executions, or actively monitor files for changes to dynamically dispatch events to tracers while the SuS executes and writes events to file. Offline tracing supports the event actions in tbl. 1; these carry the event data and are assumed to follow a pre-defined format. For instance, the offline event description fork(pid 1 , pid 2 , {calc_server, loop, [0]}) is mapped to the action pid 1 →pid 2 , calc_server:loop([0]) by the Log Tracer of fig. 3c. Our filebased approach to collecting SuS events is motivated by the fact that file logging is widely-adopted in practice, and is offered by popular frameworks such as Lager [START_REF] Basho | [END_REF] for Erlang, Log4J 2 [16] for Java [START_REF] Loy | Learning Java: An Introduction to Real-World Programming with Java[END_REF], and the Python [START_REF]Python: Logging Facility for Python[END_REF] logging facility. Besides logging, events may also be extracted from the SuS via other tracing frameworks, e.g. DTrace [START_REF] Cantrill | Hidden in Plain Sight[END_REF], LTTng [START_REF] Desnoyers | The LTTng Tracer : A Low Impact Performance and Behavior Monitor for GNU/Linux[END_REF], and OpenJ9 Trace [START_REF]IBM: Openj9[END_REF]. [START_REF] Aceto | On Benchmarking for Concurrent Runtime Verification[END_REF] Here, There and Everywhere This paper presents detectEr, a RV tool that analyses program correctness postdeployment against properties expressed in a logic that has been traditionally used for static verification [START_REF] Bunte | The mCRL2 Toolset for Analysing Concurrent Systems -Improvements in Expressivity and Usability[END_REF][START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF][START_REF] Andersen | CAAL: Concurrency Workbench, Aalborg Edition[END_REF]. Secs. 5-8 describe how detectEr can flexibly runtime check the same specifications via three instrumentation methods. The tool can be found at https://duncanatt.github.io/detecter. Future work. We intend to asses the merits of our three instrumentation methods in terms of the multi-faceted overhead metrics proposed by [START_REF] Aceto | On Benchmarking for Concurrent Runtime Verification[END_REF]. We also plan to extend detectEr to handle sHML specifications where conjunctions and universal modalities can be treated as separate logical constructs [START_REF] Aceto | Determinizing Monitors for HML with Recursion[END_REF][START_REF] Aceto | On the Complexity of Determinizing Monitors[END_REF][START_REF] Francalanza | Monitorability for the Hennessy-Milner Logic with Recursion[END_REF][START_REF] Attard | Trace Partitioning and Local Monitoring for Asynchronous Components[END_REF][START_REF] Attard | A Monitoring Tool for a Branching-Time Logic[END_REF][START_REF] Cassar | A Suite of Monitoring Tools for Erlang[END_REF][START_REF] Cassar | Improving Runtime Overheads for detectEr[END_REF]. This facilitates the composition of properties via conjunctions, e.g. formulae ϕ 1ϕ 3 from sec. 3 can be combined as ϕ 1 ∧ϕ 2 ∧ϕ 3 to synthesise one global monitor. Although detectEr focusses on properties that are known to be runtime monitorable, new results argue that monitoring can be systematically extended to the entire class of regular properties, albeit, with possibly weakened detection guarantees [START_REF] Aceto | The Best a Monitor Can Do[END_REF][START_REF] Aceto | A Framework for Parameterized Monitorability[END_REF]. We aim to incorporate these results within this tool.

Fig. 3 :

 3 Fig. 3: Inline, outline and offline instrumentation methods offered by detectEr

2 start() → 3

 3 AnlFun0 = ... % Load analysis logic.

4 P1 3 M2 5 ( 7 loop

 4357 = {Clt, {add, A1, A2}} → 4 anl:dsp(recv, self(), M2), P1 = Clt) ! M1 = {ok, A1 + A2}, 6 anl:dsp(send, self(), P1, M1), , stp} → % Stop service.13 ... 14 end. (b) Weaved analysis code in server loop

Fig. 5 :

 5 Fig. 5: Transformations to the AST of the calc_server program (shown as code)

10 init 7 recv 9 send 11 exit 12 exit 13 exit 14 (Fig. 6 :

 10146 Fig. 6: Outline instrumentation for the calculator server (analysers omitted)

Supported by the doctoral student grant (No: 207055-051) and the MoVeMnt project (No: 217987-051) under the Icelandic Research Fund, the BehAPI project funded by the EU H2020 RISE under the Marie Skłodowska-Curie action (No: 778233), the ENDEAVOUR Scholarship Scheme (Group B, national funds), and the MIUR project PRIN 2017FTXR7S IT MATTERS.


In J-Y. Girard's Logic Dictionnary in "Locus Solum", MSCS, vol. 11/3, Cambridge UP, 2001.

Giuseppe Longo

CNRS et ENS, Paris, http://www.di.ens.fr/~longo/ LAPLACE (or, Reflections on incompleteness)

A major mathematician, known for his seminal work in Infinitesimal Analysis, Astronomy, Probability Theory. Laplace proposed a paradigm for the mathematical analysis of Physics, the so called « laplacian determinism ». In this perspective, the systems of (differential) equations could "completely" describe the physical world. More precisely, if one wanted to know the state of the physical world in a future moment, with a given approximation, than it could suffice to know the current state of affairs up to an approximation of a comparable order of magnitude. By formally computing a solution of the intended equations, or by suitable approximations by Fourier series (as it will be said later), one could deduce (or predict or decide) the future state, up to the expected level of approximation.

Poincaré, as a consequence of his famous theorem on the three bodies problem, proved that minor variations of the initial conditions could give enormous changes in the final result or, even, that the solutions could depend discontinuously on the initial conditions. Then, predictability, as "completeness w.r.t. the world" of a suitable set of differential equations, failed. About one century later, D. Hilbert resumed Laplace's program in a different context. He first set the basis for the rigorous notion of « formal system », as well as for the distinction between « theory » and « metatheory ». He then conjectured that the key system for Number Theory, Peano's first order Arithmetic (where he had interpreted Geometry, 1899), was complete w.r. t. the intended structure of numbers (or that any first order assertion about the « world of numbers » could be decided by formal or « potentially mechanisable » tools).

A few soon reacted to Hilbert's program, such as the "lone wolf" among Hilbert's students, Hermann Weyl, who (though hesitantly) conjectured in Das Kontinuum, 1918 (!), the incompleteness of formal arithmetic (end of §.3). He also stressed in several places that the idea of mechanization of Mathematics trivializes it and misses the reference to meaning and structures.

Besides Weyl (and Poincaré and a few others), Wittgenstein is another thinker who criticized Hilbert's program. For him «Hilbert's metamathematics will turn out to be a disguised Mathematics» [Waismann, 1931], since «[A metamathematical proof] should be based on entirely different principles w.r. t. those of the proof of a proposition ... in no essential way there may exist a meta-mathematics» (see Wittgenstein, Philo. Rem., § 153;quoted in [Shanker,1988]) and ... «I may play chess according to certain rules. But I may also invent a game where I play with the rules themselves. The pieces of the game are then the rules of chess and the rules of the game are, say, the rules of logic. In this case, I have yet another game, not a metagame» [Wittgenstein, 1968;p. 319].

As for formal Arithmetic, the key theory for finitistic foundationalism, these remarks may be now understood in the light of Gödel's Representation Lemma [Gödel, 1931]: by this very technical result, one may encode the metatheory of arithmetic into arithmetic itself, thus the "rules of the metagame" are viewed just as ... rules of the "arithmetical game". Moreover, many proofs, which entail the consistency of Arithmetic, such as (Tait-)Girard proof of "normalization" of Impredicative Type Theory ([Girard et al., 1989]), need a blend of metalanguage and language; or even purely combinatorial statements, such as Friedman's Finite Form of Kruskal's theorem, provably require the same entangled use of metatheory, theory and semantics, by the impredicative notions involved (see [Harrington et al., 1985]); an indirect confirmation of Wittgenstein's philosophical insight (and Weyl's, as for incompleteness).

Both Laplace and Hilbert program, which are strictly parallel and contributed to positivist philosophies in physics and in mathematics, opened the way to very relevant mathematical work: when precise and robust, even wrong programs may have extraordinary developments (such as XIX century Analysis, partly motivated by the laplacian « calculus of perturbations », or the rigorous notion of mechanisable computation of the '30's and its fall-out: actual computers, as purely formal symbol pushers). However, the corresponding incompleteness theorems, Poincaré's and Gödel's or more recent « concrete » ones, such as the two mentioned above, should finally take us away for the underlying philosophies, also to go further with mathematics.

Poincaré's result, for example, is at the origin of beautiful and new mathematical theories (the geometry of dynamical systems), where qualitative predictions replace quantitative ones and the "mathematical understanding" does not need to coincide with completeness or predictability by formal tools. In mathematical logic we are not yet at a similar revolution, but the basis are being set towards breaking the metaphysics of the relevant, but artificial, organization of the discourse proposed by Hilbert, the theory/metatheory frame. Similarly, we have to overcome the believe that language ''predicates'' about the world: language and structures (of mathematics, of physics) are in permanent resonance. They construct themselves while singling out concepts and objects, in a permanent tension, which requires a parallel analysis of the foundation of these disciplines.

One further step is being now taken, well beyond the laplacian philosophy of formalism in Logic and Cognition. XX century physics departed from the Newtonian ''causal lawfulness'' of nature (and the mysterious instantaneous action at distance, gravitation) and stressed the geometric structuring of the world, by "geodetic principles". By this, it moves also towards unification with Quantum Mechanics (non-commutative geometry). In a sense, it is the structure of space and location only that matter, similarly as in the geometry of deduction in "Locus Solum".

For

  further remarks and for the references quoted above, see the downloadable papers: G. Longo "The reasonable effectiveness of Mathematics and its cognitive roots" To appear in "New Interactions of Mathematics with Natural Sciences" (L. Boi ed.), Springer 2005. G. Longo. "Laplace, Turing and the "imitation game" impossible geometry: randomness, determinism and programs in Turing's test". Invited lecture, Conference on Cognition, Meaning and Complexity, Roma, June 2002 (version française, Intellectica, n. 35, 2002/2, pp. 131-162.