A contract-based method to specify stimulus-response requirements
Software Engineering
2017-04-18 v1
Abstract
A number of formal methods exist for capturing stimulus-response requirements in a declarative form. Someone yet needs to translate the resulting declarative statements into imperative programs. The present article describes a method for specification and verification of stimulus-response requirements in the form of imperative program routines with conditionals and assertions. A program prover then checks a candidate program directly against the stated requirements. The article illustrates the approach by applying it to an ASM model of the Landing Gear System, a widely used realistic example proposed for evaluating specification and verification techniques.
Keywords
Cite
@article{arxiv.1704.04905,
title = {A contract-based method to specify stimulus-response requirements},
author = {Alexandr Naumchev and Manuel Mazzara and Bertrand Meyer and Jean-Michel Bruel and Florian Galinier and Sophie Ebersold},
journal= {arXiv preprint arXiv:1704.04905},
year = {2017}
}