2021/02/11 by Atif Mashkoor, Mashkoor, Atif, Michaël Leuschel +3 · 2 citations
Computer Science · #Advanced Software Engineering Methodologies #Model-Driven Software Engineering Techniques #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.2102.06037
Traditionally, practitioners use formal methods pre-dominately for one half\nof the quality-assurance process: verification (do we build the software\nright?). The other half -- validation (do we build the right software?) -- has\nbeen given comparatively little attention. While verification is the core of\nrefinement-based formal methods, where each new refinement step must preserve\nall properties of its abstract model, validation is usually postponed until the\nlatest stages of the development, when models can be automatically executed.\nThus mistakes in requirements or in their interpretation are caught too late:\nusually at the end of the development process. In this paper, we present a\nnovel approach to check compliance between requirements and their formal\nrefinement-based specification during the earlier stages of development. Our\nproposed approach -- "validation obligations" -- is based on the simple idea\nthat both verification and validation are an integral part of all refinement\nsteps of a system.\n