RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
Jan Baumeister Bernd Finkbeiner Sebastian Schirmer Maximilian Schwenger Christoph Torens
cs.RO cs.SE eess.SP 68V06 B.7.1; F.4.3

Time-stamp
Au-to-no-mous
RTLola


RTLola Cleared for Take-Off




Baumeister et al.
RTLola Cleared for Take-Off

  Saarland University, Department of Computer Science, 

  66123 Saarbrücken, Germany 

  {jbaumeister, finkbeiner, schwenger}@react.uni-saarland.de German Aerospace Center (DLR), 

  38108 Braunschweig, Germany 

  {christoph.torens, sebastian.schirmer}@dlr.de


RTLola Cleared for Take-Off: 
Monitoring Autonomous AircraftThis work was partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center Foundations of Perspicuous Software Systems (TRR 248, 389792660), and by the European Research Council (ERC) Grant OSARES (No. 683300).
    Jan Baumeister10000-0002-8891-7483Bernd Finkbeiner10000-0002-4280-8441 Sebastian Schirmer2 

Maximilian Schwenger10000-0002-2091-7575 Christoph Torens2

    December 30, 2023
==========================================================================================================================================================================================================================================================================================================================




  The autonomous control of unmanned aircraft is a highly
  safety-critical domain with great economic potential in a wide range
  of application areas, including logistics, agriculture, civil engineering, and
  disaster recovery.  We report on the development of a dynamic
  monitoring framework for the DLR ARTIS (Autonomous Rotorcraft Testbed
  for Intelligent Systems) family of unmanned aircraft based on the
  formal specification language RTLola.  RTLola is a stream-based
  specification language for real-time properties. An RTLola
  specification of hazardous situations and system failures is
  statically analyzed in terms of consistency and resource usage and
  then automatically translated into an FPGA-based monitor. Our
  approach leads to highly efficient, parallelized monitors with formal
  guarantees on the noninterference of the monitor with the normal
  operation of the autonomous system.


  













































§ INTRODUCTION



An unmanned aerial vehicle, commonly known as a drone, is an aircraft
without a human pilot on board. While usually connected via radio
transmissions to a base station on the ground, such aircraft are
increasingly equipped with decision-making capabilities that allow
them to autonomously carry out complex missions in applications such as
transport, mapping and surveillance, or crop and irrigation
monitoring.  Despite the obvious safety-criticality of such systems,
it is impossible to foresee all situations an autonomous aircraft
might encounter and thus make a safety case purely by analyzing all
of the potential behaviors in advance.  A critical part of the safety
engineering of a drone is therefore to carefully monitor the actual
behavior during the flight, so that the health status of the system can
be assessed and mitigation procedures (such as a return to the base
station or an emergency landing) can be initiated when needed.

In this paper, we report on the development of a dynamic monitoring
framework for the DLR ARTIS (Autonomous Rotorcraft Testbed for
Intelligent Systems) family of aircraft based on the formal
specification language .  The development of a monitoring
framework for an autonomous aircraft differs significantly from a
monitoring framework in a more standard setting, such as network
monitoring. A key consideration is that while the specification
language needs to be highly expressive, the monitor must
operate within strictly limited resources, and the monitor itself needs
to be highly reliable: any interference with the normal
operation of the aircraft could have fatal consequences.

A high level of expressiveness is necessary because the assessment of
the health status requires complex analyses, including a
cross-validation of different sensor modules such as the agreement
between the GPS module and the accelerometer. This is necessary in
order to discover a deterioration of a sensor module. At the same
time, the expressiveness and the precision of the monitor must be
balanced against the available computing resources.  The reliability
requirement goes beyond pure correctness and robustness of the
execution.  Most importantly, reliability requires that the peak
resource consumption of the monitor in terms of energy, time, and
space needs to be known ahead of time.  This means that it must be
possible to compute these resource requirements statically based on an
analysis of the specification.  The
determination whether the drone is equipped with sufficient hardware
can then be made before the flight, and the occurrence of dynamic failures
such as running out of memory or sudden drops in voltage can be ruled
out. Finally, the collection of the data from the on-board
architecture is a non-trivial problem: While the monitor needs access
to almost the complete system state, the data needs to be retrieved
non-intrusively such that it does not interfere with the normal system
operation.

