Skip to main content
Erschienen in: International Journal on Software Tools for Technology Transfer 6/2014

01.11.2014 | FMRCS

Towards Model-Driven V&V assessment of railway control systems

verfasst von: Stefano Marrone, Francesco Flammini, Nicola Mazzocca, Roberto Nardone, Valeria Vittorini

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2014

Einloggen

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

search-config
loading …

Abstract

Verification and Validation (V&V) activities aiming at certifying railway controllers are among the most critical and time-consuming in system development life cycle. As such, they would greatly benefit from novel approaches enabling both automation and traceability for assessment purposes. While several formal and Model-Based approaches have been proposed in the scientific literature, some of which are successfully employed in industrial settings, we are still far from an integrated and unified methodology which allows guiding design choices, minimizing the chances of failures/non-compliances, and considerably reducing the overall assessment effort. To address these issues, this paper describes a Model-Driven Engineering approach which is very promising to tackle the aforementioned challenges. In fact, the usage of appropriate Unified Modeling Language profiles featuring system analysis and test case specification capabilities, together with tool chains for model transformations and analysis, seems a viable way to allow end-users to concentrate on high-level holistic models and specification of non-functional requirements (i.e., dependability) and support the automation of the V&V process. We show, through a case study belonging to the railway signalling domain, how the approach is effective in supporting activities like system testing and availability evaluation.

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!

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!

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!

Fußnoten
1
Model checking is a technique for verifying or falsifying properties of a system. Test case generation may be obtained by using the ability of a model checker to construct counterexamples to violated properties. A counterexample defines the sequence of steps which are interpreted as a test case.
 
3
The MA is built according to the information about train position and speed each EVC periodically sends to RBC (Position Report) via GSM-R network.
 
