Top

International Journal on Software Tools for Technology Transfer

Published in:

21-09-2019 | Foundations for Mastering Change

Verification and abstraction of real-time variability-intensive systems

Authors: Maxime Cordy, Axel Legay

Published in: International Journal on Software Tools for Technology Transfer | Issue 6/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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.

previous article Sampling strategies for product lines with unbounded parametric real-time constraints

next article Configuration of inter-process communication with probabilistic model checking

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

This is without loss of generality, since variability and time in FTA can be considered orthogonally.

This is akin to the restriction operator defined in [18] for FTS.

Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a framework for abstraction- and interpolation-based software verification. In: CAV, pp. 672–678 (2012)

Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)MathSciNetCrossRef

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)

Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

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)CrossRef

Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL in 1995. In: TACAS’96, pp. 431–434. Springer (1996)

Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets, pp. 87–124 (2003)CrossRef

Beyer, D.: Second competition on software verification (summary of SV-COMP 2013). In: TACAS ’13, pp. 594–609 (2013)CrossRef

Beyer, D., Keremoglu, M.E.: Cpachecker: a tool for configurable software verification. In: CAV ’11, pp. 184–190 (2011)CrossRef

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)CrossRef

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)CrossRef

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)CrossRef

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)

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)

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)CrossRef

16.

Clements, P.C., Northrop, L.: Software Product Lines: Practices and Patterns. SEI Series in Software Engineering. Addison-Wesley, Boston (2001)

17.

Comtet, L.: Sperner Systems (§7.2). Springer, Berlin (1974)

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)

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)

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)

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)

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)

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)

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)CrossRef

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)CrossRef

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)

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)

28.

Falke, S., Merz, F., Sinz, C.: The bounded model checker LLBMC. In: ASE ’13, pp. 706–709 (2013)

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)CrossRef

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)

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). https://doi.org/10.1145/3106195.3106204

32.

Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Handling unbounded loops with ESBMC 1.20 (competition contribution). In: TACAS, pp. 619–622 (2013)

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)CrossRef

34.

Post, H., Sinz, C.: Configuration lifting: verification meets software configuration. In: ASE’08, pp. 347–350. IEEE CS (2008)

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)MathSciNetCrossRef

36.

Wang, F.: Efficient model-checking of timed automata with clock-restriction diagram. In: APLAS, pp. 207–224 (2001)

37.

Yi, W.: Real-time behaviour of asynchronous agents. In: Proceedings of CONCUR ’90, pp. 502–520. Springer, New York (1990)

Title: Verification and abstraction of real-time variability-intensive systems
Authors: Maxime Cordy
Axel Legay
Publication date: 21-09-2019
Publisher: Springer Berlin Heidelberg
Published in: International Journal on Software Tools for Technology Transfer / Issue 6/2019
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-019-00537-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 6/2019

Quantitative variability modelling and analysis

Applying supervisory control synthesis to priced featured automata and energy problems

Configuration of inter-process communication with probabilistic model checking

Sampling strategies for product lines with unbounded parametric real-time constraints

Automatic refactoring of delta-oriented SPLs to remove-free form and replace-free form

Quantitative properties of featured automata

Premium Partner