Our monitoring approach is based on the formal stream specification language  <cit.>. In an specification, input streams that collect data from sensors, networks, etc.,
are filtered and combined into output streams that contain data
aggregated from multiple sources and over multiple points in time such
as over sliding windows of some real-time length. Trigger
conditions over these output streams then identify critical
situations. An specification is translated into a monitor defined in a  hardware description language and subsequently realized on an .
Before deployment, the specification is checked for consistency and the minimal requirements on the are computed.
The hardware monitor is then placed in a central position where as much sensor data as possible can be collected; during the execution, it then extracts the relevant information.
In addition to requiring no physical changes to the system architecture, this integration incurs no further traffic on the bus.

Our experience has been extremely positive: Our approach leads to highly efficient, parallelized monitors with formal guarantees on the non-interference of the monitor with the normal operation of the autonomous system.
The monitor is able to detect violations to complex specifications without intruding into the system execution, and operates within narrow resource constraints. is cleared for take-off.




Cyber-physical systems (CPS) carry out increasingly safety-critical tasks, such as controlling medical CPS, power plants, and autonomous vehicles. 
The complexity of these systems often exceeds the scalability of static verification techniques.
This renders dynamic verification methods such as runtime monitoring inevitable, as can be seen in the large body of recent works in this fieldmany recent papers.
In these approaches, rather than verifying the correctness of all possible executions of a system a formal specification, a single execution — the current execution of the system — is inspected during runtime.
For this, sensors capture the state of the system, which allows for assessing the health of the system and gaining an insight into its behavior.
Upon detection of undesired behavior, an alarm is raised upon which mitigation procedures can be initiated.

There are multiple requirements on a runtime verification framework: 
Not only does the input language of the monitor need to be sufficiently expressive, the monitor itself needs to be reliable as well.
A high level of expressiveness is necessary because the assessment of a CPS's health requires complex analyses.
They need to answer questions like “To which degree do measurements of the GPS module agree with readings of the accelerometer?”, which allows for a cross-validation of different sensor modules. 
This way, the deterioration of a sensor module can be discovered and subsequently replaced by a spare module — a technique widely used in systems with a high level of redundancy such as aircraft.
However, a high level of expressiveness in the specification language comes at the cost of high resource consumption of the monitor. 
However, most embedded devices do not have exuberant amounts of spare resources, nor can the main functionality be significantly reduced to create them. 
Thus, developers of runtime verification techniques need to find the sweet spot between adequate expressiveness and resource consumption, by forsaking generality for specific, highly relevant domain-specific language features.

The reliability of the monitor is independent of the expressiveness of the input language and goes beyond pure correctness and robustness of the execution.    
Most notably, this additionally entails that its peak resource consumption in terms of energy, time, and space needs to be available statically. 
This way, engineers can evaluate whether their hardware can cope with the requirements of the monitor before deployment.
This increases the confidence in the monitor by ruling out dynamic failures such as running out of memory or sudden drops in voltage.We can elaborate here or earlier that static criteria are far superior to dynamic ones which superficially contradicts the idea that RV > MC.  However, we can also just leave it out.

Lastly, the integration of the monitor is a delicate endeavor:
While the monitor requires as much information about the system state as possible, it may not require a complete overhaul of the system architecture.
Moreover, in many systems, sensor data needs to be retrieved non-intrusively such that it does not mingle with the regular execution of the system. 

In this paper we report on the integration of the monitoring framework into an existing autonomous drone.  
The monitor is based on an input specification in the language, which is translated into a hardware description language and realized on an .
Before deployment, the specification is analyzed for inner consistency and the minimal requirements on the are computed.
The hardware monitor is then placed in a central position where as much sensor data as possible can be collected; during the execution, it then extracts the relevant information.
In addition to requiring no physical changes to the system architecture, this integration approach incurs no further traffic on the bus.
We found that the monitor is able to detect violations to complex specifications without intruding into the system execution, nor requiring unreasonable resources.




 §.§ Related Work



Stream-based monitoring approaches focus on an expressive specification language while handling non-binary data.
Its roots lie in synchronous, declarative stream processing languages like Lustre <cit.> and Lola <cit.>.
The Copilot framework <cit.> features a declarative data-flow language from which constant space and constant time C monitors are generated; these guarantees enable usage on an embedded device.
Rather than focusing on data-flow, the family of Lola-languages puts an emphasis on statistical measures and has successfully been used to monitor synchronous, discrete time properties of autonomous aircraft <cit.>.
In contrast to that,  <cit.> supports real-time capabilities and efficient aggregation of data occurring with arbitrary frequency, while forgoing parametrization for efficiency <cit.>. 
can also be compiled to and subsequently realized on an  <cit.>.

