SpringerLink
Log in

Building Models We Can Rely On: Requirements Traceability for Model-Based Verification Techniques

  • Conference paper
  • First Online:
Model-Based Safety and Assessment (IMBSA 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10437))

Included in the following conference series:

Abstract

Proving the safety of a critical system is a complex and complicated task. Model-based formal verification techniques can help to verify a System Requirement Specification (SRS) with respect to normative and safety requirements. Due to an early application of these methods, it is possible to reduce the risk of high costs caused by unexpected, late system adjustments. Nevertheless, they are still rarely used. One reason among others is the lack of an applicable integration method in an existing development process.

In this paper, we propose a process to integrate formal model-based verification techniques into the development life-cycle of a safety critical system. The core idea is to systematically refine informal specifications by (1) categorization, (2) structural refinement, (3) expected behavioral refinement, and finally, (4) operational semantics. To support modeling, traceability is upheld through all refinement steps and a number of consistency checks are introduced.

The proposed process has been jointly developed with the German Railroad Authority (EBA) and an accredited safety assessor. We implemented an Eclipse-based IDE with connections to requirement and systems engineering tools as well as various verification engines. The applicability of our approach is demonstrated via an industrial-sized case study in the context of the European Train Control System with ETCS Level 1 Full Supervision.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Acknowledged in IEC 61508-7 section B2.2.

  2. 2.

    Available online: https://cse.cs.ovgu.de/vecs/index.php/product/achievements/casestudies/etcs.

  3. 3.

    Worst case approximation by multiplying all possible state variable values.

References

  1. Aceituna, D., Do, H.: Exposing the susceptibility of off-nominal behaviors in reactive system requirements. In: RE, pp. 136–145 (2015). doi:10.1109/RE.2015.7320416

  2. Aceituna, D., Do, H., Srinivasan, S.: A systematic approach to transforming system requirements into model checking specifications. In: ICSE, pp. 165–174 (2014). doi:10.1145/2591062.2591183

  3. Ammann, P.E., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: Proceedings of the Second International Conference on Formal Engineering Methods, pp. 46–54. IEEE (1998). doi:10.1007/3-540-48166-4_10

  4. Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008). ISBN: 9780262026499

    MATH  Google Scholar 

  5. Bos, V., Bruintjes, H., Tonetta, S.: Catalogue of system and software properties. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9922, pp. 88–101. Springer, Cham (2016). doi:10.1007/978-3-319-45477-1_8

    Chapter  Google Scholar 

  6. Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173–186. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04468-7_15

    Chapter  Google Scholar 

  7. Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic fault tree analysis for reactive systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 162–176. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75596-8_13

    Chapter  Google Scholar 

  8. Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: From informal requirements to property-driven formal validation. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 166–181. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03240-0_15

    Chapter  Google Scholar 

  9. EN 50128: Railway applications-communication, signaling and processing systems-software for railway control and protection systems (2011)

    Google Scholar 

  10. Filax, M., Gonschorek, T., Lipaczewski, M., Ortmeier, F.: On traceability of informal specifications for model-based verification. In: IMBSA: Short & Tutorial Proceedings, pp. 11–18. OvGU Magdeburg (2014)

    Google Scholar 

  11. Filax, M., Gonschorek, T., Ortmeier, F.: Correct formalization of requirement specifications: a v-model for building formal models. In: Lecomte, T., **er, R., Romanovsky, A. (eds.) RSSR 2016. LNCS, vol. 9707, pp. 106–122. Springer, Cham (2016). doi:10.1007/978-3-319-33951-1_8

    Google Scholar 

  12. Ge, X., Paige, R.F., McDermid, J.A.: Analysing system failure behaviours with PRISM. In: SSIRI-C, pp. 130–136 (2010). doi:10.1109/SSIRI-C.2010.32

  13. Güdemann, M., Ortmeier, F., Reif, W.: Using deductive cause-consequence analysis (DCCA) with SCADE. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol. 4680, pp. 465–478. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75101-4_44

    Chapter  Google Scholar 

  14. Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Sci. Comput. Program. 82, 2–21 (2014). doi:10.1016/j.scico.2013.03.008

    Article  Google Scholar 

  15. IEC 61508: Functional safety of electrical/electronic/programmable electronic safety-related systems (2005)

    Google Scholar 

  16. ISO 26262: Road Vehicles-Functional Safety (2009)

    Google Scholar 

  17. OMG UML: Unified modeling language, superstructure (2011)

    Google Scholar 

  18. Ortmeier, F., Schellhorn, G.: Formal fault tree analysis-practical experiences. Electron. Not. Theoret. Comput. Sci. 185, 139–151 (2007). doi:10.1016/j.entcs.2007.05.034

    Article  MATH  Google Scholar 

  19. Soliman, D., Frey, G., Thramboulidis, K.: On formal verification of function block applications in safety-related software development. IFAC 46(22), 109–114 (2013). doi:10.3182/20130904-3-UK-4041.00015

    Google Scholar 

  20. Withall, S.: Software Requirement Patterns (Developer Best Practices). Microsoft Press (2007). ISBN: 9780735623989

    Google Scholar 

Download references

Acknowledgments

The work presented in this paper is funded by the German Ministry of Education and Science (BMBF) in the VIP-MoBaSA project (project-Nr. 16V0360).

Author information

Authors and Affiliations

  1. Chair of Software Engineering, Otto-von-Guericke University of Magdeburg, Magdeburg, Germany

    Marco Filax, Tim Gonschorek & Frank Ortmeier

Authors
  1. Marco Filax
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tim Gonschorek
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frank Ortmeier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marco Filax .

Editor information

Editors and Affiliations

  1. Fondazione Bruno Kessler, Trento, Italy

    Marco Bozzano

  2. University of Hull, Hull, United Kingdom

    Yiannis Papadopoulos

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Filax, M., Gonschorek, T., Ortmeier, F. (2017). Building Models We Can Rely On: Requirements Traceability for Model-Based Verification Techniques. In: Bozzano, M., Papadopoulos, Y. (eds) Model-Based Safety and Assessment. IMBSA 2017. Lecture Notes in Computer Science(), vol 10437. Springer, Cham. https://doi.org/10.1007/978-3-319-64119-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-64119-5_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-64118-8

  • Online ISBN: 978-3-319-64119-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation