Model Checking Families of Real Time Specifications
Model checking [MCF1, MCF2, MCF3] is a method to verify if a model of the system under verification satisfies its specification. Many languages to write the model exist and range from finite-state to infinite-state machines, from discrete-time to timed or hybrid systems, from non-deterministic automata to stochastic models, from synchronous to asynchronous communicating programs. Given a formal semantics of the input language, model checking can also be applied to models defined for other purposes (architectural description or simulation) or directly to software or hardware source code.
Many software systems are highly configurable with many variations, developed as a software product line (SPL) where variability is realised in terms of features that conceptualise pieces of system functionality that are relevant to different stakeholders [MCF4]. Many formal models of SPL exist, including over feature transitions [MCF5] and modal transition systems [MCF6], possibly with variability constraints [MCF7]. Other models have been also equipped with variability, including I/O automata [MCF8], Petri nets [MCF9], contract automata [MCF10], and timed-automata [MCF11].
A challenge of formalising SPLs is how to link the instantiated software products with the variability models. The most common approaches ae annotative variability modelling [MCF12], where systems are enriched with special annotations that allow the behaviour to be updated based on configurations, and delta variability modelling [MCF13], where variations are described as a set of transformations over a core product.
This method explores variability of the formal specification of a system and its requirements, and not the system implementation. Concrete instances of this family of specifications are either modelling variations of the implementation, or variations of how the implementation is abstracted in the formal specification. We consider specifications of real-time systems for model checking tools such as UPPAAL [MCF14] or Real-Time Maude [MCF15], which include intervals of expected execution times of individual components and the frequency of events. These are particularly common in critical embedded systems, where the complexity of the model can quickly grow when including too many details. Subdividing a complex model into smaller variations, each fine-tuned to a different group of requirements, increases the usability and applicability of a single real-time specification.
- Can check for specific properties without verifying the full system
- Exhaustively explores the state space
- Well-established verification tools and techniques with industrial applications
- The computation of the reachable states or of the abstraction may be too expensive and the techniques do not scale to complex models.
- Abstraction techniques may be too coarse and may be not effective in proving some properties.
[MCF1] Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model checking. MIT Press 1999, ISBN 978-0-262-03270-4
[MCF2] Christel Baier, Joost-Pieter Katoen: Principles of model checking. MIT Press 2008, ISBN 978-0-262-02649-9, pp. I-XVII, 1-975
[MCF3] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem: Handbook of Model Checking. Springer 2018, ISBN 978-3-319-10574-1
[MCF4] Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer (2013).
[MCF5] 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. IEEE Trans. Softw. Eng. 39(8), 1069-1089 (2013).
[MCF6] Fantechi, A., Gnesi, S.: A Behavioural Model for Product Families. In: Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE). pp. 521-524. ACM (2007).
[MCF7] 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. Meth. Program. 85(2), 287-315 (2016).
[MCF8] Lauenroth, K., Pohl, K., Töhning, S.: Model Checking of Domain Artifacts in Product Line Engineering. In: Proceedings of the 24th International Conference on Automated Software Engineering (ASE). pp. 269-280. IEEE (2009).
[MCF9] Muschevici, R., Proença, J., Clarke, D.: Feature Nets: behavioural modelling of software product lines. Softw. Sys. Model. 15(4), 1181-1206 (2016).
[MCF10] Basile, D., ter Beek, M.H., Degano, P., Legay, A., Ferrari, G.L., Gnesi, S., Di Giandomenico, F.: Controller synthesis of service contracts with variability. Sci. Comput. Program. 187 (2020).
[MCF11] Cledou, G., Proença, J., Barbosa, L.: Composing families of timed automata. In: Dastani, M. and Sirjani, M. (eds.) FSEN. LNCS, vol. 10522, pp. 51-66. Springer (2017).
[MCF12] Völter, M., Groher, I.: Product Line Implementation using Aspect-Oriented and Model-Driven Software Development. In: SPLC (2007).
[MCF13] Dave Clarke, Michiel Helvensteijn, Ina Schaefer: Abstract delta modelling. Math. Struct. Comput. Sci. 25(3): 482-527 (2015).
[MCF14] Gerd Behrmann, Alexandre David, and Kim G. Larsen: A Tutorial on UPPAAL. LNCS 3185, pp 200-236. Springer-Verlag (2004).
[MCF15] Peter Csaba Ölveczky, José Meseguer: Semantics and pragmatics of Real-Time Maude. High. Order Symb. Comput. 20(1-2): 161-196 (2007).