Most General Property-Preserving Updates

  • Davide Bresolin
  • Ivan LaneseEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10168)


Systems need to be updated to last for a long time in a dynamic environment, and to cope with changing requirements. It is important for updates to preserve the desirable properties of the system under update, while possibly enforcing new ones.

Here we consider a simple yet general update mechanism, which replaces a component of the system with a new one. The context, i.e., the rest of the system, remains unchanged. 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 which preserve 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.


Model Check Winning Strategy Sink State Model Check Problem Deadlock Freedom 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Logic 5(1), 1–25 (2004)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Anderson, G., Rathke, J.: Dynamic software update for message passing programs. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 207–222. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-35182-2_15 CrossRefGoogle Scholar
  3. 3.
    Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Aziz, A., Balarin, F., Brayton, R.K., Di Benedetto, M.D., Saldanha, A., Sangiovanni-Vincentelli, A.L.: Supervisory control of finite state machines. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 279–292. Springer, Heidelberg (1995). doi: 10.1007/3-540-60045-0_57 CrossRefGoogle Scholar
  5. 5.
    Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61(2), 75–113 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: Formal verification for components and connectors. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 82–101. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04167-9_5 CrossRefGoogle Scholar
  7. 7.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Bonchi, F., Brogi, A., Corfini, S., Gadducci, F.: A behavioural congruence for web services. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 240–256. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-75698-9_16 CrossRefGoogle Scholar
  9. 9.
    Bresolin, D., Lanese, I.: Most general property-preserving updates (TR) (2016).
  10. 10.
    Chatterjee, K., Doyen, L.: Games with a weak adversary. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 110–121. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-43951-7_10 Google Scholar
  11. 11.
    Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies. In: Holvoet, T., Viroli, M. (eds.) COORDINATION 2015. LNCS, vol. 9037, pp. 67–82. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-19282-6_5 Google Scholar
  12. 12.
    Di Giusto, C., Pérez, J.A.: Disciplined structured communications with consistent runtime adaptation. In: SAC, pp. 1913–1918. ACM (2013)Google Scholar
  13. 13.
    Duggan, D.: Type-based hot swapping of running modules. Acta Inf. 41(4–5), 181–220 (2005)CrossRefzbMATHGoogle Scholar
  14. 14.
    Hayden, C.M., Magill, S., Hicks, M., Foster, N., Foster, J.S.: Specifying and verifying the correctness of dynamic software updates. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 278–293. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-27705-4_22 CrossRefGoogle Scholar
  15. 15.
    Huebscher, M.C., McCann, J.A.: A survey of autonomic computing - degrees, models, and applications. ACM Comput. Surv. 40(3) (2008). Article No. 7Google Scholar
  16. 16.
    Lange, M.: Weak Automata for the Linear Time \(\mu \)-Calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 267–281. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-30579-8_18 CrossRefGoogle Scholar
  17. 17.
    Leite, L.A.F., et al.: A systematic literature review of service choreography adaptation. Serv. Oriented Comput. Appl. 7(3), 199–216 (2013)CrossRefGoogle Scholar
  18. 18.
    Oliveira, N., Barbosa, L.S.: On the reconfiguration of software connectors. In: SAC, pp. 1885–1892. ACM (2013)Google Scholar
  19. 19.
    Seifzadeh, H., Abolhassani, H., Moshkenani, M.S.: A survey of dynamic software updating. J. Softw.: Evol. Process 25(5), 535–568 (2013)Google Scholar
  20. 20.
    Sirjani, M., Jaghoori, M.M., Baier, C., Arbab, F.: Compositional semantics of an actor-based language using constraint automata. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 281–297. Springer, Heidelberg (2006). doi: 10.1007/11767954_18 CrossRefGoogle Scholar
  21. 21.
    Tsai, M.-H., Tsay, Y.-K., Hwang, Y.-S.: GOAL for games, omega-automata, and logics. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 883–889. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39799-8_62 CrossRefGoogle Scholar
  22. 22.
    Villa, T., et al.: The Unknown Component Problem - Theory and Application. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  23. 23.
    Zhang, J., Goldsby, H., Cheng, B.H.C.: Modular verification of dynamically adaptive systems. In: AOSD, pp. 161–172. ACM (2009)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.University of PadovaPaduaItaly
  2. 2.Focus TeamUniversity of Bologna/InriaBolognaItaly

Personalised recommendations