### Abstract

This paper describes an experiment conducted to determine how effectively formal methods could be used to capture and validate the requirements of a typical embedded system. A model of the mode logic of a Flight Guidance System was specified in the RSML^{-e} notation and translated into the NuSMV model checker and the PVS theorem prover. These tools were then used to verify several hundred properties of the RSML^{-e} model. In the process, several errors were discovered and corrected in the original model. This demonstrates that formal requirements models can be written for real problems and that formal analysis tools have matured to the point where they can be used to find errors before implementation. It also points out a clear relationship between requirements stated informally as "shalls", formal properties, and requirements models.

Original language | English (US) |
---|---|

Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Editors | Keijiro Araki, Stefania Gnesi, Dino Mandrioli |

Publisher | Springer Verlag |

Pages | 75-93 |

Number of pages | 19 |

ISBN (Print) | 9783540408284 |

DOIs | |

State | Published - 2003 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 2805 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

## Fingerprint Dive into the research topics of 'Proving the shalls'. Together they form a unique fingerprint.

## Cite this

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*(pp. 75-93). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2805). Springer Verlag. https://doi.org/10.1007/978-3-540-45236-2_6