Verification and abstraction of real-time variability-intensive systems

  • Maxime CordyEmail author
  • Axel Legay
Foundations for Mastering Change Quantitative Variability Modelling and Analysis


Featured timed automaton (FTA) is a concise formalism to model the real-time behaviour of variability-intensive systems. FTA extends the timed automaton by allowing optional transitions and clock constraints that are relevant only for a subset of the system variants. Then, one can verify a variant individually by deriving the corresponding TA from the FTA and using established tools like UPPAAL or apply family-based algorithms to verify all variants at once. These latter algorithms consist of computing the reachability relation in FTA as an antichain. Yet, they suffer from a three-source complexity: the number of states, the number of time clocks and the number of variants. This motivates the design of abstraction refinement heuristics to reduce verification effort. In this paper, we present the syntax and semantics of FTA, efficient algorithms to compute their reachability relations, and discuss how abstraction methods can be applied.


Model checking Variability Real time Abstraction 



  1. 1.
    Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a framework for abstraction- and interpolation-based software verification. In: CAV, pp. 672–678 (2012)Google Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Apel, S., Speidel, H., Wendler, P., von Rhein, A., Beyer, D.: Feature-interaction detection using feature-aware verification. In: ASE’11, pp. 372–375. IEEE (2011)Google Scholar
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  5. 5.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in uppaal. In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 174–188. Springer, Berlin (2001)CrossRefGoogle Scholar
  6. 6.
    Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL in 1995. In: TACAS’96, pp. 431–434. Springer (1996)Google Scholar
  7. 7.
    Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets, pp. 87–124 (2003)CrossRefGoogle Scholar
  8. 8.
    Beyer, D.: Second competition on software verification (summary of SV-COMP 2013). In: TACAS ’13, pp. 594–609 (2013)CrossRefGoogle Scholar
  9. 9.
    Beyer, D., Keremoglu, M.E.: Cpachecker: a tool for configurable software verification. In: CAV ’11, pp. 184–190 (2011)CrossRefGoogle Scholar
  10. 10.
    Chechik, M., Devereux, B., Easterbrook, S.M., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371–408 (2003)CrossRefGoogle Scholar
  11. 11.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E., Sistla, A. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 1855, pp. 154–169. Springer, Berlin (2000)CrossRefGoogle Scholar
  12. 12.
    Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. Trans. Softw. Eng. 39, 1069–1089 (2013)CrossRefGoogle Scholar
  13. 13.
    Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: ICSE’11, pp. 321–330. ACM (2011)Google Scholar
  14. 14.
    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, pp. 335–344. ACM (2010)Google Scholar
  15. 15.
    Cledou, G., Proença, J., Barbosa, L.S.: Composing families of timed automata. In: Dastani, M., Sirjani, M. (eds.) Fundamentals of Software Engineering, pp. 51–66. Springer, Cham (2017)CrossRefGoogle Scholar
  16. 16.
    Clements, P.C., Northrop, L.: Software Product Lines: Practices and Patterns. SEI Series in Software Engineering. Addison-Wesley, Boston (2001)Google Scholar
  17. 17.
    Comtet, L.: Sperner Systems (§7.2). Springer, Berlin (1974)Google Scholar
  18. 18.
    Cordy, M., Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Managing evolution in software product lines: a model-checking perspective. In: VaMoS’12, pp. 183–191. ACM (2012)Google Scholar
  19. 19.
    Cordy, M., Classen, A., Perrouin, G., Heymans, P., Schobbens, P.Y., Legay, A.: Simulation-based abstractions for software product-line model checking. In: ICSE’12, pp. 672–682. IEEE (2012)Google Scholar
  20. 20.
    Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: FSE’14, pp. 190–201. ACM (2014)Google Scholar
  21. 21.
    Cordy, M., Heymans, P., Schobbens, P.Y., Legay, A.: Behavioural modelling and verification of real-time software product lines. In: SPLC’12. ACM (2012)Google Scholar
  22. 22.
    Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A.: Beyond Boolean product-line model checking: dealing with feature attributes and multi-features. In: ICSE’13, pp. 472–481. IEEE (2013)Google Scholar
  23. 23.
    Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A.: Provelines: a product-line of verifiers for software product lines. In: SPLC’13, pp. 141–146. ACM (2013)Google Scholar
  24. 24.
    Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.F., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems, pp. 114–129. Springer, Berlin (2007)CrossRefGoogle Scholar
  25. 25.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, pp. 197–212. Springer, New York (1990)CrossRefGoogle Scholar
  26. 26.
    Dimovski, A.S., Wasowski, A.: From transition systems to variability models and from lifted model checking back to UPPAAL. In: Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, pp. 249–268 (2017)Google Scholar
  27. 27.
    Ehlers, R., Fass, D., Gerke, M., Peter, H.J.: Fully symbolic timed model checking using constraint matrix diagrams. In: Proceedings of the 2010 31st IEEE Real-Time Systems Symposium, RTSS ’10, pp. 360–371. IEEE Computer Society, Washington (2010)Google Scholar
  28. 28.
    Falke, S., Merz, F., Sinz, C.: The bounded model checker LLBMC. In: ASE ’13, pp. 706–709 (2013)Google Scholar
  29. 29.
    Kramer, J., Magee, J., Sloman, M., Lister, A.: CONIC: an integrated approach to distributed computer control systems. IEE Proc. E Comput. Digit. Tech. 130(1), 1–10 (1983)CrossRefGoogle Scholar
  30. 30.
    Lazreg, S., Collet, P., Mosser, S.: Assessing the functional feasibility of variability-intensive data flow-oriented systems. In: 33rd Symposium on Applied Computing (2018)Google Scholar
  31. 31.
    Luthmann, L., Stephan, A., Bürdek, J., Lochau, M.: Modeling and testing product lines with unbounded parametric real-time constraints. In: Proceedings of the 21st International Systems and Software Product Line Conference: Volume A, SPLC ’17, pp. 104–113. ACM, New York (2017).
  32. 32.
    Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Handling unbounded loops with ESBMC 1.20 (competition contribution). In: TACAS, pp. 619–622 (2013)Google Scholar
  33. 33.
    Nagaoka, T., Okano, K., Kusumoto, S.: An abstraction refinement technique for timed automata based on counterexample-guided abstraction refinement loop. IEICE Trans. Inf. Syst. 93–D, 994–1005 (2010)CrossRefGoogle Scholar
  34. 34.
    Post, H., Sinz, C.: Configuration lifting: verification meets software configuration. In: ASE’08, pp. 347–350. IEEE CS (2008)Google Scholar
  35. 35.
    ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Methods Program. 85(2), 287–315 (2016)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Wang, F.: Efficient model-checking of timed automata with clock-restriction diagram. In: APLAS, pp. 207–224 (2001)Google Scholar
  37. 37.
    Yi, W.: Real-time behaviour of asynchronous agents. In: Proceedings of CONCUR ’90, pp. 502–520. Springer, New York (1990)Google Scholar

Copyright information

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

Authors and Affiliations

  1. 1.Interdisciplinary Centre on Security, Reliabiliy and TrustUniversity of LuxembourgLuxembourgLuxembourg
  2. 2.Université Catholique de LouvainLouvain-La-NeuveBelgium

Personalised recommendations