Online Monitoring of Spatio-Temporal Properties for Imprecise Signals

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires to reason about complex spatio-temporal properties of physical and/or computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and to reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing their spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterising the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.

INTRODUCTION
Complex emergent spatio-temporal patterns such as traffic congestion or travelling waves are central in the understanding of networked dynamical systems where locally interacting entities are operating at different time and spatial scales. We can observe these patterns both in biological systems [3,5,11] as well as human engineered artefacts such as Collective Adaptive Systems [22] (CAS) and Cyber-Physical Systems [31] (CPS). CAS and CPS consist of a large number of heterogeneous (physical and computational in CPS) and spatially distributed entities featuring complex interactions among themselves, with humans and other systems. Example include biking sharing systems, the internet of things, contact tracing devices preventing the epidemic spread, vehicular networks and smart cities. Many of these systems are also safety-critical [31], meaning that a failure could result in loss of life or in catastrophic consequences for the environment.
The complex interaction with the physical environment in which these systems are embedded prevents them from being exhaustively verified at design time. A common alternative is testing [4]: traces generated during their execution/simulation are stored and monitored offline with respect to a formal specification used as an oracle. However, testing may provide a limited coverage and does not take into account physical failures that may happen during the execution. Online monitoring is instead a preferable solution when the monitoring verdict requires the immediate action of a policy maker during the system's execution or when it is very computationally expensive [32] generating and storing the system's execution traces to be monitored offline. Motivating example. As a case study we consider a sensor network for environmental monitoring. Air pollution is the primary cause of the loss of biodiversity, of the reduction of agricultural productivity and of many diseases for humans' lungs and cardiovascular system. Policy makers are constantly monitoring the amount of 2 , an air pollutant that forms from the combustion of fossil fuels, to activate special policies that mitigate its release when levels grow too significantly for the public concern. For example, in the Italian region of Lombardy, there are over 80 stations distributed throughout the region monitoring the level of 2 in the air.  [20] in terms of / 3 . Red crosses and dotted line represent missing values. Data from the open data initiative of ARPA Lombardia [21].
the location of these stations, and the value reported in the town of Rezzato, for the first quarter of 2021. The measurements happen regularly every hour, but sometimes the sensors fail to communicate the measurements, because of meteorological issues, or temporary faults, and the actual values are provided later on. Furthermore, the values measured by the sensors are noisy and they have a certain degree of uncertainty. Another way to deal with the missing values, could be to check that nearby locations (e.g. within 10 Km) do not register alarming values of particles in the air and this is possible only if we consider spatio-temporal properties.
In this paper we address the problem of online monitoring of spatio-temporal properties over systems from which we can observe noisy signals with possible missing data or out-of-order samples. Spatio-temporal monitoring. In the last decade there has been a great effort to develop logic-based specification languages and monitoring frameworks for spatio-temporal properties. Examples include SpaTeL [12], SSTL [29], (SaSTL) [23,24] and STREL [1]. For more details on the underlying spatial models and the language expressiveness we refer the reader to [28]. In this paper, we consider STREL [1] a spatio-temporal logic operating over a dynamic weighted graph representing the spatial arrangement of spatially distributed entities. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterising the node's behavior. STREL extends the Signal Temporal Logic (STL) [25] with the reach and escape operators that generalizes the somewhere, everywhere and surronded spatial modalities, simplifying the monitoring that can be computed locally with respect to each node. However, the original work on STREL [1,2] provides only an offline monitoring algorithm. In contrast we present here the first online monitoring algorithm for STREL and in general for spatio-temporal monitoring.
Online Monitoring. To the best of our knowledge, the only online monitoring techniques [7,8,14,15,26,27,30] that are available in the literature can handle temporal specification languages such as STL [25] and Metric Temporal Logic [17] (MTL). One of the main challenges for online monitoring is how and when to decide the satisfaction/violation of a formula with temporal operators reasoning about future and not yet observed events. In [8] the authors provides, for the first time, a dynamic programming algorithm for the online monitoring of the robustness metric of MTL formulas with bounded future and unbounded past. The past formula is used to reason about the robustness of the actual system observations, while for evaluating the future formula they use a predictor to estimate the likely robustness. However, the value forecasted by the predictor needs to be trusted because it is not the real value that the system will provide. Other approaches [14,15,30] address the problem of deciding about the future using a technique called pastification that rewrites the future operators as past ones and delays the verdict. Similarly the works of Mamouras et al [26,27] delay the output verdict until some part of the future input is seen. In [7] the authors present an efficient online algorithm to compute the robust interval semantics for bounded horizon formulas. All these approaches assume that the data and the events to be observed come synchronously and in-order. Our contribution In contrast to these works, we present a novel approach to monitor online imprecise spatio-temporal signals (signals are defined on intervals, not just the robustness) where the samples can be processed also out-of-order. The notion of an interval is instrumental when representing partial knowledge about a value that is at least known to be within some boundaries. This might be because of errors in the measurement, or maybe because of some other sources of uncertainty throughout the process of acquiring and processing them. We define both a Boolean and a quantitative interval semantics for STREL and we prove the soundness and the correctness of the robust interval semantics. We design and implement, as extensions to the Moonlight tool 1 , the first online monitoring algorithm for not-in-order sampled signals, and the first online spatio-temporal monitoring tool. Our experiments demonstrate also convincing performances comparing with the state-of-the-art tool BREACH [9] for the online monitoring of temporal properties over in-order sampled signals.
Paper organization The rest of this paper is structured as follows. We provide the important aspects of interval algebra and our notion of imprecise signals in Section 2. In Section 3 we introduce the interval extension of the STREL logic, and its primary results, while in Section 4 we present our approach for the online monitoring of imprecise signals. Lastly, we present a realistic use case in Section 5 and we share our concluding remarks in Section 6.

INTERVAL ALGEBRA, SIGNALS AND SPATIAL MODEL
In this section, we define the key elements of interval algebra, signal and spatial model, which will be useful to characterize samples of the kind depicted in Figure 1. In addition to the classical notion of interval, it is useful to recall some basic operations that can be performed.
Definition 2.4 (Hausdorff Distance). Let , be two non-empty subsets of a metric space ⟨ , ⟩, we will call (Hausdorff) distance the function : P ( ) × P ( ) → R ≥0 defined as In practice, in our context, we can just consider the metric space defined by the euclidean distance over the real numbers, and thus reduces to computing max(| 1 − 2 |, | 1 − 2 |) for any two 1 , 2 ∈ I (R ∞ ), although for doing that we say, by definition, that if both 1 , 2 (or both 1 , 2 ) are infinite, then their Hausdorff distance is 0.
Now we have all the tools to introduce the concept of imprecise signals.
Definition 2.5 (Imprecise Temporal Signal). Let T ≡ [0, ∞] be a set representing the time domain, and let F (T, ), with ⊆ I (R) for a fixed ∈ N, be the family of functions over Cartesian products of real intervals; we call imprecise time signal, any ∈ F (T, ), i.e. any function : T → It is convenient, in some cases, to slice the signals based on the domain of interest, for that reason, we recall the concept of (signal) projection.
To represent a set of signals distributed in the space, we introduce the following definition. . We can naturally describe the distance between spatio-temporal signals by considering the Hausdorff distance from Definition 2.4 over all possible locations of the space, and time instants. Definition 2.8 (Spatio-Temporal Signal Distance). Let s 1 , s 2 ∈ F (L, T, ), we will call signal distance the largest Hausdorff distance over space and time, defined as: To describe the interplay of signals in different locations, we need to encompass the information related to the spatial distribution of the locations. Definition 2.9 (Spatial model). We call spatial model the tuple S = ⟨L, ⟩ 3 , where L is a set of locations and ⊆ L × R ∞ ≥0 × L is a proximity function associating at most one label ∈ R ∞ ≥0 to each distinct pair ℓ 1 , ℓ 2 ∈ L An obvious spatial model for the region of Figure 1 is a graph where every location is connected to all the others, and the proximity function is defined by labels corresponding to the minimal aerial distance between each pair of locations. Finally to consider distance on paths of locations we introduce the notion of routes over the spatial model. Definition 2.10 (Routes). A route on S is a (potentially infinite) sequence ℓ 0 , ℓ 1 , . . . ℓ . . . , such that for any ℓ , ℓ +1 ∈ , there is a label (ℓ , , ℓ +1 ) ∈ . We indicate by Λ(ℓ) the set of routes on S starting at ℓ. Moreover, we will use [ ] to denote the -th node of the route, [ . . . ] to denote the subroute starting at the -th node, and (ℓ ) to denote the first occurrence of ℓ in . Lastly, we will indicate by ℓ 1 < (ℓ 2 ) the fact that ℓ 1 precedes ℓ 2 in the route .
Routes have the same intuitive meaning as they have in the physical world, and, similarly to the real world, we can define the concept of route (or travel) distance, as the aggregated sum of all the labels traversed by the route.
Lastly, routes allow us to conveniently define the distance between any two locations ℓ 1 , ℓ 2 ∈ L, whichever the spatial model being considered. In fact, from the location ℓ 1 to ℓ 2 , one can consider the minimal distance among all the routes starting at ℓ 1 and ending in ℓ 2 :

