Advertisement

Software & Systems Modeling

, Volume 18, Issue 5, pp 2875–2906 | Cite as

Certifying delta-oriented programs

  • Vítor RodriguesEmail author
  • Simone Donetti
  • Ferruccio Damiani
Regular Paper

Abstract

A major design concern in modern software development frameworks is to ensure that mechanisms for updating code running on remote devices comply with given safety specifications. This paper presents a delta-oriented approach for implementing product lines where software reuse is achieved at the three levels of state-diagram modeling, C/\(\text {C}^{_{_{_{++}}}} \)source code and binary code. A safety specification is expressed on the properties of reusable software libraries that can be dynamically loaded at run time after an over-the-air update. The compilation of delta-engineered code is certified using the framework of proof-carrying code in order to guarantee safety of software updates on remote devices. An empirical evaluation of the computational cost associated with formal safety checks is done by means of experimentation.

Keywords

Model-driven development Delta-oriented programming Safety properties Proof-carrying code Runtime systems 

Notes

Acknowledgements

We thank the anonymous SoSyM referees for comments and suggestions for improving the paper.

References

  1. 1.
    Albert, E., Arenas, P., Puebla, G., Hermenegildo, M.: Reduced Certificates for Abstraction-Carrying Code, pp. 163–178. Springer, Berlin (2006).  https://doi.org/10.1007/11799573_14 zbMATHCrossRefGoogle Scholar
  2. 2.
    Apel, S., Batory, D., Kstner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, Berlin (2013). IncorporatedCrossRefGoogle Scholar
  3. 3.
    Arndt, J., Behlert, S., et al.: SUSE Linux. Technical report. Novel Inc, Washington (2006)Google Scholar
  4. 4.
    Ayavoo, D., Pont, M.J., Parker, S.: Observing the development of a reliable embedded system. In: Proceedings of the 10th Ada-Europe International Conference on Reliable Software Technologies, Springer, Berlin. Ada-Europe’05, pp. 167–179 (2005).  https://doi.org/10.1007/11499909_14
  5. 5.
    Bailey, J.W., Basili, V.R.: A meta-model for software development resource expenditures. In: Proceedings of the 5th International Conference on Software Engineering. IEEE Press, Piscataway, ICSE ’81, pp. 107–116 (1981)Google Scholar
  6. 6.
    Basili, V.R., Weiss, D.M.: A methodology for collecting valid software engineering data. IEEE Trans. Softw. Eng. 10(6), 728–738 (1984).  https://doi.org/10.1109/TSE.1984.5010301 CrossRefGoogle Scholar
  7. 7.
    Basili, V.R., Selby, R.W., Hutchens, D.H.: Experimentation in software engineering. IEEE Trans. Softw. Eng. 12(7), 733–743 (1986)CrossRefGoogle Scholar
  8. 8.
    Batory, D., Sarvela, J., Rauschmayer, A.: Scaling step-wise refinement. IEEE Trans. Softw. Eng. 30(6), 355–371 (2004)CrossRefGoogle Scholar
  9. 9.
    Bavota, G.: Using structural and semantic information to support software refactoring. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 1479–1482 (2012).  https://doi.org/10.1109/ICSE.2012.6227057
  10. 10.
    Berger, T., Rublack, R., Nair, D., Atlee, J.M., Becker, M., Czarnecki, K., Wąsowski, A.: A survey of variability modeling in industrial practice. In: Proceedings of the Seventh International Workshop on Variability Modelling of Software-Intensive Systems, ACM, New York, VaMoS ’13, pp. 7:1–7:8 (2013).  https://doi.org/10.1145/2430502.2430513
  11. 11.
    Bernardeschi, C., Francesco, N.D., Lettieri, G., Martini, L., Masci, P.: Decomposing bytecode verification by abstract interpretation. ACM Trans Program Lang Syst 31(1), 3:1–3:63 (2008).  https://doi.org/10.1145/1452044.1452047 CrossRefGoogle Scholar
  12. 12.
    Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions, 1st edn. Springer, Berlin (2010)Google Scholar
  13. 13.
    Bezemer, C.P., Mcintosh, S., Adams, B., German, D.M., Hassan, A.E.: An empirical study of unspecified dependencies in make-based build systems. Empirical Softw Engg 22(6), 3117–3148 (2017).  https://doi.org/10.1007/s10664-017-9510-8 CrossRefGoogle Scholar
  14. 14.
    Biere, A., Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability Volume 185: Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)zbMATHGoogle Scholar
  15. 15.
    Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: a comparative survey. ACM Comput. Surv. 38(4), 1–62 (2006).  https://doi.org/10.1145/1177352.1177354 CrossRefGoogle Scholar
  16. 16.
    Brown, A.W., Wallnau, K.C.: A framework for evaluating software technology. IEEE Softw. 13(5), 39–49 (1996).  https://doi.org/10.1109/52.536457 CrossRefGoogle Scholar
  17. 17.
    Bryant, R.E., O’Hallaron, D.R.: Computer Systems: A Programmer’s Perspective, 2nd edn. Addison-Wesley Publishing Company, New York (2010)Google Scholar
  18. 18.
    Burow, N., Carr, S.A., Brunthaler, S., Payer, M., Nash, J., Larsen, P., Franz, M.: Control-flow integrity: precision, security, and performance. ACM Comput. Surv. 50:16:1–16, 33 (2017).  https://doi.org/10.1145/3054924 CrossRefGoogle Scholar
  19. 19.
    Calcote, J.: Autotools: A Practitioner’s Guide to GNU Autoconf, Automake, and Libtool. No Starch Press, San Francisco (2010)Google Scholar
  20. 20.
    Calder, B., Phillips, L.W., Tybout, A.: The concept of external validity. J. Consum. Res. 9, 240–244 (1982)CrossRefGoogle Scholar
  21. 21.
    Catuogno, L., Visconti, I.: A format-independent architecture for run-time integrity checking of executable code. In: Cimato, S., Persiano, G., Galdi, C. (eds.) Security in Communication Networks, pp. 219–233. Springer, Berlin (2003)CrossRefGoogle Scholar
  22. 22.
    Chesta, C., Damiani, F., Dobriakova, L., Guernieri, M., Martini, S., Nieke, M., Rodrigues, V., Schuster, S.: A toolchain for delta-oriented modeling of software product lines. In: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications—7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part II, pp. 497–511 (2016).  https://doi.org/10.1007/978-3-319-47169-3_40
  23. 23.
    Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison Wesley Longman, Boston (2001)Google Scholar
  24. 24.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ACM, New York, NY, USA, POPL ’77, pp. 238–252 (1977).  https://doi.org/10.1145/512950.512973
  25. 25.
    De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, TACAS’08/ETAPS’08, pp. 337–340 (2008)Google Scholar
  26. 26.
    DeTreville, J., Leijen, D., Swierstra, W.: Dependable software deployment. Technical report, Microsoft Research (2006)Google Scholar
  27. 27.
    Donald, J.: Improved Portability of Shared Libraries. Technical report, Princeton University, Princeton (2003)Google Scholar
  28. 28.
    Drepper, U.: How to Write Shared Libraries. Technical Report. Red Hat Inc, Raleigh (2011)Google Scholar
  29. 29.
    Drusinsky, D.: Chapter 1—formal requirements and finite automata overview. In: Drusinsky, D. (ed) Modeling and Verification Using UML Statecharts, Newnes, Burlington, pp. 1–41 (2006).  https://doi.org/10.1016/B978-075067949-7/50003-9
  30. 30.
    Drusinsky, D.: Chapter 2—Statecharts. In: Drusinsky, D. (ed.) Modeling and Verification Using UML Statecharts, pp. 43–102. Newnes, Burlington (2006).  https://doi.org/10.1016/B978-075067949-7/50004-0 CrossRefGoogle Scholar
  31. 31.
    Ducasse, S., Nierstrasz, O., Schärli, N., Wuyts, R., Black, A.P.: Traits: a mechanism for fine-grained reuse. ACM Trans. Program Lang. Syst. 28(2), 331–388 (2006).  https://doi.org/10.1145/1119479.1119483 CrossRefGoogle Scholar
  32. 32.
    European Commission (2017) eCall: Time saved = lives saved. https://ec.europa.eu/digital-single-market/en/ecall-time-saved-lives-saved
  33. 33.
    Fenton, N.E.: Software Metrics: A Rigorous Approach. Chapman & Hall Ltd, London (1991)zbMATHGoogle Scholar
  34. 34.
    Garfinkel, S.: PGP: Pretty Good Privacy, 1st edn. O’Reilly & Associates Inc, Sebastopol (1996)zbMATHGoogle Scholar
  35. 35.
    Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. Proceedings, Springer, Berlin, pp. 306–320 (2009).  https://doi.org/10.1007/978-3-642-02658-4_25
  36. 36.
    GmbH VSI (2018) RTT-DCC: Data and Control Coupling Analyser. https://www.verified.de/products/rtt-dcc/. Accessed 31 July 2018
  37. 37.
    Gosling, J., Joy, B., Steele, G.L., Bracha, G., Buckley, A.: The Java Language Specification, Java SE 8 Edition, 1st edn. Addison-Wesley Professional, Boston (2014)Google Scholar
  38. 38.
    Guo, C., Ren, S., Jiang, Y., Wu, P.L., Sha, L., Berlin, R.B. Jr: Transforming medical best practice guidelines to executable and verifiable statechart models. In: Proceedings of the 7th International Conference on Cyber-Physical Systems. IEEE Press, Piscataway, ICCPS ’16, pp 34:1–34:10 (2016)Google Scholar
  39. 39.
    Haber, A., Rendel, H., Rumpe, B., Schaefer, I., van der Linden, F.: Hierarchical variability modeling for software architectures. In: Proceedings of the 15th International Software Product Line Conference, IEEE, pp. 150–159(2011).  https://doi.org/10.1109/SPLC.2011.28
  40. 40.
    Habets, T.: Shared libraries diamond problem (2012). https://blog.habets.se/2012/05/Shared-libraries-diamond-problem.html. Accessed 31 July 2018
  41. 41.
    Hallsteinsen, S., Hinchey, M., Park, S., Schmid, K.: Dynamic software product lines. Computer 41(4), 93–95 (2008).  https://doi.org/10.1109/MC.2008.123 CrossRefGoogle Scholar
  42. 42.
    Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The Statemate Approach, 1st edn. McGraw-Hill Inc, New York (1998)Google Scholar
  43. 43.
    Hawkins, R.D., Kelly, T.P.: Software safety assurance—what is sufficient? In: 4th IET International Conference on Systems Safety 2009. Incorporating the SaRS Annual Conference, pp. 1–6 (2009).  https://doi.org/10.1049/cp.2009.1542
  44. 44.
    Hermenegildo, M.V., Albert, E., López-García, P., Puebla, G.: Abstraction carrying code and resource-awareness. In: Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, ACM, New York, PPDP ’05, pp. 1–11 (2005).  https://doi.org/10.1145/1069774.1069775
  45. 45.
    Hutchens, D.H., Basili, V.R.: System structure analysis: clustering with data bindings. IEEE Trans. Softw. Eng. 11(8), 749–757 (1985).  https://doi.org/10.1109/TSE.1985.232524 CrossRefGoogle Scholar
  46. 46.
    Hutchinson, J., Rouncefield, M., Whittle, J.: Model-driven engineering practices in industry. In: Proceedings of the 33rd International Conference on Software Engineering, ACM, New York, NY, USA, ICSE ’11, pp. 633–642 (2011).  https://doi.org/10.1145/1985793.1985882
  47. 47.
    Iscoe, N., Williams, G.B., Arango, G.: Domain modeling for software engineering., In: [1991 Proceedings] 13th International Conference on Software Engineering, pp. 340–343 (1991).  https://doi.org/10.1109/ICSE.1991.130660
  48. 48.
    Jiang, L., Su, Z.: Profile-guided program simplification for effective testing and analysis. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ACM, New York, SIGSOFT ’08/FSE-16, pp. 48–58 (2008).  https://doi.org/10.1145/1453101.1453110
  49. 49.
    Kernighan, B.W., Ritchie, D.M.: The M4 Macro Processor. Technical report, Bell Laboratories (1977)Google Scholar
  50. 50.
    Kirovski, D., Drinić, M., Potkonjak, M.: Enabling trusted software integrity. SIGPLAN Not. 37(10), 108–120 (2002).  https://doi.org/10.1145/605432.605409 CrossRefGoogle Scholar
  51. 51.
    Krueger, C.W.: Software reuse. ACM Comput. Surv. 24(2), 131–183 (1992).  https://doi.org/10.1145/130844.130856 CrossRefGoogle Scholar
  52. 52.
    Lienhardt, M., Damiani, F., Testa, L., Turin, G.: On checking delta-oriented product lines of statecharts. Sci. Comput. Program. 166, 3–34 (2018).  https://doi.org/10.1016/j.scico.2018.05.007 CrossRefGoogle Scholar
  53. 53.
    Lindholm, T., Yellin, F.: Java Virtual Machine Specification, 2nd edn. Addison-Wesley Longman Publishing Co. Inc, Boston (1999)Google Scholar
  54. 54.
    Martin, J.C.: Introduction to Languages and the Theory of Computation, 2nd edn. McGraw-Hill Higher Education, New York (1997)zbMATHGoogle Scholar
  55. 55.
    McCabe, T.J.: A complexity measure. In: Proceedings of the 2nd International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, ICSE ’76, p. 407 (1976)Google Scholar
  56. 56.
    Menon, V., Pingali, K.: A case for source-level transformations in matlab. SIGPLAN Not. 35(1), 53–65 (1999).  https://doi.org/10.1145/331963.331972 CrossRefGoogle Scholar
  57. 57.
    Moura, L., Bjørner, N.: Satisfiability modulo theories: an appetizer. In: Oliveira, M.V., Woodcock, J. (eds.) Formal Methods: Foundations and Applications, pp. 23–36. Springer, Berlin (2009).  https://doi.org/10.1007/978-3-642-10452-7_3 CrossRefGoogle Scholar
  58. 58.
    Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, New York, POPL ’97, pp. 106–119 (1997).  https://doi.org/10.1145/263699.263712
  59. 59.
    Nelson, G. (ed.): Systems Programming with Modula-3. Prentice-Hall Inc, Upper Saddle River (1991)Google Scholar
  60. 60.
    Oliveira, N., Varanda Pereira, M.J., Henriques, P.R., da Cruz, D.: Domain-specific languages—a theoretical survey. In: Proceedings of the 3rd Compilers, Programming Languages, Related Technologies and Applications (CoRTA’2009), pp. 35–46 (2009)Google Scholar
  61. 61.
    Parkes, A.P.: Finite State Transducers, pp. 189–207. Springer, London (2008).  https://doi.org/10.1007/978-1-84800-121-3_8 CrossRefGoogle Scholar
  62. 62.
    Percival, C.: Matching with mismatches and assorted applications. Ph.D. thesis, University of Oxford (2006)Google Scholar
  63. 63.
    Pohl, K., Böckle, G., Linden, F.J.V.D.: Software Product Line Engineering: Foundations, Principles and Techniques. Springer, Secaucus (2005)zbMATHCrossRefGoogle Scholar
  64. 64.
    Raistrick, C., Francis, P., Wright, J.: Model Driven Architecture with Executable UML (TM). Cambridge University Press, New York (2004)Google Scholar
  65. 65.
    Ramsey, H.R., Atwood, M.E., Van Doren, J.R.: Flowcharts versus program design languages: an experimental comparison. Commun. ACM 26(6), 445–449 (1983).  https://doi.org/10.1145/358141.358149 CrossRefGoogle Scholar
  66. 66.
    Rodrigues, V., Lopes, J.C., Moreira, A.: An hybrid design solution for spacecraft simulators. In: Proceedings of the Forum at the CAiSE’08 Conference, Montpellier, France, June 18–20, 2008, pp. 29–32 (2008)Google Scholar
  67. 67.
    Rodrigues, V., Akesson, B., Florido, M., de Sousa, S.A.M., Pedroso, J.A.P., Vasconcelos, P.: Certifying execution time in multicores. Sci. Comput. Program. 111(P3), 505–534 (2015).  https://doi.org/10.1016/j.scico.2015.06.006 CrossRefGoogle Scholar
  68. 68.
    Røst, T.B., Seidl, C., Yu, I.C., Damiani, F., Johnsen, E.B., Chesta, C.: Hyvar. In: Mann, Z, Á., Stolz, V. (eds.) Advances in Service-Oriented and Cloud Computing. Springer, Cham, Communications in Computer and Information Science, vol. 824, pp. 159–163 (2018).  https://doi.org/10.1007/978-3-319-79090-9_12
  69. 69.
    Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education, London (2004)Google Scholar
  70. 70.
    Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds). Software Product Lines: Going Beyond (SPLC 2010). Springer, Lecture Notes in Computer Science, vol. 6287, pp. 77–91 (2010).  https://doi.org/10.1007/978-3-642-15579-6_6
  71. 71.
    Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujillo, S., Villela, K.: Software diversity: state of the art and perspectives. Int. J. Softw. Tools Technol. Transfer 14(5), 477–495 (2012).  https://doi.org/10.1007/s10009-012-0253-y CrossRefGoogle Scholar
  72. 72.
    Schürr, A., Selic, B. (eds.): Model driven engineering languages and systems. In: 12th International Conference, MODELS 2009, Denver, CO, USA, October 4–9, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5795. Springer, Berlin (2009).  https://doi.org/10.1007/978-3-642-04425-0
  73. 73.
    Seidl, C., Schaefer, I., Aßmann, U.: Deltaecore—a model-based delta language generation framework. In: Modellierung 2014, 19.-21. März 2014, Wien, Österreich, pp. 81–96 (2014)Google Scholar
  74. 74.
    Shneiderman, B., Mayer, R., McKay, D., Heller, P.: Experimental investigations of the utility of detailed flowcharts in programming. Commun. ACM 20(6), 373–381 (1977).  https://doi.org/10.1145/359605.359610 CrossRefGoogle Scholar
  75. 75.
    Stallman, R.M., McGrath, R.: GNU Make: A Program for Directed Compilation. Free Software Foundation, Boston (2002)Google Scholar
  76. 76.
    Team CAS (2004) Clarification of Structural Coverage Analyses of Data Coupling and Control Coupling. https://www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/archive/
  77. 77.
    Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6:1–6:45 (2014a).  https://doi.org/10.1145/2580950 CrossRefGoogle Scholar
  78. 78.
    Thüm, T., Kästner, C., Benduhn, F., Meinicke, J., Saake, G., Leich, T.: Featureide: an extensible framework for feature-oriented software development. Sci. Comput. Program. 79, 70–85 (2014b).  https://doi.org/10.1016/j.scico.2012.06.002 CrossRefGoogle Scholar
  79. 79.
    Tichy, W.F., Lukowicz, P., Prechelt, L., Heinz, E.A.: Experimental evaluation in computer science: a quantitative study. J. Syst. Softw. 28(1), 9–18 (1995).  https://doi.org/10.1016/0164-1212(94)00111-Y CrossRefGoogle Scholar
  80. 80.
    Tu, Q., Godfrey, M.W.: The build-time software architecture view. In: Proceedings IEEE International Conference on Software Maintenance. ICSM 2001, pp. 398–407 (2001).  https://doi.org/10.1109/ICSM.2001.972753
  81. 81.
    Turner, A.J.: Iterative enhancement: a practical technique for software development. IEEE Trans. Softw. Eng. 1(1), 390–396 (1975).  https://doi.org/10.1109/TSE.1975.6312870 CrossRefGoogle Scholar
  82. 82.
    Vaughan, G.V, Elliston, B., Tromey, T., Taylor, I.L., Mac Kenzie, D.: GNU Autoconf, Automake and Libtool. Expert Insight into Porting Software and Building Large Projects using GNU Autotools. New Riders, Indianapolis (2001)Google Scholar
  83. 83.
    Weiss, D.M., Basili, V.R.: Evaluating software development by analysis of changes: some data from the software engineering laboratory. IEEE Trans. Softw. Eng. SE–11(2), 157–168 (1985).  https://doi.org/10.1109/TSE.1985.232190 CrossRefGoogle Scholar
  84. 84.
    Weyuker, E.J.: Evaluating software complexity measures. IEEE Trans. Softw. Eng. 14(9), 1357–1365 (1988).  https://doi.org/10.1109/32.6178 MathSciNetCrossRefGoogle Scholar
  85. 85.
    Williams, M., Grajales, C., Kurkiewicz, D.: Assumptions of multiple regression: correcting two misconceptions. Pract. Assess. Res. Eval. 18, 1 (2013)Google Scholar
  86. 86.
    Wolverton, R.W.: The cost of developing large-scale software. IEEE Trans. Comput. C–23(6), 615–636 (1974).  https://doi.org/10.1109/T-C.1974.224002 zbMATHCrossRefGoogle Scholar
  87. 87.
    Wong, B., Czajkowski, G., Daynes, L.: Dynamically loaded classes as shared libraries: an approach to improving virtual machine scalability. In: Proceedings International Parallel and Distributed Processing Symposium (2003).  https://doi.org/10.1109/IPDPS.2003.1213123
  88. 88.
    Yourdon, E.: Techniques of Program Structure and Design, 1st edn. Prentice Hall PTR, Upper Saddle River (1986)zbMATHGoogle Scholar
  89. 89.
    Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: dynamic storage allocation. In: 12th European Symposium on Programming on Science of Computer Programming, vol. 50, no. 1, pp. 101–127 (2004).  https://doi.org/10.1016/j.scico.2004.01.003 (ESOP 2003)

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  • Vítor Rodrigues
    • 1
    Email author
  • Simone Donetti
    • 1
  • Ferruccio Damiani
    • 1
  1. 1.University of TurinTurinItaly

Personalised recommendations