Apart from stream-based monitoring, there is a rich body of monitoring based on real-time temporal logics <cit.> such as Signal Temporal Logic (STL) <cit.>.
Such languages are a concise way to describe temporal behaviors with the shortcoming that they are usually limited to qualitative statements, boolean verdicts.
This limitation was addressed for STL <cit.> by introducing a quantitative semantics indicating the robustness of a satisfaction.
To specify continuous signal patterns, specification languages based on regular expressions can be beneficial, e.g. Signal Regular Expressions (SRE) <cit.>. 
The R2U2 tool <cit.> stands out in particular as it successfully brought a logic closely related to STL onto unmanned aerial systems as an external hardware implementation.





§ SETUP

The Autonomous Rotorcraft Testbed for Intelligent Systems (ARTIS) is a platform used by the Institute of Flight Systems of the German Aerospace Center (DLR) to conduct research on autonomous flight.
It consists of a set of unmanned helicopters and fixed-wing aircraft of different sizes which can be used to develop new techniques and evaluate them under real-world conditions.

The case study presented in this paper revolves around the superARTIS, a large helicopter with a maximum payload of 85, depicted in <ref>. 
The high payload capabilities allow the aircraft to carry multiple sensor systems, computational resources, and data links.
This extensive range of avionic equipment plays an important role in improving the situational awareness of the aircraft <cit.> during the flight.
It facilitates safe autonomous research missions which include flying in urban or maritime areas, alone or with other aircraft.   
Before an actual flight test, software- and hardware-in-the-loop simulations, as well as  real-time logfile replays strengthen confidence in the developed technology.



 §.§ Mission

One field of application for unmanned aerial vehicles (UAVs) is reconnaissance missions.
In such missions, the aircraft is expected to operate within a fixed area in which it can cause no harm. 
The polygonal boundary of this area is called a geo-fence.
As soon as the vehicle passes the geo-fence, mitigation procedures need to be initiated to ensure that the aircraft does not stray further away from the safe area.

The case study presented in this paper features a reconnaissance mission. 
<ref> shows the flight path (blue line) within a geo-fence (red line). 
Evidently, the aircraft violates the fence several times temporarily.
A reason for this can be flawed position estimation:  An aircraft estimates its position based on several factors such as landmarks detected optically or GPS sensor readings.
In the latter case, GPS satellites send position and time information to earth. 
The GPS module uses this data to compute the aircraft's absolute position with trilateration. 
However, signal reflection or a low number of GPS satellites in range can result in imprecisions in the position approximation.
If the aircraft is continuously exposed to imprecise position updates, the error adds up and results in a strong deviation from the expected flight path.

The impact of this effect can be seen in <ref>.
It shows the velocity of a ground-borne aircraft in an enclosed backyard according to its GPS module.[GPS modules only provide absolute position information; the first derivative thereof, however, is the velocity.]
During the reported period of time, the aircraft was pushed across the backyard by hand.
While the expected graph is a smooth curve, the actual measurements show an erratic curve with errors of up to ± 1.5, 
which can be mainly attributed to signals being reflected on the enclosure.
The strictly positive trend of the horizontal velocity can explain strong deviations from the desired flight path seen in <ref>.

A counter-measure to these imprecisions is the cross-validation of several redundant sensors. 
As an example, rather than just relying on the velocity reported by a GPS module, its measured velocity can be compared to the integrated output of an accelerometer. 
When the values deviate strongly, the values can be classified as less reliable than when both sensors agree.






 §.§ Non-Intrusive Instrumentation


When integrating the monitor into an existing system, the system architecture usually cannot be altered drastically.
Moreover, the monitor should not interfere with the regular execution of the system, by requiring the controller to send explicit messages to it.
Such a requirement could offset the timing behavior and thus have a negative impact on the overall performance of the system.

The issue can be circumvented by placing the monitor at a point where it can access all data necessary for the monitoring process non-intrusively.
In the case of the superARTIS, the logger interface provides such a place as it compiled the data of all position-related sensors as well as the output of the position estimation <cit.>.
<ref> outlines the relevant data lines of the aircraft. 
Sensors were polled with fixed frequencies of up to 100. 
The schematic shows that the logger explicitly sends data to the monitor.
This is not a strict requirement of the monitor as it could be connected to the data busses leading to the logger and passively read incoming data packets.
However, in the present setting, the logger did not run at full capacity. 
Thus sending information to the monitor came at no relevant cost while requiring few hardware changes to the bus layout.