STREL WITH INTERVAL SEMANTICS
We present in this section an interval semantics that allows for a conservative analysis that considers both the minimum and the maximum values of intervals. This way, a plethora of use scenarios can fit into this specification language, spanning from traditional offline monitoring of a given specification over imprecise signals to online monitoring with out-of-order updates. All the proofs of theorems and lemmas are reported in appendix.
Definition 3.1 (STREL Syntax). We consider logical formulae belonging to the language L generated by the following BNF grammar: where • ∈ {>, <}, ∈ R, is associated to a projection function of Definition 2.6, i.e. • are inequalities on the variables of the systems. U is the until temporal operator, with real interval, while R ≤ and E ≥ are the spatial operators reach and escape , with ∈ R >0 . In addition, we have the derived Boolean operators as and (∧) and implies (→), temporal operators eventually (F ) and globally (G ), and spatial operators somewhere ( ≤ ) and everywhere ( ≤ ).
Considering again the air pollution case study, current regulation in Lombardy requires to take action when the level of nitrogen dioxide ( 2 ) exceeds the threshold of 400 / 3 for more than three hours. Let 2 < 400 denote the atomic proposition that states that the level of nitrogen dioxide is lower than 400 / 3 . A requirement as the previous one could be expressed like in (1): Temporal operators like F specify properties on the dynamic evolution of the system. In fact, when (1) is violated, the alerting procedure could be triggered, to inform the citizens about the danger. However, since it is known that noise and local faults frequently happen, one could consider of alerting the population also when the close neighbourhood (e.g. within 10 Km) exhibits a similar phenomenon. For this aim, a property like (2) can be monitored.
Spatial operators like instead specify properties related to the spatial configuration, and in this context, the exact meaning is that at least a location in a range of less than 10 km must have a level of nitrogen dioxide lower than 400 / 3 . We will see other examples of the logic language in the next sections. For a more detailed description of the logic, we refer the reader to [1]. We present now the Boolean and quantitative interval semantics for STREL.
This is a three-valued semantics, which is equal to 1 if the interval signal (s, ℓ, , ) satisfies , −1 if the formula is not satisfied, and 0 if we cannot answer. The semantics is directly derived from the standard Boolean semantics and the interval algebra described in the previous section. For atomic proposition (s, ℓ, , • ) = 1 iff the inequality (s(ℓ, )) • is true. This means, e.g., (s, ℓ, , 2 > 400) = 1 iff 2 , the left extreme of the projected signal 2 , is greater than 400. (s, ℓ, , 2 > 400) = −1 if the right extreme is less than 400, and (s, ℓ, , 2 > 400) = 0 otherwise, so if 400 ∈ 2 interval value. Similar calculation can be done for the other combination of • and .
The three-valued Boolean semantics can be sufficient in applications where the interest is only whether or not the specification is satisfied. However, in many complex cases, one might be interested in getting some insights about the degree by which a property is satisfied or violated. In the following, we introduce an extension of the quantitative semantics that provides numerical bounds to the robustness degree of a specification.
We will indicate with : L × T → I (R ∞ ) the robustness signal, i.e. the signal generated by the partial application of the function to a given formula and a given signal s, so that (ℓ, ) ≡ (s, ℓ, , ).
Note that without the interval semantics we have defined, missing values should be substituted by some values that approximate the actual value (e.g. by linear interpolation), and therefore only approximate the actual value of satisfaction or robustness of a given property at that specific time point. Conversely, by exploiting the interval semantics, one could actually get upper/lower bounds at those points, which can actually be sufficient in real-world applications. To provide the correctness of the interval semantics over imprecise signals, we introduce the following lemma: . For any ∈ T, for any ℓ ∈ L, for any ∈ L, for any > 0, we have: PROOF. See the extended version of this article for the proof. □

