Composing Families of Timed Automata
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.
KeywordsSoftware Product Lines Featured Timed Automata Compositionality
- 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). http://dl.acm.org/citation.cfm?id=1985838
- 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). http://doi.acm.org/10.1145/2362536.2362549
- 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). http://doi.acm.org/10.1145/1755952.1755967
- 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
- 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). http://dx.doi.org/10.1016/j.jlamp.2015.09.004, Formal Methods for Software Product Line Engineering