Marco Filax, Tim Gonschorek, Frank Ortmeier : Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models. In: Publishing, Springer International (Hrsg.): Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, S. 106 - 122, 2016, ISBN: 978-3-319-33951-1.

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.

BibTeX (Download)

@inproceedings{MF16-RSSR,
title = {Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models},
author = {Marco Filax and Tim Gonschorek and Frank Ortmeier },
editor = {Springer International Publishing },
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/RSSR_CorrectFormalizationOfRequirementSpecifications.pdf},
doi = {10.1007/978-3-319-33951-1_8},
isbn = {978-3-319-33951-1},
year  = {2016},
date = {2016-06-15},
booktitle = {Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings},
pages = {106 - 122},
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.},
keywords = {Formal Modelling Process, Railway System Verification, Requirements Traceability, System Verification, VIP-MoBaSA},
pubstate = {published},
tppubtype = {inproceedings}
}