ONLINE MONITORING
In this section a novel online (out-of-order) monitoring algorithm for STREL is presented. Differently from the standard offline approach, where all the data is available at the beginning of the execution, online monitoring is performed incrementally, when a new piece of data is available. In this case, the uncertainty related to the absence of information must be taken into account. For that aim, the machinery of imprecise signals can be exploited to represent the uncertainty, where the result of the monitoring process, whether it is a satisfaction or a robustness signal, is refined as soon as new updates of the input arrive.
The semantics for STREL is defined for arbitrary signals, but algorithms, for computational reason, are provided for piecewise constant ones, along the lines of [1,7]. This class of signals is convenient, and frequently chosen as the class of reference for a number of reasons: (i) it naturally describes digital signals, (ii) it can be stored in memory very efficiently, and processed fast enough to be considered for real-time applications, (iii) it allows to express the vast majority of real-valued signals of practical use with a limited loss of information. Since the presented signals are Lipschitz-continuous (we consider only inequalities on the variables of the system), we can always bound our error, considering the minimum time step and the maximum of their individual Lipschitz constants. An imprecise piecewise-constant signal : T → I (R ∞ ), can be characterized in the following way: , for ≤ < ∞ and graphically represented as in Figure 2. Note that frequently when monitoring real-time application the last part of the signal will be characterized by the widest interval possible, as this denotes the fact that the knowledge collected so far is insufficient for providing any insight about the monitored specification for future values of the signal. Similar infinite interval can be considered for missed values.
We consider space-synchronized (s.s.) signals, i.e. signals defined on the same time intervals for any location of the space model. More precisely, a p.c. s.s. signal : L × T → is a signal that can be represented as a sequence of pairs {( , V )} ∈N , where each pair ( , V ) of the sequence represents a piece of the signal, such that it maps any time-instant between and +1 in T, to the |L| × matrix V that represents the values of the dimensions of the signal at each location ℓ in L. The space-synchronization restriction might appear to be a severe limitation, but this shows one of the conceptual differences between online and offline monitoring: in an offline setting, the space-synchronization hypothesis would likely have detrimental effects on the performances, as it would force all the processing to happen at a temporal granularity that is the union of the temporal granularities of the signals at the different locations.
In an online setting, on the other hand, the temporal granularity is determined by the time when new information is available, and the space-synchronization hypothesis makes it possible to exploit in future work the Single-Instruction Multiple-Data (SIMD) capabilities of modern processors (see [13,18]), resulting in execution times that are virtually independent from the number of locations, when appropriate hardware is available. In this context, we call signal update u the triplet ( , , V), representing a mapping to the value matrix V for any time instant between (included) and (excluded). Signal updates can be seen as some special kinds of signals that we use to represent upcoming partial information from the online behavior of the monitored system. In the context of our analysis, we always assume updates to provide truthful information (the case of hard faults, i.e. where updates provide wrong information, will be explored in future work), and, for that reason, we can always assume updates to be well-formed, meaning that the interval V they provide is always included in the previous interval of the signal we stored for that time and location. To express the online nature of the computation we want to pursue, we need some way of describing the incremental evaluation of new information.
The refinement relation expresses the fact that s 1 and s 2 represent the same information, except that s 2 has a smaller degree of uncertainty. By the notions of signal update and signal refinement, we can easily represent the online evolution of a signal as a chain of signal refinements s 0 ≻ · · · ≻ s ≻ . . . , where the signal s +1 at the step + 1 can be computed from s and update u like in Algorithm 1. The REFINE( ) procedure takes a signal s as a sequence of ordered pairs, and an update as the triplet ( , , V). In practice, it removes all the pieces of the signal that start within the interval [ , ), and adds a piece with value V in the case and/or lay in between of and +1 . Clearly, for efficiency reasons, the algorithm can jump to the next pair each time +1 < , and can terminate as end for 14: end procedure soon as > . The updated signal at the end of the execution is the next element of the refinement chain, i.e. s +1 . The Monitoring Problem. When monitoring online a given specification , let s 0 be the signal representing the starting information on which the atoms of the formula are defined. Let also (u ) ∈N denote a (finite or infinite) sequence of signal updates. The online monitoring problem can be framed as computing the robustness signal s +1 , given s (or, alternatively, the satisfaction signal s +1 given s ), with s ≻ s +1 , starting from s 0 . A naïve implementation of an online monitor could just ignore the information coming from previous monitoring steps and restart the computation over the whole signal each time new information is available. As already noted in [7,8], such an implementation would result in huge amounts of wasted resources when monitoring time signals, and it would therefore be even more costly when monitoring space-time signals. To properly scope the effect that an out-of-order update of the input signal generates for the evaluation of a formula, it is convenient to think of updates as starting from the atoms of the monitored formula, and then propagating their effects up through the syntactic tree, generating a ripple effect where the impacted time span widens based on the operators of the subformulae. Figure 3 shows the ripple effect resulting from the propagation of update information through the syntactic tree. From this intuition we can define the update ripple function, to scope the resulting update's time span, based on the provided update, and on the operator being computed in the following way: otherwise Being able to assess the time boundaries of the effect of an update, we can therefore define an online monitoring procedure that updates the robustness (or satisfaction) signal when needed and that keeps the valid parts otherwise. In general, we have that at the step + 1, t t t t Figure 3: The ripple effect generated from the propagation of an update of the signal , over the formula the monitoring function can be evaluated as: Note that in all the cases where the updates overlap, they must be processed sequentially in order to generate correct results. Monitoring Procedure. To compute the monitoring result signal online, it is crucial to be able to exploit the knowledge from the past each time new information is available. The most natural way for doing so is to develop a stateful algorithm that stores the relevant information from previous computations. We will represent by M the persistent memory (i.e. the state) that we keep throughout the various iterations of the monitoring process, and by M [ ] the access to the item from memory. The memory M is organized around a data structure that represents the set of robustness signals of all the subformulae of the monitored formula , as computed in the last iterations. This set can be encoded as an array indexed on some ordering of the subformulae. We represent as M [ ] the access to the respective robustness signal for some formula . This data structure is extremely important to maximize the time performance of the monitoring process, as next iterations will re-compute only the differing fragments based on the update ripple. Before starting the monitoring process, the memory is initialized by storing an undefined signal for any subformula in the set of the subformulae of the formula being monitored. We call undefined signal the special signal : L × T → [−∞, +∞], which represents the total absence of knowledge about the value, at any possible time instant.
Once the memory is initialized, the monitoring can start. We assume that the signal is always received as a sequence of signal updates u , starting from = 0, where the input signal is considered to be undefined. Algorithm 2 represents the base routine triggered when receiving an update u of the input signal. The recursive procedure MONITOR(M, , u) is responsible for propagating the input signal update to the subformulae and then fetching the corresponding updates of the robustness signal. We indicate by ⟨M, { }⟩ the return value of the algorithm, to mean that it returns an updated version of the memory, and a list of robustness updates of the formula that might either be used by the caller or discarded. The general procedure of Algorithm 2 calls the specific procedures of Algorithms 3-6 depending on the operators encountered while traversing the tree of the formula. Note that all of the above exploit the REFINE( ) primitive operation from Algorithm 1. Online Monitoring Of Non-temporal Operators When monitoring formulae containing Boolean or Spatial operators, the online evaluation can be performed very efficiently by simply updating the robustness signal at the times corresponding to the received update. Algorithm 3 shows the algorithm for monitoring atomic formulae, Algorithm 4 presents the one for monitoring unary operators (i.e. ¬ and E ), and Algorithm 5 shows the one for binary operators (i.e. ∨ and R ). We represent by COMPUTE_OP(OP, V) (and COM-PUTE_OP(OP, V 1 , V 2 )) the execution of the semantic operation corresponding to the operator OP, along the lines of Definitions 3.2,3.3, i.e.
[max]/[min] direct computation for Booleans, and the classical reach/escape routines [1] for spatial operators. A key difference from the offline version of the spatial algorithms, however, is that in our online version the COMPUTE_OP implementation has been crafted to enable spatial-parallelization, i.e. monitors' users with appropriate hardware and the need to speed-up for large spaces, can opt-in for the multi-threaded version of the algorithm, where COMPUTE_OP is executed in parallel for any location of the spatial model. The algorithm for monitoring binary operators is slightly more complex, as it requires to take into account the corresponding value  return ⟨M, {u 1 OP 2 }⟩ 12: end function Online Monitoring Of Temporal Operators To execute temporal operators quickly enough for online needs, on the other hand, we need to store some extra information throughout the process. Firstly, it is useful to recollect that, in general, every temporal operator can be decomposed [10] in the conjunction of two (efficiently computable) operators: • the bounded eventually F (or equivalently the bounded globally G ) • the unbounded until U We propose here an enhanced algorithm for monitoring bounded globally/eventually operators with out-of-order updates. For that aim, we slightly adapted the classical sliding window algorithm from Lemire [19] so that it is constrained on the function and that it can deal seamlessly with numerical and interval values. Algorithm 6 presents primary routine of the sliding window for computing updates of bounded unary temporal operators OP . The algorithm exploits an additional data structure W that is a deque, such that new elements of the window are added at the end, and such that when the window is saturated (i.e. the elements inside denote a time span bigger than the definition interval of the operator), they are removed from left and propagated as updates. The logic of the algorithm is essentially the following: for each update received in input, the sliding window is initialized on the fragment of the robustness signal of the subformula defined by the update ripple function . For each piece of the fragment, the sliding window is updated (line 10), and each time the new piece makes the data in the window exceed the maximum size, the sliding window slides to the right, removing from the window some elements that can be safely propagated as updates (line 8); some edge cases are not covered to keep the algorithm concise (e.g. the case when the current piece is by itself wider than the window size). The precise behaviour of SLIDE and ADD, that control the mutation of W can be examined in the extended version of the paper or in the Moonlight implementation. The second fundamental temporal algorithm is the one for computing the unbounded until. Unfortunately, being unbounded, any update might require to recompute, in the worst case, the whole robustness/satisfaction signal. In our implementation, we consider the algorithm in [7]. Note that it requires to keep the minimum value of preceding computations of 1 and the maximum value of preceding computations of the whole formula as secondary data structures. A last remark about the implementation must be made: while the algorithms have been developed with the goal to enable out-of-order execution, all of them have been implemented also in an in-order variant, so that the execution time penalty from not assuming that updates are at the end, does not affect the users of the tool, when the use case of interest allows to.

EXPERIMENTAL EVALUATION
The interval semantics we presented in Section 3 and the online (in-order and out-of-order) monitoring strategies of Section 4 have been implemented as extensions to the Moonlight tool. To showcase the kind of applications where they can be exploited, and to compare the performances with other state-of-the-art approaches, we propose here three different examples: (i) we present and discuss the results of the properties previously introduced, in the context of air quality monitoring; (ii) we compare the performances of our approach for the evaluation of a temporal property on the Abstract Fuel Control Simulink model from the Breach [9] tool; (iii) we compare the performances of the online approach versus the offline version of Moonlight on a simulated sensor network adopting the ZigBee protocol. All the computations have been executed on an Intel ® Core ™ i7-5820K CPU @ 3.30GHz, 15M cache, 6 cores (12 threads), with 32GB RAM, running Ubuntu ® 20.04.2 LTS, and Matlab ™ R2021a.

Use case: Air pollution monitoring
Recalling Properties 1, 2 from Section 3, we can see in Figure 4 the results of the monitoring. Note that when both the upper and lower bounds are below the 0 threshold, the property is certainly violated, while when only the lower bound is below 0, then the property is potentially violated. Property 1 gives some important insights on the faults observed in Figure 1. In fact, we can see that of the six observed failures for the ten-days span of interest, only three happen for a time that is long enough to potentially trigger public concern, which correspond to the spikes to minus infinity in the lower bound of Figure 4 (left). In essence, with the interval semantics we learn that the property could potentially be violated in those timespans, while it is certainly not for the other missing values. However, Property 2 tells us something more about the neighbourhood: in fact, by combining the observations registered from close location, it is apparent that just one of the failures (the one happening during March 20th) likely corresponds to a violation of the property, since there is no close location exhibiting low levels of nitrogen dioxide in Figure 4 (right).