In turn, the monitor provides feedback regarding violations of the specification. 
Here, we distinguish between different timing behaviors of triggers. 
The monitor evaluates event-based triggers whenever the system passes new events to the monitor and immediately replies with the results.
For periodic triggers, , those annotated with an evaluation frequency, the evaluation is decoupled from the communication between monitor and system.
Thus, the monitor needs to wait until it receives another event until reporting the verdict.  
This incurs a short delay between detection and report.  




































 §.§ StreamLAB

[<stream-lab.eu>]<cit.> is a monitoring framework revolving around the stream-based specification language . 
It emphasizes on analyses conducted before deployment of the monitor. 
This increases the confidence in a successful execution by providing information to aid the specifier.
To this end, it detects inconsistencies in the specification such as type errors, an lossy conversion of a floating point number to an integer, or timing errors, accessing values that might not exist. 
Further, it provides two execution modes: an interpreter and an compilation.  
The interpreter allows the specifier to validate their specification. 
For this, it requires a trace, a series of data that is expected to occur during an execution of the system.
It then checks whether a trace complies with the specification and reports the points in time when specified bounds are violated.
After successfully validating the specification, it can be compiled into code.
Yet again, the compiled code can be analyzed with respect to the space and power consumption.
This information allows for evaluating whether the available hardware suffices for running the monitor.

An specification consists of input and output streams, as well as trigger conditions.
Input streams describe data the system produces asynchronously and provides to the monitor. 
Output streams use this data to assess the health state of the system by computing statistical information.
Trigger conditions distinguish desired and undesired behavior. 
A violation of the condition issues an alarm to the system.

The following specification declares a floating point input stream height representing sensor readings of an altimeter.
The output stream avg_height computes the average value of the height stream over two minutes.  
The aggregation is a sliding window computed once per second, as indicated with the @1Hz annotation.[Details on how such a computation can cope with a statically-bounded amount of memory can be found in <cit.>.] 
The stream δheight computes the difference between the average and the current height. 
A strong deviation of these values constitutes a suspicious jump in sensor readings, which might indicate a faulty sensor or an unexpected loss or gain in height.
In this case, the trigger in the specification issues a warning to the system, which can initiate mitigation measures.

  input height: Float32
  output avg_height @1Hz := height.aggregate(over: 2min, using: avg)
  output δheight := abs(avg_height.hold().defaults(to: height) - height)
  trigger δheight > 50.0 "WARNING: Suspicious jump in height."

Note that this is just a brief introduction to and the framework.  
For more details, the authors refer to <cit.>.




 §.§ FPGA as Monitoring Platform


An specification can be compiled into the hardware description language and subsequently realized on an as proposed by Baumeister <cit.>.
An as target platform for the monitor has several advantages in terms of improving the development process, reducing its cost, and increasing the overall confidence in the execution.

Since the is a separate module and thus decoupled from the control software, these components do not share processor time or memory.
This especially means that control and monitoring computations happen in parallel.
Further, the monitor itself parallelizes the computation of independent output streams with almost no additional overhead. 
This significantly accelerates the monitoring process <cit.>.
The compiled specification allows for extensive static analyses. 
Most notably, the results include whether the board is sufficiently large in terms of look-up tables and storage capabilities to host the monitor, and the power consumption when idle or at peak performance.
Lastly, an is the sweet spot between generality and specificity: it runs faster, is lighter, and consumes less energy than general purpose hardware while retaining a similar time-to-deployment.
The latter combined with a drastically lower cost renders the superior to application-specific integrated circuits () during development phase.
After that, when the specification is fixed, an might be considered for its yet increased performance.



 §.§ RTLola Specifications

The entire specification for the mission is comprised of three sub-specifications.  
This section briefly outlines each of them and explains representative properties in <ref>.
The complete specifications as well as a detailed description were presented in earlier work <cit.>.


  
  Sensor Validation (<ref>) 
    Sensors can produce incorrect values, when too few GPS satellites are in range for an accurate trilateration or if the aircraft flies above the range of a radio altimeter. 
    A simple exemplary validation is to check whether the measured altitude is non-negative. 
    If such a check fails, the values are meaningless, so the system should not take them into account in its computations.
  
  Geo-Fence (<ref>) 
    During the mission, the aircraft has permission to fly inside a zone delimited by a polygon, called a geo-fence. 
    The specification checks whether a face of the fence has been crossed, in which case  the aircraft needs to ensure that it does not stray further from the permitted zone.
  
  Sensor Cross-Validation (<ref>) 
    Sensor redundancy allows for validating a sensor reading by comparing it against readings of other sensors. 
    An agreement between the values raises the confidence in their correctness.  
    An example is the cross-validation of the GPS module against the accelerometer. 
    Integrating the readings of the latter twice yields an absolute position which can be compared against the GPS position.


