Abstract
This paper introduces a technique for incremental and compositional model checking that allows efficient reuse of model-checking results associated with the features in a product line. As the use of product lines has increased, so has the need to verify the models used to construct the products in the product line. However, this effort is currently hampered by the difficulty of composing model-checking results for the features in a way that allows reuse for subsequent products. The contributions of this paper are to remove restrictions on how the features can be sequentially composed, to describe how to generate obligations such that all sequentially composed systems can be verified, and to show how to compositionally model check the product in the product line by reusing the variation-point obligations. The paper develops the technique and its implementation in the context of a medical-device product line.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507–535 (1995). http://doi.acm.org/10.1145/203095.201069
Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. Theor. Comput. Sci. 354(2), 211–229 (2006). doi:10.1016/j.tcs.2005.11.016
Batory, D., Benavides, D., Ruiz-Cortes, A.: Automated analysis of feature models: challenges ahead. Commun. ACM 49(12), 45–47 (2006). http://doi.acm.org/10.1145/1183236.1183264
Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: Proc. COMPOS, pp. 81–102. Springer, Berlin (1998)
Blundell, C., Fisler, K., Krishnamurthi, S., Hentenryck, P.V.: A constraint-based approach to open feature verification. Tech. Rep. CS-03-07, Department of Computer Science, Brown University (2003)
Blundell, C., Fisler, K., Krishnamurthi, S., Hentenryck, P.V.: Parameterized interfaces for open system verification of product lines. In: ASE ’04: Proceedings of the 19th IEEE International Conference on Automated Software Engineering, pp. 258–267. IEEE Comput. Soc., Washington (2004). 10.1109/ASE.2004.53
Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: CAV ’99: Proceedings of the 11th International Conference on Computer Aided Verification, pp. 274–287. Springer, London (1999)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)
Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: LICS, pp. 353–362 (1989)
Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: ICSE ’10: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, pp. 335–344. ACM, New York (2010). http://doi.acm.org/10.1145/1806799.1806850
Cleaveland, R.: Tableau-based model checking in the propositional mu-calculus. Acta Inform. 27(8), 725–748 (1990). citeseer.ist.psu.edu/61863.html
Ellenbogen, K.A., Wood, M.A.: Cardiac Pacing and ICDs, 4th edn. Blackwell, Oxford (2005)
Fantechi, A., Gnesi, S.: A behavioural model for product families. In: ESEC-FSE ’07: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 521–524. ACM, New York (2007). http://doi.acm.org/10.1145/1287624.1287700
Fischbein, D., Uchitel, S., Braberman, V.: A foundation for behavioural conformance in software product line architectures. In: ROSATEA ’06: Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, pp. 39–48. ACM, New York (2006). http://doi.acm.org/10.1145/1147249.1147254
Fisler, K., Krishnamurthi, S.: Modular verification of collaboration-based software designs. In: ESEC/FSE-9: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 152–163. ACM, New York (2001). http://doi.acm.org/10.1145/503209.503231
Fisler, K., Krishnamurthi, S.: Modular verification of feature-oriented software models. Tech. Rep. WPI-CS-TR-02-28, Department of Computer Science, WPI (2002). http://web.cs.wpi.edu/kfisler/Pubs/tr-02-28.pdf
Gheorghiu, M., Giannakopoulou, D., Pasareanu, C.S.: Refining interface alphabets for compositional verification. In: TACAS, pp. 292–307 (2007)
Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption generation for software component verification. In: ASE ’02: Proceedings of the 17th IEEE International Conference on Automated Software Engineering, pp. 3–12. IEEE Comput. Soc., Washington (2002)
Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: FMOODS ’08: Proceedings of the 10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 113–131. Springer, Berlin (2008). 10.1007/978-3-540-68863-1_8
Hall, R.: Feature interactions in electronic mail. In: Feature Interactions in Telecommunications Systems, pp. 67–82. IOS Press, Amsterdam (2000)
Havelund, K., Lowry, M.R., Penix, J.: Formal analysis of a space-craft controller using SPIN. Softw. Eng. 27(8), 1000–9999 (2001). citeseer.ist.psu.edu/havelund98formal.html
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2004). http://pubs.doc.ic.ac.uk/logic-computer-science-second/
Jacobson, I., Griss, M., Jonsson, P.: Software Reuse: Architecture, Process and Organization for Business Success. Addison-Wesley, Reading (1997)
Kaivola, R.: Formal verification of Pentium 4 components with symbolic simulation and inductive invariants. In: Etessami, K., Rajamani, S.K. (eds.) CAV. Lecture Notes in Computer Science, vol. 3576, pp. 170–184. Springer, Berlin (2005)
Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-oriented domain analysis (foda) feasibility study. Tech. rep., Carnegie-Mellon University Software Engineering Institute (1990)
Kang, K.C., Lee, J., Donohoe, P.: Feature-oriented product line engineering. IEEE Softw. 19(4), 58–65 (2002). http://doi.ieeecomputersociety.org/10.1109/MS.2002.1020288
Kishi, T., Noda, N., Katayama, T.: Design verification for product line development. In: SPLC, pp. 150–161 (2005)
Krishnamurthi, S., Fisler, K.: Foundations of incremental aspect model-checking. ACM Trans. Softw. Eng. Methodol. 16(2), 7 (2007). http://doi.acm.org/10.1145/1217295.1217296
Larsen, K.G., Nyman, U., Wasowski, A.: Modal i/o automata for interface and product line theories. In: ESOP’07: Proceedings of the 16th European Conference on Programming, pp. 64–79. Springer, Berlin (2007)
Lauenroth, K., Pohl, K.: Towards automated consistency checks of product line requirements specifications. In: ASE ’07: Proceedings of the Twenty-Second IEEE/ACM International Conference on Automated Software Engineering, pp. 373–376. ACM, New York (2007). http://doi.acm.org/10.1145/1321631.1321687
Li, H., Krishnamurthi, S., Fisler, K.: Verifying cross-cutting features as open systems. In: SIGSOFT ’02/FSE-10: Proceedings of the Tenth ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 89–98. ACM, New York (2002a). http://doi.acm.org/10.1145/587051.587066
Li, H.C., Krishnamurthi, S., Fisler, K.: Interfaces for modular feature verification. In: ASE ’02: Proceedings of the 17th IEEE International Conference on Automated Software Engineering, p. 195. IEEE Comput. Soc., Washington (2002b)
Li, H.C., Krishnamurthi, S., Fisler, K.: Modular verification of open features using three-valued model checking. Autom. Softw. Eng. 12(3), 349–382 (2005). 10.1007/s10515-005-2643-9
Littlewood, B., Strigini, L.: Validation of ultrahigh dependability for software-based systems. Commun. ACM 36(11), 69–80 (1993). http://doi.acm.org/10.1145/163359.163373
Liu, J.: Research prototype model checker for compositional model checking of software product lines (2010). http://www.cs.iastate.edu/~janetlj/PrototypeModelChecker/
Liu, J., Dehlinger, J., Lutz, R.: Safety analysis of software product lines using state-based modeling. J. Syst. Softw. 80(11), 1879–1892 (2007a). 10.1016/j.jss.2007.01.047
Liu, J., Dehlinger, J., Sun, H., Lutz, R.: State-based modeling to support the evolution and maintenance of safety-critical software product lines. In: ECBS ’07: Proceedings of the Fourteenth Annual IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, pp. 596–608. IEEE Comput. Soc., Washington (2007b). 10.1109/ECBS.2007.66
Liu, J., Hauptman, M., Lutz, R., Geppert, B., Rossler, F.: A tool-supported technique for specification & management of model-checking properties for software product lines. Tech. Rep. 08-05, Department of Computer Science, Iowa State University (2008). http://archives.cs.iastate.edu
Nejati, S., Sabetzadeh, M., Chechik, M., Uchitel, S., Zave, P.: Towards compositional synthesis of evolving systems. In: International Symposium on Foundations of Software Engineering (2008). http://publicaciones.dc.uba.ar/Publications/2008/NSCUZ08
Ossher, H., Tarr, P.: Multi-dimensional separation of concerns and the hyperspace approach. In: Proceedings of the Symposium on Software Architectures and Component Technology: The State of the Art in Software Development. Kluwer Academic, Norwell (2000). citeseer.ist.psu.edu/ossher00multidimensional.html
Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering: Foundations, Principles and Techniques. Springer, New York (2005)
Queille, J., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Proceedings of the International Symposium in Programming (1982)
Szyperski, C.: Component Software: Beyond Object-Oriented Programming. ACM Press/Addison-Wesley, New York (1998)
Thang, N.T.: Incremental verification of consistency in feature-oriented software. PhD Thesis, Japan Advanced Institute of Science and Technology (2005)
Wang, X.: A modular model checking algorithm for cyclic feature compositions. Master’s Thesis, Worcester Polytechnic Institute (2005)
Webber, D.L., Gomaa, H.: Modeling variability in software product lines with the variation point model. Sci. Comput. Program. 53(3), 305–331 (2004). 10.1016/j.scico.2003.04.004
Weiss, D.M., Lai, R.: Software Product Line Engineering: A Family-Based Software Development Process. Addison-Wesley, Reading (1999)
Xie, F., Browne, J.C.: Verified systems by composition from verified components. SIGSOFT Softw. Eng. Notes 28(5), 277–286 (2003). http://doi.acm.org/10.1145/949952.940109
Zave, P.: Feature interactions and formal specifications in telecommunications. Computer 26(8), 20–29 (1993). 10.1109/2.223539
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Liu, J., Basu, S. & Lutz, R.R. Compositional model checking of software product lines using variation point obligations. Autom Softw Eng 18, 39–76 (2011). https://doi.org/10.1007/s10515-010-0075-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10515-010-0075-7