Online comparison: Abstract Fuel Control
Consider a Simulink ® model that describes a black-box representation of an engine's air-fuel ratio controller aimed at complying to emission targets of a vehicle, where the user has direct control over the engine speed and pedal angle. Each input and output is represented as a signal that is sampled regularly, the outputs being the actual air-to-fuel ratio (AF), and the mean air-to-fuel ratio value for the given input parameters (AF ref ) at a sampling period = 0.1 . For a full description of the model, the reader can see [16], while [7] provides the reference implementation for online monitoring in Breach.
In our experiments, we monitored the following STL property (note that STREL is an extension of STL, and therefore each STL formula is also a STREL formula) = G [10,30] for different sample sizes, considering both updates as an order chain and by shuffling them at random to simulate out-of-order retrieval and processing. The result of | − | from the model has been stored in a file and loaded before starting the stopwatch for both monitors, to eliminate the simulation and loading time from the performance evaluation. Breach monitor has been measured via the reference implementation as a Simulink model, while Moonlight is implemented as a Java program. Table 1  The interesting insight of the comparison is the fact that, while our in-order implementation provides reliably faster performances (note that the offline version of Moonlight had already shown better performance than Breach in [2]), the penalty that comes from not assuming ordered inputs grows substantially with the increase of the input size, as this requires longer searches in the output signal, to find the spot where the update should be applied. Nevertheless, the biggest sample size we considered is quite extreme (ten thousand randomly-shuffled samples), yet the execution time (4.489 ms/sample on average) is way smaller than the sampling time (0.1 s), which therefore makes it reasonable for most real-time scenarios.

Moonlight comparison: ZigBee Protocol
Consider a collection of moving devices communicating via the ZigBee (IEEE 802.15.4) protocol. From the protocol description we know that the devices can have three roles: they can either be coordinators, routers or sensor-node. Each device is equipped with an humidity sensor ℎ( ) that reports at each time instant the observed value of the humidity at the current location. The humidity observed can be described as an MA(0) process, i.e.
where the observed value comes from the real value 0 , with some perturbation from the zero-mean white noise of variance 2 . Each device can communicate with the ones that are close enough directly, but they can also communicate with furthest ones, as long as there is some router between them that can bridges the communication. Let denote the true value of humidity for a given device at a given time, let denote the role of a given sensor, and some time threshold to warn the observers. We monitored the following properties on the system: 2 = <10 ( = coordinator) Property 1 denotes an alert condition: if the humidity measured by a device goes beyond 60%, then it must fall down at 30% afterwords, within the time threshold . Property 2 , on the other hand, defines a reachability criterion between the sensors: it checks whether it is true that from any location, it is possible to reach a coordinator ( = coordinator) in less than 10 hops. Similarly to previous versions of this model [1,6], we can consider the spatial model as a graph where all the devices are the nodes, and the edges between the nodes are all labeled by = 1 to denote the networking hop from one device to another. Table 2 shows the difference in monitoring 1 and 2 both online and offline. It is interesting to see how the different algorithms behave on same formula and data: in fact, the online temporal algorithms are penalized by the complexity added by the fact that some values must be recomputed. Conversely, the online spatial ones benefit from the hypothesis of spatial synchronization of the locations, resulting in a slightly more efficient computations in the case we explored. Lastly, it can be seen that the benefit of parallelization is particularly evident when the number of nodes is strictly smaller than the number of cores of the CPU (10 in our case), while the benefit practically vanishes (actually resulting in more overhead) as the number of parallel threads grows significantly more than the cores available.

CONCLUSIONS & FUTURE WORK
We extended the traditional definition of signals to also consider imprecise signals defined by intervals of values. We presented an interval semantics for STREL, we proved its soundness and correctness, and we introduced an online monitoring algorithm for STREL that exploits imprecise signals that can be refined by updates arriving in any order, and that can monitor updates on different locations in parallel. We implemented the proposed methodology in the Moonlight monitoring tool. We motivated our framework from an air pollution control specification with real data from the region of Lombardy, Italy. Lastly, we compared the new methodology with other state-of-the art tools, and discussed the differences. Many directions of future work can be followed, for example, the space-synchronization hypothesis helped us simplifying the implementation of the algorithms, but is not needed from a theoretical point of view. It will be interesting in the future to clearly assess the computational advantages and disadvantages of that hypothesis, and to which extent it can be relaxed. Another intriguing topic for future development concerns spatial models representing (and interacting as) distributed systems. In that context, multiple directions could be pursued, like considering an ownership model for the atomic formulae, or by reasoning on an actor-based communication model among locations. Another interesting idea could be to expand the kind of failures we can monitor, for example, we could consider some form of error correction in case some received updates later prove to have provided wrong information (maybe because of some broken sensors). Lastly, different form of computational optimization could be explored, like stopping when some bounds on the satisfiability/robustness have been reached, as well as intensive parallelization and hardware acceleration of the main algorithms.


An Intelligent Code Search Approach Using Hybrid Encoders

The intelligent code search with natural language queries has become an important researching area in software engineering. In this paper, we propose a novel deep learning framework At-CodeSM for source code search. The powerful code encoder in At-CodeSM, which is implemented with an abstract syntax tree parsing algorithm (Tree-LSTM) and token-level encoders, maintains both the lexical and structural features of source code in the process of code vectorizing. Both the representative and discriminative models are implemented with deep neural networks. Our experiments on the CodeSearchNet dataset show that At-CodeSM yields better performance in the task of intelligent code searching than previous approaches.

Introduction
In the modern world, the application of computer software has already penetrated every aspect of our lives. The necessities of life, such as medical care, resources, transportation, and public security, depend on the running of high-quality software. For code quality and efficiency, programmers repeatedly involve successful code snippets developed by other authors. It has been a key task in the field of software engineering to locate target code snippets, which are returned by natural language queries, in code repositories such as GitHub and SourceForge.
The traditional code search algorithms are mostly implemented with information retrieval methods, which are widely used in the field of natural language processing. These approaches usually treat the source code as a plain text or a sequence of tokens, and then return the related code snippets by computing the similarity of queries and code documents. The token-based code search toolkits have been already used in industry, e.g., Sourcerer and Krugle. They treat both the query words and code snippets in codebase as plain text and return the target codes by key wordmatching or template-matching technology. In the academic area, McMillan et al. propose a searching model Portfolio [1], which returns a chain of functions through keyword matching and the PageRank algorithm. Lv et al. developed a famous code-searching engine CodeHow [2], which com-bines text similarity and API matching through an extended Boolean model.
Source code search algorithms based on text retrieval strategy often fail in practice. Different from plain text, code snippets usually contain both the structural and semantic information. The source code snippets made by programmers and queries written in natural languages are essentially heterogeneous. They may not share common lexical tokens, synonyms, or language structures. Sometimes programmers are extremely unsatisfied with searching results from traditional information retrieval algorithms. To improve code search according to natural language queries, researchers tend to use various code representations. They construct different code encoders with machine learning methods, which map source code and query words to the same vector space. The most related code vectors are returned as searching results according to the distance [3] between adjacent vectors.
In recent years, with the rapid development of deep learning technology, researchers in the field of software engineering begin to analyze the structural and semantic features of source code with deep learning approaches. Based on the common neural networks such as the convolutional neural network, the recursive neural network, and the recurrent neural network, scholars exploit various deep encoders to represent source code in different vector spaces [4][5][6]. Compared to traditional approaches, deep neural networks can extract the structural and semantic information hidden in the source code snippets during code embedding, which might improve the representation ability of code vectors.
In this paper, we propose a novel source code search model using deep learning algorithms. The model maps both the code snippets in the codebase and natural language queries to the same high-dimensional vector space and then return the most related code snippets by computing the cosine similarity between code vectors and query vectors. Different from previous research, At-CodeSM vectorizes the source code with three independent encoders, e.g., the method name encoder, the lexical encoder, and the structural encoder. The lexical encoder extracts the tokens from the source code and encodes them with an attention-based LSTM network. The core tokens are strengthened with heavy attention scores. The structural encoder firstly transforms the source code into an AST, and then encodes the whole tree using a tree-LSTM network in a recursive way. The combination of three encoders in At-CodeSM retains both the lexical and syntactics of code in the process of representation, which improves the searching performance.
In practice, At-CodeSM firstly updates the parameters of the source code encoder and query encoder by offline learning on the training set. It then conducts an offline embedding on all the code snippets in the search base. Finally, At-CodeSM uses an online matching algorithm to compare the cosine similarity between the query vector and code vectors from the search base. The code snippets with higher similarity scores are returned as the searching results.
The main contributions of this work are as follows: (i) We propose a novel source code representation model based on the deep neural network. The model implements the encoding of method name, method body, and method grammar tree, respectively, with three independent encoders. Compared with other models, the representation process in At-CodeSM effectively retains both the lexical and semantic characteristics of the code snippets (ii) To our knowledge, we are the first to introduce a self-attention mechanism, which was developed in NLP, into the area of intelligent code search. With the self-attention mechanism, key words in the source code are strengthened, which finally improve the searching performance (iii) The big achievements are made when we apply our representation model in the intelligent code search area. We improve the model parameters with supervised learning on a large-scale dataset Code-SearchNet, which is made by Microsoft. The experiments show that our model is superior to the state-of-art approaches The remainder of this paper is organized as follows: Section 2 describes related work in the code search area. Section 3 presents background materials of various LSTM structures and the self-attention mechanism. Section 4 elaborates on the details of At-CodeSM. Section 5 gives the experiment and evaluation. In Section 6, we discuss the crucial factors which may affect the searching performance. Finally, we conclude the paper in Section 7.

