iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/s10009-017-0470-5
Runtime verification of autopilot systems using a fragment of MTL- $${\int }$$ | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

Runtime verification of autopilot systems using a fragment of MTL-\({\int }\)

  • FMICS-AVoCS
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Current real-time embedded systems development frameworks lack support for the verification of properties using explicit time where counting time (i.e., durations) may play an important role in the development process. Focusing on the real-time constraints inherent to these systems, we present a framework that addresses the specification of duration properties for runtime verification by employing a fragment of metric temporal logic with durations. We also provide an overview of the framework, the synthesis tools, and the library to support monitoring properties for real-time systems developed in C++11. The results obtained provide clear evidence of the feasibility and advantages of employing a duration-sensitive formalism to increase the dependability of avionic controller systems such as the PX4 and the Ardupilot flight stacks.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6

Similar content being viewed by others

Notes

  1. By constant time, we mean that a monitor executes the same number of CPU cycles at each invocation.

  2. The instructions to generate the C++11  code files that are the output of the use case experiments are fully detailed in [29] .

  3. Available at https://github.com/anmaped/rmtld3synth/tree/v0.3-alpha, version 0.3-alpha.

References

  1. Ranjbaran, M., Khorasani, K.: Fault recovery of an under-actuated quadrotor aerial vehicle. In: CDC, pp. 4385–4392 (2010)

  2. Meier, L., Honegger, D., Pollefeys, M.: Px4: a node-based multithreaded open source robotics framework for deeply embedded platforms. In: ICRA, pp. 6235–6240 (2015)

  3. Bauer, A., Leucker, M., Schallhart, C.: Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)

    Article  Google Scholar 

  4. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  5. de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods, volume 54 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)

  6. Harrison, John: Handbook of Practical Logic and Automated Reasoning, 1st edn. Cambridge University Press, New York (2009)

    Book  MATH  Google Scholar 

  7. Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. In: RTSS, pp. 2–13 (2003)

  8. Liu, J.W.S., Shih, W.-K., Lin, K.-J., Bettati, R., Chung, J.-Y.: Imprecise computations. Proc. IEEE 82(1), 83–94 (1994)

    Article  Google Scholar 

  9. Mizotani, K., Hatori, Y., Kumura, Y., Takasu, M., Chishiro, H., Yamasaki, N.: An integration of imprecise computation model and real-time voltage and frequency scaling. In: CATA, pp. 63–70 (2015)

  10. Lakhneche, Y., Hooman, J.: Metric temporal logic with durations. Theor. Comput. Sci. 138(1), 169–199 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  11. Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: FORMATS ’08, pp. 1–13, Springer, Berlin (2008)

  12. Pike, L.: Modeling time-triggered protocols and verifying their real-time schedules. In: FMCAD, pp. 231–238, (2007)

  13. Pedro, A.M., Pereira, D., Pinho, L.M., Pinto, J.S.: Logic-based schedulability analysis for compositional hard real-time embedded systems. SIGBED Rev. 12(1), 56–64 (2015)

    Article  Google Scholar 

  14. Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: CAV, pp. 176–189. Springer, New York (2008)

  15. Cimatti, A., Roveri, M., Tonetta, S.: Requirements validation for hybrid systems. In: CAV, pp. 188–203. Springer, New York (2009)

  16. Pedro, A.M., Pereira, D., Pinho, L.M., Pinto, J.S.: Monitoring for a decidable fragment of mtld. In: RV, pp. 169–184. Springer, New York (2015)

  17. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. SIGSAM Bull. 10(1), 10–12 (1976)

    Article  Google Scholar 

  18. Chen, Y., Chang, L., Kuo, T.I., Mok, A.K.: Real-time task scheduling anomaly: observations and prevention. In: SAC, pp. 897–898. ACM, New York (2005)

  19. Barringer, H., Rydeheard, D., Havelund, K.: Rule Systems for Run-Time Monitoring: From Eagle to Ruler. Springer, Berlin (2007)

    MATH  Google Scholar 

  20. Sammapun, U., Lee, I., Sokolsky, O.: Rt-mac: runtime monitoring and checking of quantitative and probabilistic properties. In: RTCSA, pp. 147–153 (2005)

  21. Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: RV’10, pp. 345–359. Springer, Berlin (2010)

  22. Bauer, A., Kuster, J., Vegliach, G.: From Propositional to First-order Monitoring. Springer, Berlin (2013)

    Book  MATH  Google Scholar 

  23. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: TACAS, pp. 341–356. Springer, New York (2014)

  24. Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97–116 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  25. Koymans, Ron: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  26. Pnueli, A.: The temporal logic of programs. In: SFCS ’77, pp. 46–57. IEEE Computer Society, Washington (1977)

  27. Pedro, A.M.: rtmlib Monitoring Library. https://anmaped.github.io/rtmlib/doc/ (2016), version 0.1-alpha

  28. The OCaml Development Team. Ocaml programming language (2013)

  29. Pedro, A.M.: rmtld3synth Synthesis Tool. https://github.com/cistergit/rmtld3synth/ (2016), version 0.1-alpha

  30. Nelissen, G., Pereira, D., Pinho, L.M.: A novel run-time monitoring architecture for safe and efficient inline monitoring. Ada-Europe 2015, 66–82 (2015)

    Google Scholar 

  31. Coombes, M., McAree, O., Chen, W. H., Render, P.: Development of an autopilot system for rapid prototyping of high level control algorithms. In: Proceedings of 2012 UKACC CONTROL, pp. 292–297 (2012)

  32. Nutt, G.: NuttX Real-Time Operating System. http://nuttx.org/ (2007), version 7.11

  33. Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2u2: Monitoring and diagnosis of security threats for unmanned aerial systems. In: RV 2015, pp. 233–249 (2015)

  34. Pedro, A.M.: Use Case (1) and Use Case (2) configure files with settings. https://github.com/anmaped/rmtld3synth/tree/dev/config (2016). version 1

  35. Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: CONCUR, pp. 138–152. Springer, Berlin (2000)

  36. Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: IEEE Computer Society, pp. 349–357 (2013)

  37. Navabpour, S., Bonakdarpour, B., Fischmeister, S.: Time-triggered runtime verification of component-based multi-core systems. In: RV. Springer, New York (2015)

  38. Mueller, M.W., D’Andrea, R.: Stability and control of a quadrocopter despite the complete loss of one, two, or three propellers. In: IEEE international conference on robotics and automation (ICRA), pp. 45–52, (2014)

