국내 최대 기계 및 로봇 연구정보

기술보고서

기술보고서 게시판 내용
타이틀	Formal Methods for Life-Critical Software
저자	Ricky W. Butler and Sally C. Johnson
Keyword	formal methods, formal specification, verification and validation, mechanical verification, life-critical
URL	http://techreports.larc.nasa.gov/ltrs/PDF/aiaa-93-4516.pdf
보고서번호	AIAA-93-4516
발행년도	1993
출처	NASA Langley Research Center
ABSTRACT	The use of computer software in life-critical applications, such as for civil air transports, demands the use of rigorous formal mathematical verification procedures. This paper demonstrates how to apply formal methods to the development and verification of software by leading the reader step-by-step through requirements analysis, design, implementation, and verification of an electronic phone book application. The current maturity and limitations of formal methods tools and techniques are then discussed, and a number of examples of the successful use of formal methods by industry are cited.