Related Work
2.1. Traditional Approaches. Using common NLP methods, most traditional code search approaches treat source code as plain text or a set of tokens, ignoring its structure and semantics. Such models often extract code features manually or with NLP methods, and then return related code snippets via a text similarity algorithm [7,8]. Mostly applied in the early stage, these models completed simple search tasks with keyword matching. Due to the low complexity and crossplatform features, these approaches have been widely used in industry. For instance, Lucene is a successful code search platform implemented with traditional approaches.
In 1993, Chang and Eastman [9] proposed a famous code search tool SMART, which was based on keyword searching. SMART identified the code snippets as token sequences and then returned the target code according to a common keyword-matching algorithm. The early SMART model implemented an exact matching algorithm on keywords. Inspired by SMART, software companies such as Google and GitHub improved matching strategies in their code search tools with fuzzy search algorithms.
People began to study different matching algorithms for code search performance. LV et al. [2] proposed CodeHow, which transformed the queries into corresponding APIs. The target code was returned by API matching in codebase. Reiss et al. [10] presented a semantic search engine, which improved the searching performance by filtering unrelated code snippets. The structural semantic indexing model proposed by Bajracharya et al. [11] could establish the connection between natural language queries and source code keywords.
Marcus et al. [12] attempted to introduce Latent Semantic Analysis (LSA) into the field of code search. Their model made a good achievement by semantic code analysis. Inspired by a previous study, Jiang et al. [13] proposed ROSF, which combined IR and supervised learning technology during code embedding. It performed well in the task of code search when applying multiple structural extraction approaches.

Deep Learning Approaches.
With the development of deep learning theory, people tend to solve problems in every field with deep learning approaches [14][15][16][17][18]. In recent years, researchers in the field of software engineering have introduced deep neural networks [19][20][21][22] such as multilayer perceptron network, recurrent neural network and convolutional neural network to solve the problems. The researchers carefully update their models with supervised or unsupervised learning on large-scale datasets. The neural network model through supervised or unsupervised training. Compared with previous coding encoding algorithms, deep neural encoders can automatically extract the structural and semantic features hidden in the source code.
Iyer et al. [23] presented LSTM networks with attention to produce summaries that describe C# code snippets and 2 Wireless Communications and Mobile Computing SQL queries. Their model codeNN is built on a classical encoder-decoder framework, which takes the source code as plain text and models the conditional distribution of the summary. Allamanis et al. [24] applied a neural convolutional attentional model to vectorize the source code snippets. These learning-based approaches mainly learn the latent features from source code with neural networks. Gu et al. [25] proposed a code search model called codeNN with complicated neural networks. Inspired by joint embedding in the image processing field, codeNN treats the code snippet as a combination of function names, API calls, and a sequence of tokens. The code encoder is implemented with bi-LSTM and MLP networks. They build their own dataset by collecting Java source code snippets from GitHub. The first sentence of the code comment is identified as the data label. The typical questions posted on StackOverflow are accumulated as the queries in the test set, and corresponding code snippets for each query are also collected with other code search engines. The matching scores between snippets and queries are judged by experts. The construction of datasets and evaluation methods have been used by scholars for contrast experiments. codeNN makes full use of the structural characteristics of source code in the process of code encoding. It outperforms the classical code search engines Lucene and CodeHow. Although inaccurate results might be returned, or partial-related items are ahead of exact matching ones in the result list, it is still the most effective code search method right now. Cambronero et al. [19] reconfirmed this ranking in their latest review in 2019, but they declared the complex network structure also resulted in low embedding efficiency.
The searching models with unsupervised learning has attracted the attention of researchers for lack of labeled data, although their performance might not match one with supervised learning models. Sachdev et al. [3] trained their search model on large-scale corpus with unsupervised learning. The model encodes all the snippets in a codebase with common document embedding and TD-IDF techniques, and then returns related code vectors according to a specific vector similarity algorithm.
The famous pretrained model BERT [26], which was proposed in 2018, has played an important role in wordembedding techniques in the area of NLP. Researchers Kanade et al. [27] were the first to introduce BERT into the field of code retrieval. The contrast experiments show that their model with BERT embedding outperforms searching models based on LSTM networks with word2vec embedding. They declare that their pretrained model also outperforms the Transformer [28], which is trained from scratch.
Recent scholars manage to improve the models' searching ability by intensifying the expressiveness of queries [29][30][31]. Programmers often apply code search with few words for simplicity so that queries lack semantic information, which fails to meet the requirements of developers. In 2019, Liu et al. [32] proposed a NQE model which is capable of enlarging query words. The query enhancer in the model inputs a small number of query keywords and outputs an extended query statement with new words. The searching models are trained on a specific corpus with supervised learning. Experiments show that the searching performance is obviously improved by the query enhancer in NQE.

Preliminaries
In this section, we briefly give some well-accepted definitions in the area of source code search and deep learning.
3.1. Abstract Syntax Tree. Abstract syntax tree is a kind of syntax tree representing the abstract syntactic structure of the source code. It has been widely used by programming compliers and software engineering tools due to the powerful representation ability. Different from concrete syntax trees (CTS), abstract syntax trees do not contain all the details of source code such as the punctuation and delimiters. They only include the syntax structure of the source code at an abstract level. AST contains both the lexical and syntax information of the source code, which is often employed in the industry as an intermediate tool to extract the hidden information Figure 1 is the structure of an AST. Nodes of the AST correspond to the constructs or symbols of the source code. We conclude from the graph that the AST fully retains the structural information of the source code.

Attention.
The attention mechanism is the internal process for machines to imitate the human observation of things in the world. When processing images, our vision quickly obtains the target area by a global scan, i.e., the focus of attention. Then, the brain pays more attention to the focus area for details, while suppressing irrelevant information.
Bahdanau et al. [33] firstly applied the attention mechanism in the field of machine translation, i.e., sequence to sequence learning. He successfully solved the problem of long-term dependency in machine translation, i.e., the translation models based on fixed vector representations often lost history information of long sentences in the decoding process. After that, people began to study deep encoders with attention layers, which achieved amazing effects in all areas of NLP.
Mathematically, the attention is essentially a mapping function composed of Query, Key, and Value. The calculation of attention values is divided into three steps: Step 1. Query is combined with each Key to calculate the attention weight. The similarity function f ðQ, KÞ can be defined in multiple ways. The simplest calculation is shown as follows: Step 2. The softmax function is used to normalize the attention weight obtained in Step 1, as shown in equation (2). Sometimes, we have to scale the attention scores later as the original ones are too large to calculate: Step 3. The final attention is the weighted sum of normalized weights a i and corresponding values, which is shown as follows:

