nach oben

Erschienen in:

2024 | OriginalPaper | Buchkapitel

Model-Based Testing of Asynchronously Communicating Distributed Controllers

verfasst von : Bence Graics, Milán Mondok, Vince Molnár, István Majzik

Erschienen in: Formal Aspects of Component Software

Verlag: Springer Nature Switzerland

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Programmable controllers are gaining prevalence even in distributed safety-critical infrastructures, e.g., in the railway and aerospace industries. Such systems are generally integrated using multiple loosely-coupled reactive components and must satisfy various critical requirements. Thus, their systematic testing is an essential task, which can be encumbered by their distributed characteristics. This paper presents a model-based integration test generation approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then transformed (via a symbolic transition systems formalism – XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta and Spin in an automated way. The model checkers are utilized for test generation based on multiple coverage criteria. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Symbolic Path-Guided Test Cases for Models with Data and Time

Nächstes Kapitel A Mechanized Semantics for Component-Based Systems in the HAMR AADL Runtime

Nur mit Berechtigung zugänglich

More information about the framework (e.g., preprints) and the source code can be found at http://gamma.inf.mit.bme.hu/ and https://github.com/ftsrg/gamma/.

Model descriptions and measurement results can be found at https://github.com/ftsrg/gamma/tree/v2.9.0/examples/, as well as [16] (RSS) and [14] (RIS).

Ambrosi, G., Bartocci, S., Basara, L., et al.: The electronics of the high-energy particle detector on board the CSES-01 satellite. Nucl. Instrum. Methods Phys. Res. Sect. A Accel. Spectrom. Detect. Assoc. Equip. 1013, 165639 (2021). https://doi.org/10.1016/j.nima.2021.165639

Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305–343. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_11CrossRef

Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011). https://doi.org/10.1109/MS.2011.27CrossRef

Behrmann, G., et al.: UPPAAL 4.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006, pp. 125–126. IEEE Computer Society, USA (2006). https://doi.org/10.1109/QEST.2006.59

Boulanger, J.L.: CENELEC 50128 and IEC 62279 Standards. Wiley, Hoboken (2015)CrossRef

DeLine, R., Leino, K.R.M.: BoogiePL: a typed procedural language for checking object-oriented programs. Technical report. MSR-TR-2005-70, Microsoft Research (2005)

Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986). https://doi.org/10.1145/4904.4999

Enoiu, E.P., Čaušević, A., Ostrand, T.J., Weyuker, E.J., Sundmark, D., Pettersson, P.: Automated test generation using model checking: an industrial evaluation. Int. J. Softw. Tools Technol. Transfer 18(3), 335–353 (2016). https://doi.org/10.1007/s10009-014-0355-9CrossRef

Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H.: Systematic evaluation and usability analysis of formal methods tools for railway signaling system design. IEEE Trans. Software Eng. 48(11), 4675–4691 (2022). https://doi.org/10.1109/TSE.2021.3124677CrossRef

10.

Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verification Reliab. 19(3), 215–261 (2009). https://doi.org/10.1002/stvr.402CrossRef

11.

Golarits, Z., Sinka, D., Jávor, A.: Proris - a new interlocking system for regional and moderate-traffic lines. Signal+DRAHT-Signal. Datacommun. (114), 28–36 (2022)

12.

Graics, B.: Documentation of the Gamma Statechart Composition Framework v0.9. Technical report, Budapest University of Technology and Economics, Department of Measurement and Information Systems (2016). https://tinyurl.com/yeywrkd6

13.

Graics, B.: Mixed-semantic composition and verification of reactive components. Technical report, Budapest University of Technology and Economics, Department of Measurement and Information Systems (2023). https://tinyurl.com/2p9dae58

14.

Graics, B., Majzik, I.: Integration test generation and formal verification for distributed controllers. In: Renczes, B. (ed.) Proceedings of the 30th Ph.D. Minisymposium. Budapest Univesity of Technology and Economics, Department of Measurement and Information Systems (2023). https://doi.org/10.3311/minisy2023-001

15.

Graics, B., Molnár, V.: Formal compositional semantics for Yakindu statecharts. In: Pataki, B. (ed.) Proceedings of the 24th PhD Mini-Symposium, pp. 22–25. Budapest University of Technology and Economics, Department of Measurement and Information Systems, Budapest, Hungary (2017)

16.

Graics, B., Molnár, V., Majzik, I.: Integration test generation for state-based components in the Gamma framework. Preprint (2022). https://tinyurl.com/4dhubca4

17.

Graics, B., Molnár, V., Vörös, A., Majzik, I., Varró, D.: Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw. Syst. Model. 19(6), 1483–1517 (2020). https://doi.org/10.1007/s10270-020-00806-5CrossRef

18.

Hajdu, Á., Tóth, T., Vörös, A., Majzik, I.: A configurable CEGAR framework with interpolation-based refinements. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 158–174. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39570-8_11CrossRef