Download references

Author information

Authors and Affiliations

  1. CISTER/INESC TEC, ISEP, Polytechnic Institute of Porto, Porto, Portugal

    André de Matos Pedro, David Pereira & Luís Miguel Pinho

  2. HASLab/INESC TEC & Universidade do Minho, Braga, Portugal

    Jorge Sousa Pinto

Authors
  1. André de Matos Pedro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jorge Sousa Pinto
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Pereira
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Luís Miguel Pinho
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to André de Matos Pedro.

A rmtld3synth tool User’s Guide

A rmtld3synth tool User’s Guide

The rmtld3synth synthesis tool is able to automatically generate monitors based on the formal specifications written in RMTL-\(\int _3\). Polynomial inequalities are supported by this formalism as well as the most common operators of temporal logics. Furthermore, quantification is also considered in the language of RMTL-\(\int _3\) as a means to facilitate the decomposition of the quantified formulas into several monitoring conditions.

We will now present an overview of the typical process for generating monitors for Ocaml and C++11 languages using this tool, together with a running example of a simple monitoring case generation. We begin by the running example, present the generated monitors, and show how to configure the RV monitoring model to couple with the system.

Consider the formula

$$\begin{aligned} (a \rightarrow ((a \vee b) \, \mathrm {U} _{<10} \, c)) \wedge \int ^{10} c < 4 \end{aligned}$$
(1)

that intuitively describes that given an event a, b occurs until c and, at the same time, the duration of b shall be less than four time units over the next 10 time units. For instance, a trace that satisfies this formula is

$$\begin{aligned} (a,2),(b,2),(a,1),(c,3),(a,3),(c,10). \end{aligned}$$

From rmtld3synth2ocaml tool, we have synthesized the formula’s example into the code of Listing 4. For that, we have used the command in Listing 2.

figure b

Next, we can also generate C++11 monitors by replacing –synth-ocaml with –synth-cpp11. The outcome is the monitor illustrated in Listing 5. To use those monitors, we need to define a trace for Ocaml reference as in Listing 3.

figure c

For the Ocaml language, experimental integration with RTMLib is available. However, we do not describe it here, but refer the reader for the examples in rmtld3synth’s repository Footnote 3. For C++11 we will now briefly describe how it is performed. Given the verbosity of the generated code, we have removed the conjunction including the duration inequality and used instead the simple formula

$$\begin{aligned} \int ^{10} c< 4. \end{aligned}$$
figure d

Now, we describe the settings for constructing the RV monitoring model.

Overview of the configuration settings. The settings for rmtld3synth tool are defined using the syntax

figure e
figure f

where | distinguishes between the supported types of arguments such as Boolean, integer or string, and setting_id is a string containing the name of the setting to which values are assigned. An example of a set of possible settings for the tool is given in the first five lines of Listing 6.

We now briefly describe the purpose of each of the setting entries present in Listing 6:

  • gen_tests sets the automatic generations of test cases (to be used as a demo for testing monitor’s execution).

  • gen_concurrency_tests constructs tests for testing lock- and wait-free monitors executing concurrently.

  • gen_unit_tests constructs tests for C++11 synthesis using the Ocaml source code as an oracle.

  • buffer_size sets the static size of the buffer to be used (rmtld3synth tool can change it if required by some constraints).

  • minimum_inter_arrival_time establishes the minimum inter-arrival time that the events can have. It is a very pessimistic setting but provides some information for static checking.

  • maximum_period sets the maximum interval between two consecutive releases of a task’s job. It has a correlation between the periodic monitor and the minimum inter-arrival time. It provides static checks according to the size of time stamps of events.

  • event_type provides the type for dealing with events (commonly is a class parameter).

  • event_subtype provides the type for the event data. In that case, it is an identifier that can distinct 255 events. However, if more events are required, the type should be modified to *uint32_t* or greater. The number of different events versus the available size for the identifier is also statically checked.

  • cluster_name identifies the set of monitors. It acts as a label for grouping monitor specifications.

figure g
figure h

Writing formulas in RMTLD3 The formulas “m_simple” and “m_morecomplex” follow the same syntax defined in this document. For setting a periodic monitor, we use . They are formatted as a symbolic expression. The type of monitors in Ocaml is according to Listing 7.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

de Matos Pedro, A., Pinto, J.S., Pereira, D. et al. Runtime verification of autopilot systems using a fragment of MTL-\({\int }\) . Int J Softw Tools Technol Transfer 20, 379–395 (2018). https://doi.org/10.1007/s10009-017-0470-5

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-017-0470-5

Keywords

Search

Navigation