Wireless Communications and Mobile Computing
The attention mechanism is widely used in RNN-based encoder-decoder models. The input of the decoder's current state is determined by the weighted average of all hidden layers' output values in the encoder. The attention algorithm is transformed to the self-attention algorithm when Q = K = V in the encoder [28]. Our lexical encoder in At-CodeSM is implemented with a specific self-attention LSTM layer.

LSTM Networks.
Recurrent neural networks (RNN) can process input sequences of arbitrary length via the recurrent structure with shared weights. Unfortunately, a common problem with the traditional RNN is that components of the gradient vector can grow or decay exponentially over long sequences during training. Therefore, the LSTM architecture [34], which was invented by Hochreiter and Schmidhuber in 1997, addresses this problem of learning long-term dependency by introducing a memory cell that is able to preserve states over long periods of time. The core part of the LSTM is a cell memory C t , including an input gate i t , an output gate o t , and a forget gate f t . Figure 2 describes the basic structure of LSTM. Different from the original RNN, the LSTM solves the problem of long-term dependency effectively with the special structure memory cell, discarding the trivial information in the history to avoid the gradient vanishing.
The cell memory of LSTM is composed of three gate controllers. The forget gate f t controls the extent to which the previous memory cell is forgotten, which is essential a sigmoid function. The entry of f t is a weighted combination of the previous output value and the current input value. The input gate i t controls how much each unit is updated, and the output gate o t controls the exposure of the internal memory state. The LSTM transition equations are the following: where W i , W f , W o are the weighted matrices, and b i , b f , b o are the biases of LSTM to be learned during training, parameterizing the transformations of the input, forget, and output gates, respectively. σ and tan h are the activation functions, and • denotes the element-wise multiplication. x t is the input of the LSTM cell unit, and h t is the output of the hidden layer at the current time step. In order to deal with structural data, Tai et al. [35] invented tree-based LSTM networks (Tree-LSTM) from the standard LSTM networks. Figure 3 shows the difference between standard LSTM and tree-LSTM networks. Figure 3(a) is the common LSTM network designed for sequential data, while Figure 3(b) is the tree-LSTM network used for structural data. Unlike traditional LSTM networks, tree-LSTM contains an output and n inputs at time step t, for which it is convenient to handle data stored in trees. Normally, it is used for binary trees when n = 2. The updating equations of tree-LSTM are detailed in Section 4.2.3.

Our Proposed Approach
4.1. General Framework. In this section, we detail the workflow of At-CodeSM, which is summarized in Figure 4. It contains a source code encoder E c and a query encoder E q . E c maps the source code into representation vectors with a neural network, while E q maps the queries written in natural languages into vectors with another neural network. Both encoders are trained with supervised learning on large corpora.

Wireless Communications and Mobile Computing
The code search usually contains an offline data preprocessing and an online search. In the process of offline data preprocessing, At-CodeSM updates E c and E q on the training corpus, and then apply an offline embedding on the search corpus with E c . All the snippets in the search base are transformed to code vectors. In the process of online search, E q firstly encodes the users' query, and then matches the query vector with each code vector on the search corpus. The top k snippets are returned as search lists according to the cosine similarity between vectors. All the encoders of At-CodeSM are detailed in the following subsections.

Source Code Encoder.
As the core component of our model, E c applies lexical embedding and structural embedding, respectively, during encoding process, so that the output vector maintains both the structural and semantic characteristics of the source code. Figure 5 shows the structure of the source code encoder. It is a combined model, which includes a method name encoder, a lexical encoder, and a structural encoder. The method name encoder inputs the full name of the function and output a representation vector V name . The lexical encoder inputs the body of the function and outputs a representation vector V token . The structural encoder outputs a representation vector V ast by embedding the corresponding AST with a specific traversal algorithm. Finally, V name , V token , and V ast are fused into a unified vector v c through a fully connected layer in At-CodeSM.
We present all the encoders in the following sections.

Lexical
Embedding. The body of source code methods contains many core words which describes the functionality. During lexical embedding, At-CodeSM extracts core tokens from the method body, and then embeds them with common word-embedding technology in NLP by treating the source code snippets as plain texts. Finally, the output vector is generated with an attentional LSTM network. We use an independent attention layer at the back of lexical encoder, as the contribution of each token varies in implementing the functionality. The process of lexical embedding is divided into three steps: (1) Data preprocessing: in order to collect tokens from a Java method, we tokenize the method body and split each token according to a camel case, e.g., change-ToPDF and parseXML. All the duplicated tokens, stop words, and Java keywords are removed as they frequently occur in source code and are not discriminative (2) Token embedding: let T = ftoken1, token2, token3, ⋯g denote the sequence of tokens from source code after step (1). The lexical encoder includes a transformation f , which makes f ðtoken1, token2, token3, ⋯Þ = v token1 , v token2 , v token3 , ⋯. By contrast, we implement the transformation f with Word2vec [36].
(3) Source code vector generation: the sequence of token vectors v token1 , v token2 , v token3 , … are loaded into a standard bi-LSTM. Equation (5) shows the calculation of LSTM, where h t ! and h t denote the forward and backward hidden status at step t, and h t is the However, the effect of each token is different in high-level programming languages, e.g., the token XML is more important than other tokens in a method dealing with the data storage in XML files. In this paper, we attempt to introduce the self-attention algorithm in the process of lexical embedding. To our knowledge, it is the first time to use attention mechanism in the field of code search. Since our model only includes the encoder, we decide to use the self-attention algorithm. The attention scores can be calculated in many ways as there are various definitions of similarity function. In our paper, equation (6) and equation (7) are used to calculate the attention scores, which are defined in [37]: where h i denotes the hidden states of the bidirectional LSTM, K denotes a context vector which is initialized randomly. Hu et al. [38] indicates that the inner product of h i and K denotes the contribution of h i to the source code vector. The value of K is updated continuously with other parameters via supervised learning. α i denotes the ith attention score, corresponding with the hidden state h i . v token is the representation vector of the given code fragment, which is generated by the weighted sum of all the hidden states. Figure 6 shows the encoding process with the self-attention layer.
x t x + Tanh x Tanh The method name is a description of the method functionality, which is composed of a small amount of keywords. Early code search algorithms apply a simple keyword matching between queries and method names. At-CodeSM uses an independent encoder for the embedding of method names, which is simpler than lexical embedding. Let T = fname1, name2, name3, ⋯g denote the sequence of small names extracted from the method name; after that, the encoder applies a transformation f , which makes f ðname1, name2, name3, ⋯Þ = v name1 , v name2 , v name3 , ⋯ with Word2vec technology. Finally, At-CodeSM outputs the representation vector for the method name with a bi-LSTM network, which is shown as follows: where h mt ! and h mt are the forward and backward hidden states of the bi-LSTM, v name is the final semantic vector of the method name, generated from the concatenation of h mt ! and h mt . We tried to implement self-attention in the embedding layer, which had no performance improvement by experiments. Experimental results with various selfattention layers are discussed later.

Structural Embedding.
We employ javalang to generate an abstract syntax tree (AST) from the source code snippet. The structural encoder then transforms the AST into a high-dimensional vector V ast according to a specific AST traversal algorithm. Recent researchers have proposed several AST embedding algorithms, e.g., RvNN embedding algorithm [6], structure-based algorithm (SBT) [38], tree-LSTM embedding algorithm [35], and tree-CNN embedding algorithms [39]. We implement the structural encoder in At-CodeSM with a special tree-LSTM embedding algorithm, which is used by Hu et al. in their code clone detector CDLH. Tai et al. proposed the tree-based LSTM networks, which is used for the embedding of ASTs in CDLH. Different from standard LSTM networks, neural cells in tree-LSTM contain several forget gates, each of which corresponds with an input. The transition equations for tree-LSTM are the following: Figure 3: Comparison between standard LSTM and tree-LSTM. 6 Wireless Communications and Mobile Computing where x is the embedding of the corresponding token, L denotes the number of children, f l are L forget gates for the children of the AST node, l is the index number for its children, r is a control variable for the output, W i , W f , W o , W u , U il , U f l , U ol , and U ul are weight matrices, and b i , b f , b o , b u are bias vectors. ⊙ denotes the element-wise multiplication, and σ is the sigmoid function.
The original ASTs generated from source code might have multiple branches. The classical tree-LSTM networks can be used for the embedding of ASTs with multiple branches. The number of children L varies for different AST nodes, which might cause problems in the parametersharing of weight matrices. We transform the original ASTs into binary trees, whose nodes contain 0 or 2 children.
The transform algorithm for binary trees is divided into two steps: (1) We split nodes with more than 2 children and generate a new right child together with the old left child as its children, and then put all children except the leftmost as the children of this new node. Repeat the operation in an up-down way until only nodes with 0, 1, and 2 children are left (2) The nodes with 1 child are merged with its child After transformation, the AST is transformed into a full binary tree, nodes of which contain 0 or 2 children. Figure 7 describes the transformation of a subtree. The binary tree on the right part of the figure is transformed from the left one, and node 6 and node 7 are generated after two splits.
For implementation, we input the embeddings of the two children into the Tree-LSTM networks, and the hidden state for each internal node is computed recursively in a bottomup way. The final output from the AST root V ast is the representation for the code snippet.  In practice, programmers input queries in the repositories for code search. In the training process, the query encoder is updated with target descriptions. Both queries and descriptions are a sequence of natural language words. The lower part of Figure 5 describes the structure of the query encoder equation. The process of query embedding is similar to the embedding of method names in source code. The query encoder transforms a sequence of tokens to a sequence of vectors v query1 , v query2 , and v query3 with word-embedding technology. Finally, the embedding network embeds this sequence of vectors into a query vector using bi-LSTM, which is shown as follows: where h qt ! and h qt are the forward and backward hidden  Figure 5: The structure of source code encoder and query encoder.