19.

Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987). https://doi.org/10.1016/0167-6423(87)90035-9MathSciNetCrossRef

20.

Hartman, A., Nagin, K.: The AGEDIS tools for model based testing. ACM Sigsoft Softw. Eng. Notes 29 (2004). https://doi.org/10.1145/1007512.1007529

21.

Heineman, G.T., Councill, W.T.: Component-based software engineering. Putting the Pieces Together. Addison Wesley (2001). https://doi.org/10.5555/379381

22.

Henzinger, T.A., Majumdar, R.: A classification of symbolic transition systems. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 13–34. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46541-3_2CrossRef

23.

Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Harlow (2011)

24.

Holzmann, G.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997). https://doi.org/10.1109/32.588521CrossRef

25.

Huang, L.: The past, present and future of railway interlocking system. In: 2020 IEEE 5th International Conference on Intelligent Transportation Engineering (ICITE), pp. 170–174 (2020). https://doi.org/10.1109/ICITE50838.2020.9231438

26.

Jéron, T., Morel, P.: Test generation derived from model-checking. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 108–122. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_12CrossRef

27.

Ke, X., Sierszecki, K., Angelov, C.: COMDES-II: a component-based framework for generative development of distributed real-time control systems. In: 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), pp. 199–208 (2007). https://doi.org/10.1109/RTCSA.2007.29

28.

Legeard, B., Bouzy, A.: Smartesting CertifyIt: model-based testing for enterprise IT. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, pp. 391–397 (2013). https://doi.org/10.1109/ICST.2013.55

29.

Li, J., Post, M., Wright, T., Lee, R.: Design of attitude control systems for CubeSat-class nanosatellite. J. Control Sci. Eng. 2013 (2013). https://doi.org/10.1155/2013/657182

30.

Li, W., Le Gall, F., Spaseski, N.: A survey on model-based testing tools for test case generation. In: Itsykson, V., Scedrov, A., Zakharov, V. (eds.) TMPA 2017. CCIS, vol. 779, pp. 77–89. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-71734-0_7CrossRef

31.

Lukács, G., Bartha, T.: Formal modeling and verification of the functionality of electronic urban railway control systems through a case study. Urban Rail Transit. 8 (2022). https://doi.org/10.1007/s40864-022-00177-8

32.

Martinez, S., Pereira, D.I.D.A., Bon, P., Collart-Dutilleul, S., Perin, M.: Towards safe and secure computer based railway interlocking systems. Int. J. Transp. Dev. Integr. 4(3), 218–229 (2020)CrossRef

33.

Mohalik, S., Gadkari, A.A., Yeolekar, A., Shashidhar, K., Ramesh, S.: Automatic test case generation from Simulink/Stateflow models using model checking. Softw. Test. Verif. Reliab. 24, 155–180 (2014). https://doi.org/10.1002/stvr.1489CrossRef

34.

Molnár, V., Graics, B., Vörös, A., Majzik, I., Varró, D.: The Gamma Statechart Composition Framework. In: 40th International Conference on Software Engineering (ICSE), Gothenburg, Sweden, pp. 113–116. ACM (2018). https://doi.org/10.1145/3183440.3183489

35.

Mondok, M.: Efficient abstraction-based model checking using domain-specific information. Technical report, Budapest University of Technology and Economics, Department of Measurement and Information Systems (2021). https://tinyurl.com/yh4b8w98

36.

Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217CrossRef

37.

Radnai, B.: Integration of SCXML state machines to the Gamma framework. Technical report, Budapest University of Technology and Economics, Department of Measurement and Information Systems (2022). https://tinyurl.com/4mmtsw7v

38.

39.

Sztipanovits, J., Bapty, T., Neema, S., Howard, L., Jackson, E.: OpenMETA: a model- and component-based design tool chain for cyber-physical systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) ETAPS 2014. LNCS, vol. 8415, pp. 235–248. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54848-2_16CrossRef

40.

Tóth, T., Hajdu, A., Vörös, A., Micskei, Z., Majzik, I.: Theta: a framework for abstraction refinement-based model checking. In: Stewart, D., Weissenbacher, G. (eds.) Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, pp. 176–179 (2017). https://doi.org/10.23919/FMCAD.2017.8102257

41.

Zhou, J., Hu, Q., Friswell, M.I.: Decentralized finite time attitude synchronization control of satellite formation flying. J. Guid. Control. Dyn. 36(1), 185–195 (2013). https://doi.org/10.2514/1.56740CrossRef

Titel: Model-Based Testing of Asynchronously Communicating Distributed Controllers
verfasst von: Bence Graics
Milán Mondok
Vince Molnár
István Majzik
Verlag: Springer Nature Switzerland
Buch: Formal Aspects of Component Software
Print ISBN: 978-3-031-52182-9

Electronic ISBN: 978-3-031-52183-6

Copyright-Jahr: 2024
DOI: https://doi.org/10.1007/978-3-031-52183-6_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner