{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T18:44:58Z","timestamp":1761417898280,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s10009-017-0470-5","type":"journal-article","created":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T04:55:41Z","timestamp":1503291341000},"page":"379-395","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Runtime verification of autopilot systems using a fragment of MTL- $${\\int }$$ \u222b"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9452-0995","authenticated-orcid":false,"given":"Andr\u00e9","family":"de Matos Pedro","sequence":"first","affiliation":[]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[]},{"given":"David","family":"Pereira","sequence":"additional","affiliation":[]},{"given":"Lu\u00eds Miguel","family":"Pinho","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"470_CR1","doi-asserted-by":"crossref","unstructured":"Ranjbaran, M., Khorasani, K.: Fault recovery of an under-actuated quadrotor aerial vehicle. In: CDC, pp. 4385\u20134392 (2010)","DOI":"10.1109\/CDC.2010.5718140"},{"key":"470_CR2","doi-asserted-by":"crossref","unstructured":"Meier, L., Honegger, D., Pollefeys, M.: Px4: a node-based multithreaded open source robotics framework for deeply embedded platforms. In: ICRA, pp. 6235\u20136240 (2015)","DOI":"10.1109\/ICRA.2015.7140074"},{"issue":"4","key":"470_CR3","doi-asserted-by":"crossref","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"470_CR4","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"470_CR5","unstructured":"de\u00a0Roever, W.P., de\u00a0Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods, volume\u00a054 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)"},{"key":"470_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"John Harrison","year":"2009","unstructured":"Harrison, John: Handbook of Practical Logic and Automated Reasoning, 1st edn. Cambridge University Press, New York (2009)","edition":"1"},{"key":"470_CR7","unstructured":"Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. In: RTSS, pp. 2\u201313 (2003)"},{"issue":"1","key":"470_CR8","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1109\/5.259428","volume":"82","author":"JWS Liu","year":"1994","unstructured":"Liu, J.W.S., Shih, W.-K., Lin, K.-J., Bettati, R., Chung, J.-Y.: Imprecise computations. Proc. IEEE 82(1), 83\u201394 (1994)","journal-title":"Proc. IEEE"},{"key":"470_CR9","unstructured":"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\u201370 (2015)"},{"issue":"1","key":"470_CR10","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/0304-3975(94)00151-8","volume":"138","author":"Y Lakhneche","year":"1995","unstructured":"Lakhneche, Y., Hooman, J.: Metric temporal logic with durations. Theor. Comput. Sci. 138(1), 169\u2013199 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"470_CR11","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: FORMATS \u201908, pp. 1\u201313, Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85778-5_1"},{"key":"470_CR12","doi-asserted-by":"crossref","unstructured":"Pike, L.: Modeling time-triggered protocols and verifying their real-time schedules. In: FMCAD, pp. 231\u2013238, (2007)","DOI":"10.1109\/FAMCAD.2007.10"},{"issue":"1","key":"470_CR13","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/2752801.2752808","volume":"12","author":"AM Pedro","year":"2015","unstructured":"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\u201364 (2015)","journal-title":"SIGBED Rev."},{"key":"470_CR14","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: CAV, pp. 176\u2013189. Springer, New York (2008)","DOI":"10.21236\/ADA476791"},{"key":"470_CR15","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Tonetta, S.: Requirements validation for hybrid systems. In: CAV, pp. 188\u2013203. Springer, New York (2009)","DOI":"10.1007\/978-3-642-02658-4_17"},{"key":"470_CR16","doi-asserted-by":"crossref","unstructured":"Pedro, A.M., Pereira, D., Pinho, L.M., Pinto, J.S.: Monitoring for a decidable fragment of mtld. In: RV, pp. 169\u2013184. Springer, New York (2015)","DOI":"10.1007\/978-3-319-23820-3_11"},{"issue":"1","key":"470_CR17","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1145\/1093390.1093393","volume":"10","author":"GE Collins","year":"1976","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. SIGSAM Bull. 10(1), 10\u201312 (1976)","journal-title":"SIGSAM Bull."},{"key":"470_CR18","doi-asserted-by":"crossref","unstructured":"Chen, Y., Chang, L., Kuo, T.I., Mok, A.K.: Real-time task scheduling anomaly: observations and prevention. In: SAC, pp. 897\u2013898. ACM, New York (2005)","DOI":"10.1145\/1066677.1066881"},{"key":"470_CR19","volume-title":"Rule Systems for Run-Time Monitoring: From Eagle to Ruler","author":"H Barringer","year":"2007","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule Systems for Run-Time Monitoring: From Eagle to Ruler. Springer, Berlin (2007)"},{"key":"470_CR20","doi-asserted-by":"crossref","unstructured":"Sammapun, U., Lee, I., Sokolsky, O.: Rt-mac: runtime monitoring and checking of quantitative and probabilistic properties. In: RTCSA, pp. 147\u2013153 (2005)","DOI":"10.1109\/RTCSA.2005.84"},{"key":"470_CR21","doi-asserted-by":"crossref","unstructured":"Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: RV\u201910, pp. 345\u2013359. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16612-9_26"},{"key":"470_CR22","volume-title":"From Propositional to First-order Monitoring","author":"A Bauer","year":"2013","unstructured":"Bauer, A., Kuster, J., Vegliach, G.: From Propositional to First-order Monitoring. Springer, Berlin (2013)"},{"key":"470_CR23","doi-asserted-by":"crossref","unstructured":"Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: TACAS, pp. 341\u2013356. Springer, New York (2014)","DOI":"10.1007\/978-3-642-54862-8_23"},{"issue":"2","key":"470_CR24","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/j.ic.2009.10.004","volume":"208","author":"P Bouyer","year":"2010","unstructured":"Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97\u2013116 (2010)","journal-title":"Inf. Comput."},{"issue":"4","key":"470_CR25","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"Ron Koymans","year":"1990","unstructured":"Koymans, Ron: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"470_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: SFCS \u201977, pp. 46\u201357. IEEE Computer Society, Washington (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"470_CR27","unstructured":"Pedro, A.M.: rtmlib Monitoring Library. https:\/\/anmaped.github.io\/rtmlib\/doc\/ (2016), version 0.1-alpha"},{"key":"470_CR28","unstructured":"The OCaml Development Team. Ocaml programming language (2013)"},{"key":"470_CR29","unstructured":"Pedro, A.M.: rmtld3synth Synthesis Tool. https:\/\/github.com\/cistergit\/rmtld3synth\/ (2016), version 0.1-alpha"},{"key":"470_CR30","first-page":"66","volume":"2015","author":"G Nelissen","year":"2015","unstructured":"Nelissen, G., Pereira, D., Pinho, L.M.: A novel run-time monitoring architecture for safe and efficient inline monitoring. Ada-Europe 2015, 66\u201382 (2015)","journal-title":"Ada-Europe"},{"key":"470_CR31","doi-asserted-by":"crossref","unstructured":"Coombes, M., McAree, O., Chen, W.\u00a0H., Render, P.: Development of an autopilot system for rapid prototyping of high level control algorithms. In: Proceedings of 2012 UKACC CONTROL, pp. 292\u2013297 (2012)","DOI":"10.1109\/CONTROL.2012.6334645"},{"key":"470_CR32","unstructured":"Nutt, G.: NuttX Real-Time Operating System. http:\/\/nuttx.org\/ (2007), version 7.11"},{"key":"470_CR33","doi-asserted-by":"crossref","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2u2: Monitoring and diagnosis of security threats for unmanned aerial systems. In: RV 2015, pp. 233\u2013249 (2015)","DOI":"10.1007\/978-3-319-23820-3_15"},{"key":"470_CR34","unstructured":"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"},{"key":"470_CR35","doi-asserted-by":"crossref","unstructured":"Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: CONCUR, pp. 138\u2013152. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44618-4_12"},{"key":"470_CR36","doi-asserted-by":"crossref","unstructured":"Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: IEEE Computer Society, pp. 349\u2013357 (2013)","DOI":"10.1109\/LICS.2013.41"},{"key":"470_CR37","doi-asserted-by":"crossref","unstructured":"Navabpour, S., Bonakdarpour, B., Fischmeister, S.: Time-triggered runtime verification of component-based multi-core systems. In: RV. Springer, New York (2015)","DOI":"10.1007\/978-3-319-23820-3_10"},{"key":"470_CR38","unstructured":"Mueller, M.W., D\u2019Andrea, 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\u201352, (2014)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0470-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0470-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0470-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T12:30:10Z","timestamp":1570019410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0470-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["470"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0470-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2017,8,21]]}}}