Wireless Communications and Mobile Computing
states produced by the final layer of LSTM in the query encoder, and v query is the output vector of the query sentence. We tried to add a self-attention layer in the query encoder, which had no performance improvement by experiments.

Loss Function.
In this section, we present the loss function used in At-CodeSM. With carefully trained encoders, and At-CodeSM maps both the source code and queries to different vectors in a unified vector space. The goal of training is as follows: if a code snippet and a description have similar semantics, their embedded vectors should be close to each other. In other words, given an arbitrary code snippet C and an arbitrary description D, we want it to predict a distance with high similarity if D is an exact description of C, and a little similarity otherwise. We build each training instance as a triple hC, D+,D − i for supervised training. For each code snippet C, there is a positive description D + (correct description) and a negative description D − (false description) randomly chosen from the collection of other D + . In the training process, the search model predicts the cosine similarities of both hC, D + i and hC, D − i pairs and minimizes the ranking loss [40], which is defined as follows: where θ indicates the model parameters, P indicates the training corpus, ϵ is a constant margin. c, d + , and d − are the embedded vectors of C, D + , and D-, respectively. The lost function LðθÞ encourages the similarity between a code snippet and its correct description to increase, and the similarity between a code snippet and its false description to decrease.

Bidirectional LSTM
Token embedding layer

Evaluation
Metrics. The objective of code search models is to locate suitable code snippets in code repositories. They often return many results based on similarity algorithms due to the big capacity of codebase. In most cases, developers only focus on the snippets ahead in the result list. In our experiment, we select MRR and NDCG as evaluation metrics which are often used in the field of information retrieval [2,25,41,42], to compare the performances of At-CodeSM and other baselines.

Experiments
All the experiments are conducted on a server, having a CPU of 16 cores with GPU acceleration. The framework is built on python 3.6 and CUDA 9.0. All the tokens are embedded using word2vec with the Skip-gram algorithm, and we set the embedding size to be 128.
The standard LSTM and tree-LSTM networks are used to build the encoders, respectively, where the hidden dimensions are set to be 128. We use SGD to train the model and set Batch_size to 64. We employ the optimizer Adam with a learning rate of 0.005 to train the model.

Dataset Preparation.
There are very few public datasets for source code search as it is very difficult to collect exact descriptions for code snippets in the code repositories with massive code data. Especially, the similarity scores between code snippets and queries should be judged by experts, which might cause human bias. Researchers usually construct three datasets for contrast experiments in code search area.
(1) Training corpus: it refers to a dataset of paired code and the natural language description. A common example for the natural language description could be the code snippet's corresponding docstring. A training corpus is used to update the searching models with supervised labeling. Unsupervised learning models use only code snippets from the training corpus (2) Search corpus: it refers to a dataset of unique code entries after data preprocessing. Entries are unique to avoid repetition in search results. Code search engines take effort to apply an offline embedding on each code snippet in the search corpus with their code encoders before an online search. Data in the search corpus are not necessarily like the ones in training corpus. Sometimes, code snippets in the search corpus might not be paired with descriptions (3) Testing corpus (benchmark queries): it refers to a set of evaluation queries and corresponding code snippets used to gauge the performance of trained models. It is defined as Depending on the size of C i , testing sets generally fall into two categories in code search: (a) Each test case includes a query and a corresponding code snippet, i.e., ∀query i , jC i j = 1. These test cases can be automatically collected and evaluated. However, due to the complexity of the code structure, it is possible for search engines in prac-tice to return heterogeneous code snippets with the same functionality, e.g., type 4 clone pairs. These correct cases are probably identified as "false." The evaluation for code snippets with similar functionality, which are returned by search engines, will lose effectiveness (b) Each test case includes a query and several corresponding code snippets, i.e., ∃query i , jC i j > 1.
Test cases of this kind successfully solve the problem of code snippets with similar functionality but different shapes. Based on these test cases, we can evaluate the search engine's performance with traditional methods in the IR field. However, it is difficult to find all the target snippets related to the same query and judge the relatedness between them. Recent scholars manage to collect similar code snippets according to the same query by various search models, and the relatedness scores are often obtained manually. Hence, the testing corpus does not have a large capacity. We believe that the problem of collecting test cases will be solved with the development of deep learning methods in the field of source code clone detection [3,43] build their own datasets by collecting source code from code repositories, due to the lack of public datasets for code search and summarization. In order to solve the problem, Microsoft Cambridge Research Center and GitHub company released a large-scale dataset CodeSearchNet [44] for machine learning in 2020. The dataset contains more than 6 million code snippets extracted from GitHub, an open-source code repository with massive code data, among which more than 2 million snippets are commented methods. The code extraction is applied according to "popularity" as indicated by the number of stars and forks in GitHub. The dataset authors generate the label for each code snippet by extracting the first sentence from its comment. Table 1 shows the data in Code-SearchNet, which are grouped by programming language. These labeled data on the second column of Table 1 can be used for code search and code summarization tasks. We conduct contrast experiments on the Java subset. The dataset for java in CodeSearchNet is split in 80-10-10 train/valid/test proportions after data preprocessing. We use the labeled java dataset as the search corpus, the original training set as our training corpus. Figure 8 shows the partition of Java dataset in our experiments.

Dataset Description. Previous researchers
At-CodeSM and other baseline models are evaluated with two different testing sets, which are described in Section 5.1: (1) Test A: we apply an automatic testing on the Java testing set from CodeSearchNet. Table 1 shows that the Java testing set contains 26909 methoddescription pairs. The experimental results are unbiased due to the exclusive partition of training and testing sets [45]. We calculate the MRR values of all the searching models in Test A

Wireless Communications and Mobile Computing
(2) Test B: expert scoring are employed in the evaluation of ranking models in order to cope with heterogeneous code snippets with similar functionality. Experts score each item in the result list by the relatedness between the snippet and query. Traditional IR-based methods such as NDCG are then applied for evaluation depending on the matching scores. Test B is rarely used by researchers due to the luxury manual work. Hence, the authors of CodeSearchNet construct a new dataset called CodeSearchNet Challenge for code evaluation. It is defined as fD i , hC in , R in i | i = 1, 2, ⋯, 99 ; n = 1, 2, ⋯, 100g, where D i denotes the description or query, C in is a corresponding code snippet according to D i , R in is a matching score between C in and D i given by experts CodeSearchNet Challenge contains 99 natural languages queries paired with likely results for each of six programming languages. All the queries are obtained from the famous search engine Bing with high click-through rates, each of which contains around 10 corresponding code snippets, returned by baseline code search models. Every query-result pair is labeled by a human expert, indicating the relevance of the result for the query. Table 2 shows some examples in CodeSearchNet Challenge. Table 3 shows the criterion of relevance followed by experts.

