Item Details

Raising Formal Methods to the Requirements Level

Furia, Carlo; Rossi, Matteo; Strunk, Elisabeth; Mandrioli, Dino; Knight, John
Furia, Carlo
Rossi, Matteo
Strunk, Elisabeth
Mandrioli, Dino
Knight, John
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.
Date Received
University of Virginia, Department of Computer Science, 2006
Published Date
Libra Open Repository
Logo for In CopyrightIn Copyright


Access Online