Static and dynamic property-preserving updates. (English) Zbl 1497.68251
Summary: Systems need to be updated to last for a long time in a dynamic environment. The update can be performed both statically, by restarting the system, or dynamically. Updates have to preserve the desirable properties of the system, while possibly enforcing new ones. We consider a simple yet general update mechanism, replacing a component of the system with a new one. We define contexts and components as Constraint Automata interacting via either asynchronous or synchronous communication, and we express properties using Constraint Automata too. Then we build most general updates preserving specific properties, considering both a single property and all the properties satisfied by the original system, in a given context or in all possible contexts. To tackle also dynamic update, we consider the state transfer problem, namely how to find the state in which the new component should be started to ensure a correct overall behaviour.
MSC:
| 68Q45 | Formal languages and automata |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Seifzadeh, H.; Abolhassani, H.; Moshkenani, M. S., A survey of dynamic software updating, J. Softw. Evol. Process, 25, 5, 535-568 (2013) |
| [2] | Leite, L. A.F.; Oliva, G. A.; Nogueira, G. M.; Gerosa, M. A.; Kon, F.; Milojicic, D. S., A systematic literature review of service choreography adaptation, Serv. Oriented Comput. Appl., 7, 3, 199-216 (2013) |
| [3] | Huebscher, M. C.; McCann, J. A., A survey of autonomic computing - degrees, models, and applications, ACM Comput. Surv., 40, 3, 7:1-7:28 (2008) |
| [4] | Hayden, C. M.; Magill, S.; Hicks, M.; Foster, N.; Foster, J. S., Specifying and verifying the correctness of dynamic software updates, (VSTTE. VSTTE, LNCS, vol. 7152 (2012), Springer), 278-293 |
| [5] | Hansell, S., Glitch makes teller machines take twice what they give, The New York Times |
| [6] | Gupta, D.; Jalote, P.; Barua, G., A formal framework for on-line software version change, IEEE Trans. Softw. Eng., 22, 2, 120-131 (1996) |
| [7] | Baumann, A.; Heiser, G.; Appavoo, J.; Silva, D. D.; Krieger, O.; Wisniewski, R. W.; Kerr, J., Providing dynamic update in an operating system, (USENIX Annual Technical Conference (2005), USENIX), 279-291 |
| [8] | Chen, H.; Chen, R.; Zhang, F.; Zang, B.; Yew, P., Live updating operating systems using virtualization, (VEE (2006), ACM), 35-44 |
| [9] | Baier, C.; Blechmann, T.; Klein, J.; Klüppelholz, S., Formal verification for components and connectors, (FMCO. FMCO, LNCS, vol. 5751 (2008), Springer), 82-101 · Zbl 1254.68143 |
| [10] | Baier, C.; Sirjani, M.; Arbab, F.; Rutten, J., Modeling component connectors in Reo by constraint automata, Sci. Comput. Program., 61, 2, 75-113 (2006) · Zbl 1105.68058 |
| [11] | Arbab, F., Reo: a channel-based coordination model for component composition, Math. Struct. Comput. Sci., 14, 3, 329-366 (2004) · Zbl 1085.68552 |
| [12] | Sirjani, M.; Jaghoori, M. M.; Baier, C.; Arbab, F., Compositional semantics of an actor-based language using constraint automata, (Coordination. Coordination, LNCS, vol. 4038 (2006), Springer), 281-297 |
| [13] | Tsai, M.; Tsay, Y.; Hwang, Y., GOAL for games, omega-automata, and logics, (CAV. CAV, LNCS, vol. 8044 (2013), Springer), 883-889 |
| [14] | Bresolin, D.; Lanese, I., Most general property-preserving updates, (LATA. LATA, LNCS, vol. 10168 (2017), Springer), 367-379 · Zbl 1485.68135 |
| [15] | Lange, M., Weak automata for the linear time μ-calculus, (VMCAI. VMCAI, LNCS, vol. 3385 (2005), Springer), 267-281 · Zbl 1112.68093 |
| [16] | Kobayashi, N.; Ong, C. L., Complexity of model checking recursion schemes for fragments of the modal mu-calculus, Log. Methods Comput. Sci., 7, 4, 9:1-9:24 (2011) · Zbl 1237.68124 |
| [17] | Emerson, E. A., Temporal and modal logic, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B) (1990), MIT Press), 995-1072 · Zbl 0900.03030 |
| [18] | Villa, T.; Yevtushenko, N.; Brayton, R. K.; Mishchenko, A.; Petrenko, A.; Sangiovanni-Vincentelli, A., The Unknown Component Problem - Theory and Application (2012), Springer · Zbl 1248.68023 |
| [19] | Villa, T.; Petrenko, A.; Yevtushenko, N.; Mishchenko, A.; Brayton, R. K., Component-based design by solving language equations, Proc. IEEE, 103, 11, 2152-2167 (2015) |
| [20] | Chatterjee, K.; Doyen, L., Games with a weak adversary, (ICALP. ICALP, LNCS, vol. 8573 (2014), Springer), 110-121 · Zbl 1409.68169 |
| [21] | Chrobak, M., Finite automata and unary languages, Theor. Comput. Sci., 47, 3, 149-158 (1986) · Zbl 0638.68096 |
| [22] | Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), The MIT Press · Zbl 1179.68076 |
| [23] | Giuffrida, C.; Iorgulescu, C.; Kuijsten, A.; Tanenbaum, A. S., Back to the future: fault-tolerant live update with time-traveling state transfer, (LISA (2013), USENIX Association), 89-104 |
| [24] | Bonchi, F.; Brogi, A.; Corfini, S.; Gadducci, F., A behavioural congruence for web services, (FSEN. FSEN, LNCS, vol. 4767 (2007), Springer), 240-256 · Zbl 1141.68501 |
| [25] | Krause, C.; Giese, H.; de Vink, E. P., Compositional and behavior-preserving reconfiguration of component connectors in Reo, J. Vis. Lang. Comput., 24, 3, 153-168 (2013) |
| [26] | Harbird, L.; Galloway, A.; Paige, R. F., Towards a model-based refinement process for contractual state machines, (ISORCW (2010), IEEE), 108-115 |
| [27] | Prehofer, C., Property preservation for extension patterns of state transition diagrams, (Integrated Formal Methods. Integrated Formal Methods, LNCS, vol. 9681 (2016), Springer), 260-274 |
| [28] | Schrefl, M.; Stumptner, M., Behavior-consistent specialization of object life cycles, ACM Trans. Softw. Eng. Methodol., 11, 1, 92-148 (2002) |
| [29] | Schneider, S.; Treharne, H.; Wehrheim, H., The behavioural semantics of Event-B refinement, Form. Asp. Comput., 26, 2, 251-280 (2014) · Zbl 1342.68211 |
| [30] | Duggan, D., Type-based hot swapping of running modules, Acta Inform., 41, 4-5, 181-220 (2005) · Zbl 1067.68038 |
| [31] | Stoyle, G. P.; Hicks, M. W.; Bierman, G. M.; Sewell, P.; Neamtiu, I., Mutatis mutandis: safe and predictable dynamic software updating, (POPL (2005), ACM), 183-194 · Zbl 1369.68157 |
| [32] | Anderson, G.; Rathke, J., Dynamic software update for message passing programs, (APLAS. APLAS, LNCS, vol. 7705 (2012), Springer), 207-222 |
| [33] | Dalla Preda, M.; Gabbrielli, M.; Giallorenzo, S.; Lanese, I.; Mauro, J., Dynamic choreographies: theory and implementation, Log. Methods Comput. Sci., 13, 2 (2017) · Zbl 1398.68088 |
| [34] | Dalla Preda, M.; Giallorenzo, S.; Lanese, I.; Mauro, J.; Gabbrielli, M., AIOCJ: a choreographic framework for safe adaptive distributed applications, (SLE. SLE, LNCS, vol. 8706 (2014), Springer), 161-170 |
| [35] | Coppo, M.; Dezani-Ciancaglini, M.; Venneri, B., Self-adaptive multiparty sessions, Serv. Oriented Comput. Appl., 9, 3-4, 249-268 (2015) |
| [36] | Di Giusto, C.; Pérez, J. A., Disciplined structured communications with consistent runtime adaptation, (SAC (2013), ACM), 1913-1918 |
| [37] | Zhang, J.; Goldsby, H.; Cheng, B. H.C., Modular verification of dynamically adaptive systems, (AOSD (2009), ACM), 161-172 |
| [38] | Krause, C.; Maraikar, Z.; Lazovik, A.; Arbab, F., Modeling dynamic reconfigurations in Reo using high-level replacement systems, Sci. Comput. Program., 76, 1, 23-36 (2011) · Zbl 1211.68052 |
| [39] | Krause, C., Distributed port automata, Electron. Commun. EASST, 41 (2011) |
| [40] | Oliveira, N.; Barbosa, L. S., On the reconfiguration of software connectors, (SAC (2013), ACM), 1885-1892 |
| [41] | Djoko-Djoko, S.; Douence, R.; Fradet, P., Aspects preserving properties, (PEPM (2008), ACM), 135-145 |
| [42] | Andova, S.; Groenewegen, L.; de Vink, E., Dynamic adaptation with distributed control in Paradigm, Sci. Comput. Program., 94, 333-361 (2014) |
| [43] | Alur, R.; La Torre, S., Deterministic generators and games for LTL fragments, ACM Trans. Comput. Log., 5, 1, 1-25 (2004) · Zbl 1366.03181 |
| [44] | Bloem, R.; Jobstmann, B.; Piterman, N.; Pnueli, A.; Sa’ar, Y., Synthesis of reactive(1) designs, J. Comput. Syst. Sci., 78, 3, 911-938 (2012) · Zbl 1247.68050 |
| [45] | Aziz, A.; Balarin, F.; Brayton, R. K.; DiBenedetto, M. D.; Saldanha, A., Supervisory control of finite state machines, (CAV. CAV, LNCS, vol. 939 (1995), Springer), 279-292 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