<ref> points out some representative sub-properties of the previously described specification in , which are too long to discuss them in detail. It contains a validation of GPS readings as well as a cross-validation of the GPS module against the Inertial Measurement Unit (IMU).  
The specification declares three input streams, the x-position and number of GPS satellites in range from the GPS module, and the acceleration in x-direction according to the IMU.

The first trigger counts the number of updates received from the GPS module by counting how often the input stream gps_x gets updated to validate the timing behavior of the module.

The output stream few_sat computes the indicator function for num_sat < 9, which indicates that the GPS module might report unreliable data due to few satellites in reach.
If this happens more than 12 times within five seconds, the next trigger issues a warning to indicate that the incoming GPS values might be inaccurate.
The last trigger checks whether the double integral of the IMU acceleration coincides with the GPS position up to a threshold of 0.5 meters.







 §.§ VHDL Synthesis

The specifications mentioned above were compiled into and realized on the Xilinx ZC702 Base Board[<https://www.xilinx.com/support/documentation/boards_and_kits/zc702_zvik/ug850-zc702-eval-bd.pdf>].
The following table details the resource consumption of each sub-specification reported by the synthesis tool Vivado.



  Spec           FF     FF[%]       LUT      LUT[%]      MUX     Idle []     Peak [] 

  Geo-fence      2,853     3     26,181     71     4       149     1.871 

    
  Validation     4,792     5     34,630     67     104     156     2.085 

  Cross          3,441     4     23,261     46     99      150     1.911 

  	


The number of flip-flops (FF) indicates the memory consumption in bits; neither specification requires more than 600 of memory.
The number of LUTs (Look-up Tables) is an indicator for the complexity of the logic. 
The sensor validation, despite being significantly longer than the cross-validation, requires the least amount of LUTs. 
The reason is that its computations are simple in comparison: Rather than computing sliding window aggregations or line intersections, it mainly consists of simple thresholding.
The number of multiplexers (MUX) reflects this as well: Since thresholding requires comparisons, which translate to multiplexers, the validation requires twice as many of them.
Lastly, the power consumption of the monitor is extremely low: When idle, neither specification requires more than 156 and even under peak pressure, the power consumption does not exceed 2.1.  
For comparison, a Raspberry Pi needs between 1.1 (Model 2B) and 2.7 (Model 4B) when idle and roughly twice as much under peak pressure, i.e., 2.1 and 6.4, respectively.[Information collected from <https://www.pidramble.com/wiki/benchmarks/power-consumption> in January, 2020.]

Note that the geo-fence specification checks for 12 intersections in parallel, one for each face of the fence (cf. <ref>). 
Adapting the number of faces allows for scaling the amount of resources required, as can be seen in <ref>.  
The graph does not grow linearly because the realization problem of code onto an is a multi-dimensional optimization problem with several pareto-optimal solutions.
Under default settings, the optimizer found a solution for four faces that required fewer LUTs than for three faces. 
At the same time, the worst negative slack time (WNST) of the four-face solution was lower than the WNST for the three-face solution as well (cf. <ref>), indicating that the former performs worst in terms of running time.




























































































































§ RESULTS


As the title of the paper suggests, the superARTIS with the monitor component is cleared to fly and a flight test is already scheduled.
In the meantime, the monitor was validated on log files from past missions of the superARTIS replayed under realistic conditions.
During a flight, the controller polls samples from sensors, estimates the current position, and sends the respective data to the logger and monitor.
In the replay setting, the process remains the same except for one detail: 
Rather than receiving data from the actual sensors, the data sent to the controller is read from a past log file in the same frequency in which they were recorded.
The timing and logging behavior is equivalent to a real execution. 
This especially means that the replayed data points will be recorded again in the same way. 
Control computations take place on a machine identical to the one on the actual aircraft.
As a result, from the point of view of the monitor, the replay mode and the actual flight are indistinguishable. 
Note that the setup is open-loop, , the monitor cannot influence the running system.
Therefore, the replay mode using real data is more realistic than a high-fidelity simulation.

When monitoring the geo-fence of the reconnaissance mission in <ref>, all twelve face crossings were detected successfully.  
Additionally, when replaying the sensor data of the experiment in the enclosed backyard from <ref>, the erratic GPS sensor data lead to 113 violations regarding the GPS module on its own.
Note that many of these violations point to the same culprit:  a low number of available GPS satellites, for example, correlates with the occurrence of peaks in the GPS velocity.
Moreover, the cross validation issued another 36 alarms due to a divergence of IMU and GPS readings. 
Other checks, for example detecting a deterioration of the GPS module based on its output frequency, were not violated in either flight and thus not reported.






















§ CONCLUSION


We have presented the integration of a hardware-based monitor into the superARTIS UAV. 
The distinguishing features of our approach are the high level of expressiveness of the specification language combined with the formal guarantees on the resource usage. 
The comprehensive tool framework facilitates the development of complex specifications, which can be validated on log data before they get translated into a hardware-based monitor.
The automatic analysis of the specification derives the minimal requirements on the development board needed for safe operation. 
If they are met, the specification is realized on an and integrated into the superARTIS architecture.
Our experience shows that the overall system works correctly and reliably, even without thorough system-level testing. 
This is due to the non-interfering instrumentation, the validated specification, and the formal guarantees on the absence of dynamic failures of the monitor.







	

splncs04




§ RTLOLA SPECIFICATIONS

This section gives more details on the specification. 



 §.§ Sensor Validation

In this subsection, we consider GPS receiver submodules, namely: GPS velocity and position.
In the specification shown in <ref>, the outputs of both modules are declared as inputs to the monitor (Lines 5–6 and 15–18).
Basic checks whether the absolute values of the horizontal and vertical speed are within bounds are performed in lines 9 and 10, where triggers check if any bound is exceeded.
Similarly, valid states of the position_type (Lines 21) and bounds for diff_age and solution_age (lines 23–24) are easily checked.
Lines 26–33 evaluate the performance of the position estimation based on the number of satellites in reach.
In line 27, we count once per second, with 1, the number of satellites over the last three seconds.
We expect to see at least nine satellites within this frame of time.
Next, we trigger a notification on each rising edge of behavior_num_sats (line 32–33).
The stream behavior_num_sats is an aggregation over five seconds where curr_num_sats_invalid represents an auxiliary stream which valides the number of satellites.
Once per second we check if within the last five seconds more than twelve events reported a number of satellites below 9.
If this is the case, we warn the system because the GPS modules seems to deteriorate.

The specification in <ref> complements the GPS validation.
Here, we focus on the horizontal (lines 9–11), vertical speed (lines 13–15), and the length of the speed vector (lines 17–19).
Each second, we aggregate the respective speed and take the average.
Each time we receive a new speed event, we compare its value against the computed average value of the last ten seconds.
If there is a strong deviation, we raise a violation.

The validation specification is the combination of <ref> and <ref>.







 §.§ Geo-fence

In this section, we depict the detection of a single line crossing of a geo-fence. 
The specification can be seen in <ref> where italic variables represent constant points of the geo-fence (lat, lon) and their respective slopes (m) and y-intercepts (b). 
The basic idea is to compute the intersection of the geo-fence line and the vehicle line, i.e. the line given the last position and the current position of the vehicle.
The vehicle line is computed in lines 12–21.
The slope of the line and the y-intercept are calculated in lines 20 and 21, respectively.
Given these parameters, the computation of the intersection point is basic geometry, y = m· x + t.
Finally, we check whether the intersection point lies on both the vehicle line and the geo-fence face (lines 34–41).
The output is_fnc is true if the vehicle movement can be encoded as a valid function (line 32).





 §.§ Sensor Cross-Validation

In this section, we consider two complementary sensors.
The GPS receiver based on satellite signals and an Inertial Measurement Unit (IMU) based on acceleration and angular rate data.
In the specification given in <ref>, we use the fact that the acceleration is the derivative of the velocity.
This correlation should be present when comparing IMU and GPS receiver events.
Since the IMU frequency is known, we compute the expected velocity, by averaging instead of an integration with the trapezoid abstraction (lines 15–16).
This removes undesired noise.
The average velocity given by the GPS receiver is computed in a straight forward manner (lines 19–22).
A warning is raised if the difference in velocity is greater than 0.5 (line 25). 




