Abstract
While adding formal methods to traditional software development processes can provide very high levels of assurance and reduce costs by finding errors earlier in the development cycle, there are at least four criteria that should be considered before introducing formal methods into a project. This paper describes five successful examples of the use of formal methods in the development of high integrity systems and discusses how each project satisfied these criteria.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Miller, S., Anderson, E., Wagner, L., Whalen, M., Heimdahl, M.: Formal Verification of Flight Critical Software. In: AIAA Guidance, Navigation and Control Conference and Exhibit, AIAA-2005-6431, American Institute of Aeronautics and Astronautics (2005)
Whalen, M., Innis, J., Miller, S., Wagner, L.: ADGS-2100 Adaptive Display & Guidance System Window Manager Analysis, CR-2006-213952, NASA (2006)
Whalen, M., Cofer, D., Miller, S., Krogh, B., Storm, W.: Integration of Formal Analysis into a Model-Based Software Development Process. In: 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Berlin, Germany (2007)
Greve, D., Wilding, M., Vanfleet, W.M.: A Separation Kernel Formal Security Policy. In: Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003) (2003)
Greve, D., Richards, R., Wilding, M.: A Summary of Intrinsic Partitioning Verification. In: Fifth International Workshop on the ACL2 Prover and Its Applications (ACL2-2004) (2004)
Greve, D., Wilding, M., Richards, R., Vanfleet, W.M.: Formalizing Security Policies for Dynamic and Distributed Systems. In: Systems and Software Technology Conference (SSTC 2005), Utah State University (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miller, S.P. (2008). Will This Be Formal?. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2008. Lecture Notes in Computer Science, vol 5170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71067-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-71067-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71065-3
Online ISBN: 978-3-540-71067-7
eBook Packages: Computer ScienceComputer Science (R0)