# A contract-based method to specify stimulus-response requirements

## TL;DR

This paper introduces a novel method for specifying and verifying stimulus-response requirements by translating declarative specifications into imperative programs and using program provers for validation, demonstrated on an aircraft landing gear system model.

## Contribution

It presents a new approach to specify and verify stimulus-response requirements through imperative routines and formal verification, bridging the gap between declarative specifications and executable programs.

## Key findings

- Successfully applied to an ASM model of the Landing Gear System
- Enables direct verification of requirements against imperative programs
- Provides a practical framework for formal specification and validation

## 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.