Item Details

Print View

Raising Formal Methods to the Requirements Level

Furia, Carlo; Rossi, Matteo; Strunk, Elisabeth; Mandrioli, Dino; Knight, John
Format
Report
Author
Furia, Carlo
Rossi, Matteo
Strunk, Elisabeth
Mandrioli, Dino
Knight, John
Abstract
In contrast with a formal notion of specification, requirements are often considered an informal entity. In a companion paper [SFRKM06], we have proposed a reference model that provides a clear distinction between requirements and specification, a distinction not based on the degree of formality. Using that notion of requirements, this paper shows how requirements as well as specifications can be formalized. The formalization of requirements allows one to �lift� the well-known practices of formal analysis and verification from the specification/implementation level up to the highest level of abstraction in the development of a software product. In particular, we show how a formal validity argument can be constructed, proving that the formal specification satisfies its formal requirements. These ideas are demonstrated in an illustrative example based on a runway incursion prevention system, which was also partially presented in [SFRKM06]. Although our results and methods are of general applicability, we focus especially on the real-time aspects of the example; in order to support real-time formalization and reasoning, we exploit the ArchiTRIO formal language in a UML-like environment.
Language
English
Date Received
2012-10-29
Published
University of Virginia, Department of Computer Science, 2006
Published Date
2006
Rights
All rights reserved (no additional license for public reuse)
Collection
Libra Open Repository

Availability

Access Online