Composing Families of Timed Automata

  • Guillermina CledouEmail author
  • José Proença
  • Luis Soares Barbosa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10522)


Featured Timed Automata (FTA) is a formalism that enables the verification of an entire Software Product Line (SPL), by capturing its behavior in a single model instead of product-by-product. However, it disregards compositional aspects inherent to SPL development. This paper introduces Interface FTA (IFTA), which extends FTA with variable interfaces that restrict the way automata can be composed, and with support for transitions with atomic multiple actions, simplifying the design. To support modular composition, a set of Reo connectors are modelled as IFTA. This separation of concerns increases reusability of functionality across products, and simplifies modelling, maintainability, and extension of SPLs. We show how IFTA can be easily translated into FTA and into networks of Timed Automata supported by UPPAAL. We illustrate this with a case study from the electronic government domain.


Software Product Lines Featured Timed Automata Compositionality 


  1. 1.
    de Alfaro, L., Henzinger, T.A.: Interface automata. SIGSOFT Softw. Eng. Notes 26(5), 109–120 (2001). CrossRefGoogle Scholar
  2. 2.
    Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comp. Sci. 14(3), 329–366 (2004). CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.: A compositional specification theory for component behaviours. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 148–168. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28869-2_8 CrossRefGoogle Scholar
  4. 4.
    Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. International Conference on Software Engineering, ICSE, pp. 321–330 (2011).
  5. 5.
    Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A.: Behavioural modelling and verification of real-time software product lines. In: Proceedings of the 16th International Software Product Line Conference, SPLC 2012, vol. 1. pp. 66–75. ACM, New York (2012).
  6. 6.
    David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed i/o automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, pp. 91–100. ACM, New York (2010).
  7. 7.
    Jin, X., Ma, H., Gu, Z.: Real-time component composition using hierarchical timed automata. In: Seventh International Conference on Quality Software (QSIC 2007), pp. 90–99, October 2007Google Scholar
  8. 8.
    Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71316-6_6 CrossRefGoogle Scholar
  9. 9.
    Lochau, M., Mennicke, S., Baller, H., Ribbeck, L.: Incremental model checking of delta-oriented software product lines. J. Logic Algebraic Program. 85(1, Part 2), 245–267 (2016)., Formal Methods for Software Product Line Engineering
  10. 10.
    Millo, J.-V., Ramesh, S., Krishna, S.N., Narwane, G.K.: Compositional verification of software product lines. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 109–123. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38613-8_8 CrossRefGoogle Scholar
  11. 11.
    Muschevici, R., Proença, J., Clarke, D.: Feature nets: behavioural modelling of software product lines. Softw. Syst. Model. 15(4), 1181–1206 (2016). CrossRefzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2017

Authors and Affiliations

  • Guillermina Cledou
    • 1
    • 2
    Email author
  • José Proença
    • 1
    • 2
  • Luis Soares Barbosa
    • 1
    • 2
  1. 1.HASLabINESCTECBragaPortugal
  2. 2.Universidade do MinhoBragaPortugal

Personalised recommendations