TY - UNPB
T1 - Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification
AU - Mashkoor, Atif
AU - Leuschel, Michael
AU - Egyed, Alexander
PY - 2021
Y1 - 2021
N2 - Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half -- validation (do we build the right software?) -- has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus mistakes in requirements or in their interpretation are caught too late: usually at the end of the development process. In this paper, we present a novel approach to check compliance between requirements and their formal refinement-based specification during the earlier stages of development. Our proposed approach -- "validation obligations" -- is based on the simple idea that both verification and validation are an integral part of all refinement steps of a system.
AB - Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half -- validation (do we build the right software?) -- has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus mistakes in requirements or in their interpretation are caught too late: usually at the end of the development process. In this paper, we present a novel approach to check compliance between requirements and their formal refinement-based specification during the earlier stages of development. Our proposed approach -- "validation obligations" -- is based on the simple idea that both verification and validation are an integral part of all refinement steps of a system.
UR - https://arxiv.org/abs/2102.06037
U2 - 10.48550/arXiv.2102.06037
DO - 10.48550/arXiv.2102.06037
M3 - Preprint
T3 - CoRR - Computing Research Repository
BT - Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification
ER -