Live synthesis

Innovations in Systems and Software Engineering - 2022
Bernd Finkbeiner1, Felix Klein1, Niklas Metzger1
1CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Tóm tắt

Abstract

Synthesis automatically constructs an implementation that satisfies a given logical specification. In this paper, we study the live synthesis problem, where the synthesized implementation replaces an already running system. In addition to satisfying its own specification, the synthesized implementation must guarantee a sound transition from the previous implementation. This version of the synthesis problem is highly relevant in “always-on” applications, where updates happen while the system is running. To specify the correct handover between the old and new implementation, we introduce an extension of linear-time temporal logic (LTL) called LiveLTL. A LiveLTL specification defines separate requirements on the two implementations and ensures that the new implementation satisfies, in addition to its own requirements, any obligations left unfinished by the old implementation. For specifications in LiveLTL, we show that the live synthesis problem can be solved within the same complexity bound as standard reactive synthesis, i.e., in 2EXPTIME. Our experiments show the necessity of live synthesis for LiveLTL specifications created from benchmarks of SYNTCOMP and robot control.

Từ khóa


Tài liệu tham khảo

Baumann A, Heiser G, Appavoo J, Silva DD, Krieger O, Wisniewski RW, Kerr J (2005) Providing dynamic update in an operating system. In: USENIX

Biere A (2007) The AIGER and-inverter graph (AIG) format version 20071012. Technical Report 07/1, Institute for formal models and verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria

Chen Y, Zhang Y, Wang Z, Xia L, Bao C, Wei T (2017) Adaptive android kernel live patching. In: Kirda E, Ristenpart T (eds) USENIX Security

Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault E, Xu L (2016) Spot 2.0 - A framework for LTL and $$\omega $$ -automata manipulation. In: ATVA, LNCS. https://doi.org/10.1007/978-3-319-46520-3_8

Esparza J, Kretínský J (2014) From LTL to deterministic automata: a safraless compositional approach. In: CAV. https://doi.org/10.1007/978-3-319-08867-9_13

Esparza J, Kretínský J, Raskin J, Sickert S (2017) From LTL and limit-deterministic büchi automata to deterministic parity automata. In: TACAS. https://doi.org/10.1007/978-3-662-54577-5_25

Fabry RS (1976) How to design a system in which modules can be changed on the fly. In: ICSE. IEEE Computer Society, Proceedings of the 2nd international conference on Software engineering, pp. 470–476

Faymonville P, Finkbeiner B, Tentrup L (2017) Bosy: An experimentation framework for bounded synthesis. In: CAV, pp. 470–476. https://doi.org/10.1007/978-3-319-63390-9_17

Finkbeiner B, Klein F, Metzger N (2021) Live synthesis. In: Hou Z, Ganesh V (eds) Automated technology for verification and analysis - 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, Lecture Notes in Computer Science, vol. 12971, pp. 153–169. Springer. https://doi.org/10.1007/978-3-030-88885-5_11

Frieder O, Segal ME (1991) On dynamically updating a computer program: from concept to prototype. JSS. https://doi.org/10.1016/0164-1212(91)90096-O

Ghezzi C, Greenyer J, Manna VPL (2012) Synthesizing dynamically updating controllers from changes in scenario-based specifications. In: SEAMS. IEEE Computer Society. https://doi.org/10.1109/SEAMS.2012.6224401

Giacomo GD, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Rossi F

(ed) IJCAI 2013, Proceedings of the 23rd international joint conference on artificial intelligence, Beijing, China, August 3-9, 2013, pp. 854-860. IJCAI/AAAI. http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997

Giuffrida C, Kuijsten A, Tanenbaum AS Safe and automatic live update for operating systems. SIGPLAN Not. 48. https://doi.org/10.1145/2499368.2451147

Gregersen AR, Jørgensen BN (2009) Dynamic update of java applications - balancing change flexibility vs programming transparency. JSWM. https://doi.org/10.1002/smr.406

Hayden CM, Magill S, Hicks M, Foster N, Foster JS (2012) Specifying and verifying the correctness of dynamic software updates. In: Joshi R, Müller P, Podelski A (eds) VSTTE, LNCS. https://doi.org/10.1007/978-3-642-27705-4_22

Hjalmtysson G, Gray R Dynamic C++ classes - A lightweight mechanism to update code in a running program. In: USENIX 1998. USENIX Association

Jacobs S, Basset N, Bloem R, Brenguier R, Colange M, Faymonville P, Finkbeiner B, Khalimov A, Klein F, Michaud T, Pérez GA, Raskin J, Sankur O, Tentrup L (2017) SYNTCOMP 2017. In: SYNT@CAV. https://doi.org/10.4204/EPTCS.260.10

Li J, Zhang L, Pu G, Vardi MY, He J (2014) LTLf satisfiability checking. In: ECAI, FAIA. https://doi.org/10.3233/978-1-61499-419-0-513

Makris K, Ryu KD (2007) Dynamic and adaptive updates of non-quiescent subsystems in commodity operating system kernels. In: EuroSys. ACM. https://doi.org/10.1145/1272996.1273031

Manna VPL, Greenyer J, Ghezzi C, Brenner C (2013) Formalizing correctness criteria of dynamic updates derived from specification changes. In: SEAMS. IEEE Computer Society. https://doi.org/10.1109/SEAMS.2013.6595493

Menghi C, Tsigkanos C, Berger T, Pelliccione P, Ghezzi C (2018) Property specification patterns for robotic missions. In: ICSE 2018. ACM. https://doi.org/10.1145/3183440.3195044

Meyer PJ, Sickert S, Luttenberger M (2018) Strix: explicit reactive synthesis strikes back! In: Chockler H, Weissenbacher G (eds) CAV 2018, LNCS. https://doi.org/10.1007/978-3-319-96145-3_31

Nahabedian L, Braberman VA, D’Ippolito N, Honiden S, Kramer J, Tei K, Uchitel S (2016) Assured and correct dynamic update of controllers. In: SEAMS@ICSE 2016. ACM. https://doi.org/10.1145/2897053.2897056

Pnueli A (1977) The temporal logic of programs. In: SFCS. https://doi.org/10.1109/SFCS.1977.32

Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Conference record of the sixteenth annual ACM symposium on principles of programming languages, Austin, Texas, USA, January 11-13, pp. 179–190. ACM Press (1989). https://doi.org/10.1145/75277.75293

Thông tin
Thông tin xuất bản

Innovations in Systems and Software Engineering

Thông tin tác giả