Contrast Experiments.
We compare At-CodeSM with three baseline models in the field of source code search by different experiments on CodeSearchNet dataset: (1) NBoW model (Neural Bag of Words) [45]: as a classical code search model, NBoW has already been implemented in CodeSearchNet. It applies code embedding with common NLP methods by treating source code as the plain text. The tokens extracted from the code snippet are embedded with a transformation matrix, which is updated by training. The representation vector for the code snippet is generated by a max-pooling function over all the token vectors. NBoW implements the query embedding with the same embedding algorithm. Finally, NBoW returns the most related code snippets in the vector space as search results with a similarity algorithm between vectors (2) NCS model (Neural Code Search) [3]: built in Facebook, NCS generates the representation vector of the code with a combination of token-level embedding with fastText [45], which is similar to Word2vec, and conventional IR techniques, such as TF-IDF. The encoders of NCS are not implemented with conventional deep neural networks nor supervised training (3) CODEnn model [25]: all the encoders in CODEnn are implemented with complicated neutral networks, compared to former baselines. CODEnn includes three encoders for method names, APIs, and method body, respectively. The encoders for method names and APIs are implemented with a standard LSTM, while the lexical encoder uses a simple MLP for the embedding of method body. Finally, CODEnn outputs a unified vector by merging three subvectors through a MLP layer. For query embedding, a bi-LSTM network is employed to process the sequence of token vectors extracted from the query sentence. CODEnn returns the result list according to the cosine similarity algorithm. Unlike NCS, authors of CODEnn update their model with supervised learning. The labeled data are collected from code repositories by themselves. The authors provide the framework of CODEnn in GitHub, which we use for our contrast experiments on CodeSearchNet Figure 9 shows the experimental results of At-CodeSM and baseline models on the test corpus of CodeSearchNet. The figures above the bars are the MRR values of search models, which are the rank of the first hit results. We see that the search performance of CODEnn and At-CodeSM, which is evaluated by MRR, is much higher than the former models.

Discussion
In this chapter, we take a detailed discussion about the performance of At-CodeSM and other code search models based on ablation tests. We try to find the key components which affect searching accuracy by further experiments.
6.1. Comparing with Baseline Models. Compared to other baseline models, we conclude from the contrast experiments that At-CodeSM model outperforms the other models in both MRR values, which are generated from automated testing, and NDCG values which are generated with manual evaluation. NCS model encodes the source code with common NLP methods. The unsupervised learning has a negative influence on the searching performance, although unlabeled data are easily collected. Figures 9 and 10 show the poor performance of NCS, of which the searching accuracy and ranking in the result list are lower than codeNN and At-CodeSM. The performance of NBoW is not ideal, because its code encoder ignores both the sequential information of tokens and structural information in source code.
CodeNN is a successful code search model trained with supervised learning. It introduces deep learning technology into the field of code search. It makes great achievement in source code search by using a combination of method names, tokens, and APIs during code embedding. Inspired by codeNN, we propose the At-CodeSM model. The performance of our model is slightly better than codeNN. We guess it is the introduction of self-attention and tree-LSTM networks that improve the searching performance. The core words are strengthened with a self-attention mechanism, which highlight the behavior and logic hidden in function bodies. The AST encoder in our model, which is implemented with tree-LSTM networks, further extracts the structural features hidden in source code, compared to API revocations in codeNN. Both models outperform NCS and NBoW, which only extract lexical features.
6.2. AST Traversal Algorithms. A traversal algorithm for ASTs is introduced in At-CodeSM. The corresponding AST maintains the structural feature hidden in the source code snippet. We use a tree-based LSTM network in the embedding of AST. In the field of software engineering, many AST-based traversal algorithms are proposed, with which corresponding ASTs are transformed to representation vectors.
In order to investigate the effects of the embedding algorithms for ASTs, we conduct contrast experiments on the same dataset, and the results are shown in Table 4. Models in the table are the same except that the structural encoders are implemented with three different traversal algorithms for AST embedding. Model 1 embeds the source code with a combination of the lexical encoder and method name encoder, which ignores the structural embedding completely. Model 2 implements the AST embedding with SBT, which convert the ASTs into special formatted sequences of nodes. A bi-LSTM network is used to generate the representation vector according to the sequence of nodes. The authors of SBT claim the transformation keeps the structural information. Model 3 is an At-CodeSM model, whose structural encoder is implemented with a Tree-based LSTM. We compare both the MRR and NDCG values in Table 4.
Through the above experimental results, it can be observed that model 1 shows the poorest performance, as it fails to extract the structural information hidden in the AST. The search performance of model 2 is slightly inferior to that of model 3. We guess the one-dimensional sequence  Exact match 3 It is exactly what I was looking for. I would copy-paste the code and make minor adaptions or will use this functionality of the library in my code.

12
Wireless Communications and Mobile Computing generated from SBT might lose the structural information of some tree nodes.
6.3. Self-Attention Algorithms. The use of a self-attention layer, which stresses the effect of key words in source clone embedding, is a great innovation in our paper. In this section, we investigate the effect of self-attention layers on the search performance by contrast experiments. Figure 11 shows the experimental data we collect from five code search models, each of which is built on the basic At-CodeSM model. The detailed structure of At-CodeSM is presented in Section 4.2, including three encoders for method names, code tokens, and the code structure, respectively. The structures of these models are the same except the self-attention layers: (1) NoAtt model: it does not include the self-attention layer at all. The vectors generated from three independent encoders are merged via a fusion layer (2) MNAtt model: the self-attention layer is placed at the back of the name encoder, which assigns weights to the tokens extracted from method names (3) StrAtt model: the self-attention mechanism is used during structural embedding. Each node vector is assigned with an attentional weight (4) At-CodeSM model: it is proposed in Section 4. The self-attention layer is used during lexical encoding (5) At-CodeSM2 model: it is a variant of the original At-CodeSM model, where the attention scores are computed according to equation (12). Many formulas are proposed to calculate the attention scores in the NLP field. Equation (12) is a simple implementation for the self-attention algorithm without other model parameters. We want to investigate the effects of various attention algorithms by contrast experiments Figure 11 shows that the self-attention layer greatly improves the search performance of the model. The contributions of different words are various in high-level programming languages. The core words implementing the logical functionality are more important than the normal ones. The encoder with self-attention layers can strengthen the effectiveness of core words and weaken the impact of common words such as variable declaration. Both the MRR and NDCG values of NoAtt substantially fall behind the other models. The performance improvement in MNAtt is not obvious. We guess that all the words extracted from the method name are important, the contributions of which are similar. The performance of StrAtt is close to that of At-CodeSM. However, it takes more time to train StrAtt due to the complicated structure encoder with attention. 40

Wireless Communications and Mobile Computing
We find that the search performance of At-CodeSM and At-CodeSM2 are slightly different. The performance of At-CodeSM is higher when involving an independent parameter K in equation (7). We suspect that the search performance of the second model is slightly affected due to the lack of some adjustments to the input when calculating the attention scores.

Conclusion
In this paper, we have presented a novel source codesearching model At-biLSTM based on deep learning with a self-attention mechanism. It contains a query encoder and three independent source code encoders, which successfully capture both the lexical and syntactic information of the code during embedding. The searching results are returned by computing the cosine similarity between the query vector and code vectors in a unified high-dimensional vector space. Contrast experiments show that our model significantly outperforms most of the existing code search models. We will focus on three aspects in the future. First, the At-CodeSM should be used in large-scale codebase. At present, both the algorithms for clone search and data collected in the labs cannot be applied in the real world. We will study and improve the searching performance of our model in industry. Second, we will focus on the code-embedding technology. In recent years, many pretrained models for embedding have made great achievements in NLP applications. We plan to rebuild our code encoders with BERT, which is the most popular pretrained model in the world. Third, we will make a study of query expansion technology. We plan to add a special component for the expansion of keywords in queries, which might improve the searching performance.
The threats to the validity stem from the datasets used in our experiments. The models are trained on a new dataset called CodeSearchNet which was created by Microsoft in 2020, as the labeled data for code search are difficult to accumulate. The labeled data in CodeSearchNet are collected in the same way as in other datasets. The first sentence of the method comment is identified as the query description, which is far away from the real query in practice. The matching scores for 99 queries are all given manually. The introduction of human evaluation might have a negative influence on searching results when we evaluate the models' NDCG values.

Data Availability
The data used to support the findings of this study are included in the article.

Conflicts of Interest
The authors declare that they have no conflicts of interest.