Bringing runtime verification home: a case study on the hierarchical monitoring of smart homes using decentralized specifications
Tóm tắt
Từ khóa
Tài liệu tham khảo
Aimal, S., Parveez, K., Saba, A., Batool, S., Arshad, H., Javaid, N.: Energy optimization techniques for demand-side management in smart homes. In: Advances in Intelligent Networking and Collaborative Systems, The 9th International Conference on Intelligent Networking and Collaborative Systems, INCoS-2017. Lecture Notes on Data Engineering and Communications Technologies, vol. 8, pp. 515–524. Springer (2017)
Alemdar, H.Ö., Ertan, H., Incel, Ö.D., Ersoy, C.: ARAS human activity datasets in multiple homes with multiple residents. In: 7th International Conference on Pervasive Computing Technologies for Healthcare and Workshops, PervasiveHealth 2013. pp. 232–235. IEEE (2013)
Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10–14, 2017. ACM (2017)
Bakhirkin, A., Ferrère, T., Maler, O., Ulus, D.: On the quantitative semantics of regular expressions over real-valued signals. In: Abate, A., Geeraerts, G. (eds.) Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5–7, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10419, pp. 189–206. Springer (2017)
Bartocci, E., Bloem, R., Nickovic, D., Röck, F.: A counting semantics for monitoring LTL specifications over finite traces. CoRR abs. arXiv:1804.03237 (2018)
Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification—Introductory and Advanced Topics. Lecture Notes in Computer Science, vol. 10457. Springer (2018)
Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf. (2017)
Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification—Introductory and Advanced Topics, Lecture Notes in Computer Science, vol. 10457, pp. 1–33. Springer (2018). https://doi.org/10.1007/978-3-319-75632-5_1
Bartocci, E., Grosu, R.: Monitoring with uncertainty. In: Bortolussi, L., Bujorianu, M.L., Pola, G. (eds.) Proceedings Third International Workshop on Hybrid Autonomous Systems, HAS 2013, Rome, Italy, 17th March 2013. EPTCS, vol. 124, pp. 1–4 (2013)
Basin, D.A., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., Mantel, H.: Scalable offline monitoring of temporal specifications. Formal Methods Syst. Des. 49(1–2), 75–108 (2016)
Basin, D.A., Klaedtke, F., Zalinescu, E.: Failure-aware runtime verification of distributed systems. In: Harsha, P., Ramalingam, G. (eds.) 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015. LIPIcs, vol. 45, pp. 590–603. Schloss Dagstuhl, Leibniz, Zentrum fuer Informatik (2015)
Bauer, A., Falcone, Y.: Decentralised LTL monitoring. Formal Methods Syst. Des. 48(1–2), 46–93 (2016)
Bauer, A., Leucker, M.: The theory and practice of SALT. In: NASA Formal Methods—Third International Symposium, NFM 2011. Proceedings. Lecture Notes in Computer Science, vol. 6617, pp. 13–40. Springer (2011)
Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Tasiran, S. (eds.) Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Canada, March 13, 2007, Revised Selected Papers. Lecture Notes in Computer Science, vol. 4839, pp. 126–138. Springer (2007)
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010)
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14 (2011)
Bonakdarpour, B., Fraigniaud, P., Rajsbaum, S., Rosenblueth, D.A., Travers, C.: Decentralized asynchronous crash-resilient runtime verification. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada. LIPIcs, vol. 59, pp. 16:1–16:15. Schloss Dagstuhl, Leibniz, Zentrum für Informatik (2016)
Bozzelli, L., Sánchez, C.: Foundations of boolean stream runtime verification. Theor. Comput. Sci. 631, 118–138 (2016)
Brdiczka, O., Crowley, J.L., Reignier, P.: Learning situation models in a smart home. IEEE Trans. Syst. Man Cybern. Part B 39(1), 56–63 (2009)
Chen, B., Fan, Z., Cao, F.: Activity recognition based on streaming sensor data for assisted living in smart homes. In: 2015 International Conference on Intelligent Environments, IE 2015. pp. 124–127. IEEE (2015)
Chen, L., Hoey, J., Nugent, C.D., Cook, D.J., Yu, Z.: Sensor-based activity recognition. IEEE Trans. Syst. Man Cybern. Part C 42(6), 790–808 (2012)
Colombo, C., Falcone, Y.: Organising LTL monitors over distributed systems with a global clock. Formal Methods Syst. Des. 49(1–2), 109–158 (2016)
Cotard, S., Faucou, S., Béchennec, J., Queudet, A., Trinquet, Y.: A data flow monitoring service based on runtime verification for AUTOSAR. In: 14th IEEE International Conference on High Performance Computing and Communication & 9th IEEE International Conference on Embedded Software and Systems, HPCC-ICESS 2012. pp. 1508–1515. IEEE Computer Society (2012)
Crowley, J.L., Coutaz, J.: An ecological view of smart home technologies. In: De Ruyter, B., Kameas, A., Chatzimisios, P., Mavrommati, I. (eds.) Ambient Intelligence, pp. 1–16. Springer, Cham (2015)
Cumin, J., Lefebvre, G., Ramparany, F., Crowley, J.L.: A dataset of routine daily activities in an instrumented home. In: Ubiquitous Computing and Ambient Intelligence—11th International Conference, UCAmI 2017, Proceedings. Lecture Notes in Computer Science, vol. 10586, pp. 413–425. Springer (2017)
D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174. IEEE Computer Society (2005)
Decker, N., Dreyer, B., Gottschling, P., Hochberger, C., Lange, A., Leucker, M., Scheffel, T., Wegener, S., Weiss, A.: Online analysis of debug trace data for embedded systems. In: 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018, pp. 851–856. IEEE (2018)
El-Hokayem, A., Falcone, Y.: THEMIS Smart Home Artifact Repository, gitlab.inria.fr/monitoring/themis-rv18smarthome
El-Hokayem, A., Falcone, Y.: Monitoring decentralized specifications. In: Antoine El-Hokayem and Yliès Falcone [3], pp. 125–135
El-Hokayem, A., Falcone, Y.: THEMIS: a tool for decentralized monitoring algorithms. In: Antoine El-Hokayem and Yliès Falcone [3], pp. 372–375
El-Hokayem, A., Falcone, Y.: Bringing runtime verification home. In: Colombo, C., Leucker, M. (eds.) Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10-13, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11237, pp. 222–240. Springer (2018). https://doi.org/10.1007/978-3-030-03769-7
El-Hokayem, A., Falcone, Y.: On the monitoring of decentralized specifications: semantics, properties, analysis, and simulation. ACM Trans. Softw. Eng. Methodol. 29(1), 1:1–1:57 (2020)
Falcone, Y.: You should better enforce than verify. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6418, pp. 89–105. Springer (2010)
Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Engineering Dependable Software Systems, NATO science for peace and security series, d: information and communication security, vol. 34, pp. 141–175. IOS Press (2013)
Falcone, Y., Jéron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Sci. Comput. Program. 123, 2–41 (2016)
Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci and Falcone [6], pp. 103–134
Falcone, Y., Mounier, L., Fernandez, J., Richier, J.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223–262 (2011)
Falcone, Y., Nazarpour, H., Jaber, M., Bozga, M., Bensalem, S.: Tracing distributed component-based systems, a brief overview. In: Colombo, C., Leucker, M. (eds.) Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11237, pp. 417–425. Springer (2018)
Falcone, Y., Pinisetty, S.: On the runtime enforcement of timed properties. In: Finkbeiner, B., Mariani, L. (eds.) Runtime Verification—19th International Conference, RV 2019, Porto, Portugal, October 8–11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11757, pp. 48–69. Springer (2019)
Gorostiaga, F., Sánchez, C.: Striver: Stream runtime verification for real-time event-streams. In: Colombo, C., Leucker, M. (eds.) Runtime Verification—18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11237, pp. 282–298. Springer (2018)
Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C.: Spatel: A novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 189–198. HSCC ’15, ACM, New York, NY, USA (2015)
Hallé, S., Gaboury, S., Bouchard, B.: Activity recognition through complex event processing: First findings. In: Artificial Intelligence Applied to Assistive Technologies and Smart Environments, Papers from the 2016 AAAI Workshop. AAAI Workshops, vol. WS-16-01. AAAI Press (2016)
Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions. Lecture Notes in Computer Science, vol. 4171, pp. 374–383. Springer (2005)
Institute for Software Engineering and Programming Languages: LamaConv—Logics and Automata Converter Library. http://www.isp.uni-luebeck.de/lamaconv
van Kasteren, T., Englebienne, G., Kröse, B.J.A.: Transferring knowledge of activity recognition across sensor networks. In: Pervasive Computing, 8th International Conference, Pervasive 2010. Proceedings. Lecture Notes in Computer Science, vol. 6030, pp. 283–300. Springer (2010)
Katz, S.: Assessing self-maintenance: activities of daily living, mobility, and instrumental activities of daily living. J. Am. Geriatr. Soc. 31(12), 721–727 (1983)
Kazemlou, S., Bonakdarpour, B.: Crash-resilient decentralized synchronous runtime verification. In: 37th IEEE Symposium on Reliable Distributed Systems, SRDS 2018, Salvador, Brazil, October 2–5, 2018. pp. 207–212. IEEE Computer Society (2018)
Lago, P., Lang, F., Roncancio, C., Jiménez-Guarín, C., Mateescu, R., Bonnefond, N.: The ContextAct@A4H real-life dataset of daily-living activities - activity recognition using model checking. In: Modeling and Using Context—10th International and Interdisciplinary Conference, CONTEXT 2017, Proceedings. Lecture Notes in Computer Science, vol. 10257, pp. 175–188. Springer (2017)
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)
Leucker, M., Schmitz, M., à Tellinghusen, D.: Runtime verification for interconnected medical devices. In: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications—7th International Symposium, ISoLA 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9953, pp. 380–387 (2016)
Majumder, S., Aghayi, E., Noferesti, M., Memarzadeh-Tehran, H., Mondal, T., Pang, Z., Deen, M.J.: Smart homes for elderly healthcare—recent advances and research challenges. Sensors 17(11), 2496 (2017)
Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Proceedings. Lecture Notes in Computer Science, vol. 5014, pp. 148–164. Springer (2008)
Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, Hyderabad, India, May 25–29, 2015. pp. 494–503. IEEE Computer Society (2015)
Ogale, V.A., Garg, V.K.: Detecting temporal logic predicates on distributed computations. In: Pelc, A. (ed.) Distributed Computing, 21st International Symposium, DISC 2007, Lemesos, Cyprus, September 24–26, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4731, pp. 420–434. Springer (2007)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October–1 November 1977. pp. 46–57. IEEE Computer Society (1977)
Shapiro, M., Preguiça, N.M., Baquero, C., Zawirski, M.: Conflict-free replicated data types. In: Défago, X., Petit, F., Villain, V. (eds.) Stabilization, Safety, and Security of Distributed Systems—13th International Symposium, SSS 2011, Grenoble, France, October 10–12, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6976, pp. 386–400. Springer (2011)
Szyperski, C.A., Gruntz, D., Murer, S.: Component software—beyond object-oriented programming. Addison-Wesley component software series, 2nd edn. Addison-Wesley, London (2002)
Tapia, E.M., Intille, S.S., Larson, K.: Activity recognition in the home using simple and ubiquitous sensors. In: Pervasive Computing, Second International Conference, PERVASIVE 2004, Vienna, Austria, April 21–23, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3001, pp. 158–175. Springer (2004)