Skip to main content
SpringerLink
Log in

Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models

  • Conference paper
  • First Online:
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail 2016)

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

Abstract

In recent years, formal methods have become an important approach to ensure the correct function of complex hardware and software systems. Many standards for safety critical systems recommend or even require the use of formal methods. However, building a formal model for a given specification is challenging. This is, because verification results must be considered with respect to the validity of the model.

This leads to the question: “Did I build the right model?”. For system development the analogous question “Did I build the right system?”. This is often answered with requirements traceability through the whole development cycle. For formal verification this question often remains unanswered.

The standard model, which is used in development of safety critical applications is the V-model. The core idea is to define tests for each phase during system development. In this paper, we propose an approach - analogously to the V-model for development - which ensures correctness of the formal model with respect to requirements. We will illustrate the approach on a small example from the railways domain.

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

Access this chapter

Log in via an institution
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 shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://www.eba.bund.de.

  2. 2.

    http://cse.cs.ovgu.de/vecs.

  3. 3.

    https://cse.cs.ovgu.de/vecs/index.php/techniques/examples/17-casestudies/25-pzb- achievements.

  4. 4.

    Worst case approximation by multiplying all possible state variable values.

References

  1. Boehm, B.W.: Verifying and validating software requirements and design specifications. IEEE Softw. 1, 75–88 (1984)

    Article  Google Scholar 

  2. Bose, P.: Automated translation of UML models of architectures for verification and simulation using spin. In: ASE, pp. 102–109. IEEE (1999)

    Google Scholar 

  3. Brill, M., Buschermöhle, R., Damm, W., Klose, J., Westphal, B., Wittke, H.: Formal verification of LSCs in the development process. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 494–516. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Burmester, S., Giese, H., Hirsch, M., Schilling, D.: Incremental design and formal verification with UML/RT in the FUJABA real-time tool suite. In: SVERTS, pp. 1–20. Citeseer (2004)

    Google Scholar 

  5. Carnevali, L., Grassi, L., Vicario, E.: A tailored V-model exploiting the theory of preemptive time petri nets. In: Kordon, F., Vardanega, T. (eds.) Ada-Europe 2008. LNCS, vol. 5026, pp. 87–100. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Heidelberg (2014)

    Google Scholar 

  7. CENELEC: 50129. Railway Applications: Safety Related Electronic Systems for Signalling (1998)

    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)

    Chapter  Google Scholar 

  9. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  10. Cimperman, R.: UAT Defined: A Guide to Practical User Acceptance Testing. Addison-Wesley Professional, Upper Saddle River (2006)

    Google Scholar 

  11. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  12. David, A., Möller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: on branching versus linear time temporal logic. J. ACM 33, 151–178 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  14. Fecher, H., Schönborn, J., Kyas, M., de Roever, W.-P.: 29 new unclarities in the semantics of UML 2.0 state machines. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 52–65. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Google Scholar 

  16. Giese, H., Tichy, M., Burmester, S., Schäfer, W., Flake, S.: Towards the compositional verification of real-time UML designs. In: ESEC/FSE, pp. 38–47 (2003)

    Google Scholar 

  17. Gonschorek, T., Filax, M., Lipaczewski, M., Ortmeier, F.: VECS - verification enviroment for critical systems - tool supported formal modeling an verification. In: IMBSA 2014: Short & Tutorial Proceedings, pp. 63–64 (2014)

    Google Scholar 

  18. Güdemann, M.: Qualitative and quantitative formal model-based safety analysis. Ph.D. thesis, Otto-von-Guericke-Universität Magdeburg (2011)

    Google Scholar 

  19. Lano, K., Clark, D., Androutsopoulos, K.: UML to B: formal verification of object-oriented models. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 187–206. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  20. Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the spin model-checker. FAC 11, 637–664 (1999)

    MATH  Google Scholar 

  21. Lilius, J., Paltor, I.P.: Formalising UML state machines for model checking. In: France, R.B. (ed.) UML 1999. LNCS, vol. 1723, pp. 430–444. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  22. Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: ASE, pp. 255–258. IEEE (1999)

    Google Scholar 

  23. OMG: OMG Unified Modeling Language (OMG UML), Superstructure. Object Management Group (2011)

    Google Scholar 

  24. Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. TOSEM 15, 92–122 (2006)

    Article  Google Scholar 

  25. Tang, W., Ning, B., Xu, T., Zhao, L.H.: Scenario-based modeling and verification of system requirement specification for the european train control system. In: Computers in Railways XII, pp. 759–770 (2010)

    Google Scholar 

  26. Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322–331. IEEE (1986)

    Google Scholar 

  27. Varró, A.: A formal semantics of UML statecharts by model transition systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 378–392. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  28. Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and sat-based reachability in hardware model checking. In: FMCAD, pp. 173–181. IEEE (2012)

    Google Scholar 

Download references

Acknowledgment

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 Universität 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. ClearSy, Aix en Provence, France

    Thierry Lecomte

  2. Siemens AG, Braunschweig, Niedersachsen, Germany

    Ralf Pinger

  3. Newcastle University, Newcastle upon Tyne, United Kingdom

    Alexander Romanovsky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Filax, M., Gonschorek, T., Ortmeier, F. (2016). Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2016. Lecture Notes in Computer Science(), vol 9707. Springer, Cham. https://doi.org/10.1007/978-3-319-33951-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-33951-1_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-33950-4

  • Online ISBN: 978-3-319-33951-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation