Integrating formal methods into the development process
- 1 September 1990
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Software
- Vol. 7 (5) , 37-50
- https://doi.org/10.1109/52.57891
Abstract
It is shown that integrating formal specification and verification with development is faster and more cost-effective than doing the steps separately or in parallel. This case study demonstrates their application in a security context and documents their use in several phases of development, starting from the requirements of a terminal serving a security officer, on through formal requirements and design expressed as state transitions, to detailed design specifications and proofs that these agree with higher-level specifications, stopping just before code-level verification (due to complications typical of such projects). The effects of verification on this particular project are addressed.Keywords
This publication has 5 references indexed in Scilit:
- Toward Verified Execution EnvironmentsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1987
- Processor-per-Domain Guard ArchitecturePublished by Institute of Electrical and Electronics Engineers (IEEE) ,1983
- Formal specification as a design toolPublished by Association for Computing Machinery (ACM) ,1980
- Abstract data types and software validationCommunications of the ACM, 1978
- Proof of correctness of data representationsActa Informatica, 1972