Literatur
4.
5.
Zurück zum Zitat Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley and Sons Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley and Sons
6.
Zurück zum Zitat Asztalos, M., Lengyel, L., Levendovszky, T.: Towards automated, formal verification of model transformations. In Proc. of ICST ’10, pages 15–24, Washington, DC, USA. IEEE Computer Society (2010) Asztalos, M., Lengyel, L., Levendovszky, T.: Towards automated, formal verification of model transformations. In Proc. of ICST ’10, pages 15–24, Washington, DC, USA. IEEE Computer Society (2010)
7.
Zurück zum Zitat Baarir, S., Beccuti, M., Cerotti, D., De Pierro, M., Donatelli, S., Franceschinis, G.: The greatspn tool: Recent enhancements. SIGMETRICS Perform. Eval. Rev. 36(4), 4–9 (2009)CrossRef Baarir, S., Beccuti, M., Cerotti, D., De Pierro, M., Donatelli, S., Franceschinis, G.: The greatspn tool: Recent enhancements. SIGMETRICS Perform. Eval. Rev. 36(4), 4–9 (2009)CrossRef
8.
Zurück zum Zitat Baker, P., Dai, Z.R., Grabowski, J., Haugen, Ø., Schieferdecker, I., Williams, C.: Model-Driven Testing: Using the UML Testing Profile. Springer-Verlag New York Inc, Secaucus, NJ, USA (2007) Baker, P., Dai, Z.R., Grabowski, J., Haugen, Ø., Schieferdecker, I., Williams, C.: Model-Driven Testing: Using the UML Testing Profile. Springer-Verlag New York Inc, Secaucus, NJ, USA (2007)
9.
Zurück zum Zitat Behm, Patrick, Benoit, Paul, Faivre, Alain, Meynadier, Jean-Marc: Météor: A successful application of b in a large project. In JeannetteM. Wing, Jim Woodcock, and Jim Davies, editors, FM99 Formal Methods, volume 1708 of LNCS, pages 369–387. Springer, Berlin Heidelberg (1999) Behm, Patrick, Benoit, Paul, Faivre, Alain, Meynadier, Jean-Marc: Météor: A successful application of b in a large project. In JeannetteM. Wing, Jim Woodcock, and Jim Davies, editors, FM99 Formal Methods, volume 1708 of LNCS, pages 369–387. Springer, Berlin Heidelberg (1999)
10.
Zurück zum Zitat Bernardi, S., Flammini, F., Marrone, S., Mazzocca, N., Merseguer, J., Nardone, R., Vittorini, V.: Enabling the usage of UML in the verification of railway systems: The DAM-rail approach. Reliability Engineering and System Safety 120, 112–126 (2013)CrossRef Bernardi, S., Flammini, F., Marrone, S., Mazzocca, N., Merseguer, J., Nardone, R., Vittorini, V.: Enabling the usage of UML in the verification of railway systems: The DAM-rail approach. Reliability Engineering and System Safety 120, 112–126 (2013)CrossRef
11.
Zurück zum Zitat Bernardi, S., Flammini, F., Marrone, S., Merseguer, J., Papa, C., Vittorini, V.: Model-driven availability evaluation of railway control systems. In Proc. of the Int. Conference SAFECOMP’11, pages 15–28 (2011) Bernardi, S., Flammini, F., Marrone, S., Merseguer, J., Papa, C., Vittorini, V.: Model-driven availability evaluation of railway control systems. In Proc. of the Int. Conference SAFECOMP’11, pages 15–28 (2011)
12.
Zurück zum Zitat Bernardi, S., Merseguer, J., Petriu, D. C.: A dependability profile within MARTE. In Journal of Software and Systems Modeling (2009) Bernardi, S., Merseguer, J., Petriu, D. C.: A dependability profile within MARTE. In Journal of Software and Systems Modeling (2009)
13.
Zurück zum Zitat CENELEC. EN50126 railways applications - the specification and demonstration of reliability, availability, maintainability and safety (RAMS) (1999) CENELEC. EN50126 railways applications - the specification and demonstration of reliability, availability, maintainability and safety (RAMS) (1999)
14.
Zurück zum Zitat Dai, Z.: Model-driven testing with UML 2.0. In Proc. of the 2nd European Workshop on Model Driven, Architecture (2004) Dai, Z.: Model-driven testing with UML 2.0. In Proc. of the 2nd European Workshop on Model Driven, Architecture (2004)
15.
Zurück zum Zitat Fantechi, A., Gnesi, S.: On the adoption of model checking in safety-related software industry. In Proceedings of the 30th International Conference on Computer Safety, Reliability, and Security, SAFECOMP’11, pages 383–396 (2011) Fantechi, A., Gnesi, S.: On the adoption of model checking in safety-related software industry. In Proceedings of the 30th International Conference on Computer Safety, Reliability, and Security, SAFECOMP’11, pages 383–396 (2011)
16.
Zurück zum Zitat Flammini, F., Marrone, S., Mazzocca, N., Nardone, R., Vittorini, V.: Model-driven V&V processes for computer based control systems: A unifying perspective. In Proc. ISOLA 2012, LNCS, pages 190–204. Springer, Berlin Heidelberg (2012) Flammini, F., Marrone, S., Mazzocca, N., Nardone, R., Vittorini, V.: Model-driven V&V processes for computer based control systems: A unifying perspective. In Proc. ISOLA 2012, LNCS, pages 190–204. Springer, Berlin Heidelberg (2012)
17.
Zurück zum Zitat Fleurey, F., Steel, J., Baudry, B.: Validation in model-driven engineering: testing model transformations. In First International Workshop on Model, Design and Validation (2004) Fleurey, F., Steel, J., Baudry, B.: Validation in model-driven engineering: testing model transformations. In First International Workshop on Model, Design and Validation (2004)
18.
Zurück zum Zitat Fuentes-Fernández, L., Vallecillo-Moreno, A.: An introduction to UML profiles. UML and Model, Engineering, 2 (2004) Fuentes-Fernández, L., Vallecillo-Moreno, A.: An introduction to UML profiles. UML and Model, Engineering, 2 (2004)
19.
Zurück zum Zitat Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. SIGSOFT Softw. Eng. Notes 24(6), 146–162 (1999)CrossRef Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. SIGSOFT Softw. Eng. Notes 24(6), 146–162 (1999)CrossRef
20.
Zurück zum Zitat Gnesi, S., Margaria, T. (eds.): Formal Methods for Industrial Critical Systems: A Survey of Applications. John Wiley & Sons Inc, Hoboken, NJ, USA (2012) Gnesi, S., Margaria, T. (eds.): Formal Methods for Industrial Critical Systems: A Survey of Applications. John Wiley & Sons Inc, Hoboken, NJ, USA (2012)
21.
Zurück zum Zitat Holzmann, G.: SPIN model checker, the: primer and reference manual. Addison-Wesley Professional (2003) Holzmann, G.: SPIN model checker, the: primer and reference manual. Addison-Wesley Professional (2003)
22.
Zurück zum Zitat Hyoung, S. H., Insup, L., Oleg, S., Sung, D. C.: Automatic test generation from statecharts using model checking. In In Proc. of FATES’01, pages 15–30 (2001) Hyoung, S. H., Insup, L., Oleg, S., Sung, D. C.: Automatic test generation from statecharts using model checking. In In Proc. of FATES’01, pages 15–30 (2001)
23.
Zurück zum Zitat Javed, A. Z., Strooper, P. A., Watson, G. N.: Automated generation of test cases using model-driven architecture. In Proc. of AST ’07, pages 3-, Washington, DC, USA. IEEE Computer Society (2007) Javed, A. Z., Strooper, P. A., Watson, G. N.: Automated generation of test cases using model-driven architecture. In Proc. of AST ’07, pages 3-, Washington, DC, USA. IEEE Computer Society (2007)
24.
Zurück zum Zitat Jouault, F., Kurtev, I.: Transforming models with atl. In: Bruel, Jean-Michel (ed.) Satellite Events at the MoDELS 2005 Conference, volume 3844 of LNCS, pp. 128–138. Springer, Berlin Heidelberg (2006) Jouault, F., Kurtev, I.: Transforming models with atl. In: Bruel, Jean-Michel (ed.) Satellite Events at the MoDELS 2005 Conference, volume 3844 of LNCS, pp. 128–138. Springer, Berlin Heidelberg (2006)
25.
Zurück zum Zitat Kent, S.: Model driven engineering. In Proc. of the International Conference on Integrated Formal Methods, IFM ’02, pages 286–298 (2002) Kent, S.: Model driven engineering. In Proc. of the International Conference on Integrated Formal Methods, IFM ’02, pages 286–298 (2002)
26.
Zurück zum Zitat Lagarde, F., Espinoza, H., Terrier, F., Gérard, S.: Improving UML profile design practices by leveraging conceptual domain models. In Proc. of the Int. conference on Automated Software Engineering, pages 445–448, New York, NY, USA. ACM (2007) Lagarde, F., Espinoza, H., Terrier, F., Gérard, S.: Improving UML profile design practices by leveraging conceptual domain models. In Proc. of the Int. conference on Automated Software Engineering, pages 445–448, New York, NY, USA. ACM (2007)
27.
Zurück zum Zitat Marrone, S., Papa, C., Vittorini, V.: Multiformalism and transformation inheritance for dependability analysis of critical systems. In Proc. of 8th Integrated formal methods, IFM’10, pages 215–228, Berlin, Heidelberg. Springer-Verlag (2010) Marrone, S., Papa, C., Vittorini, V.: Multiformalism and transformation inheritance for dependability analysis of critical systems. In Proc. of 8th Integrated formal methods, IFM’10, pages 215–228, Berlin, Heidelberg. Springer-Verlag (2010)
28.
Zurück zum Zitat UML profile for modeling and analysis of real-time and embedded systems (MARTE). Version 1.0, OMG document (2009) UML profile for modeling and analysis of real-time and embedded systems (MARTE). Version 1.0, OMG document (2009)
30.
Zurück zum Zitat Mazzini, S., Latella, D., Viva, D.: PRIDE: An integrated software development environment for dependable systems. DASIA 2004: Data Systems in, Aerospace (2004) Mazzini, S., Latella, D., Viva, D.: PRIDE: An integrated software development environment for dependable systems. DASIA 2004: Data Systems in, Aerospace (2004)
31.
Zurück zum Zitat Mussa, M., Ouchani, S., Al Sammane, W., Hamou-Lhadj, A.: A survey of model-driven testing techniques. Quality Software, International Conference on, pages 167–172, (2009) Mussa, M., Ouchani, S., Al Sammane, W., Hamou-Lhadj, A.: A survey of model-driven testing techniques. Quality Software, International Conference on, pages 167–172, (2009)
32.
Zurück zum Zitat UML testing profile (2012). Version 1.1, OMG document. UML testing profile (2012). Version 1.1, OMG document.
33.
Zurück zum Zitat Selic, B.: A systematic approach to domain-specific language design using UML. In ISORC ’07, pages 2–9, Washington, DC, USA. IEEE Computer Society (2007) Selic, B.: A systematic approach to domain-specific language design using UML. In ISORC ’07, pages 2–9, Washington, DC, USA. IEEE Computer Society (2007)
34.
Zurück zum Zitat Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Computing Surveys, 41(4) (2009) Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Computing Surveys, 41(4) (2009)
35.
Zurück zum Zitat Zander, J., Schieferdecker, I., Mosterman, P. J.: A taxonomy of model-based testing for embedded systems from multiple industry domains. Model-Based Testing for Embedded Systems, pages 3–22 (2011) Zander, J., Schieferdecker, I., Mosterman, P. J.: A taxonomy of model-based testing for embedded systems from multiple industry domains. Model-Based Testing for Embedded Systems, pages 3–22 (2011)
Metadaten
Titel
Towards Model-Driven V&V assessment of railway control systems
verfasst von
Stefano Marrone
Francesco Flammini
Nicola Mazzocca
Roberto Nardone
Valeria Vittorini
Publikationsdatum
01.11.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 6/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0320-7

Weitere Artikel der Ausgabe 6/2014

International Journal on Software Tools for Technology Transfer 6/2014 Zur Ausgabe

Premium Partner