Software Reliability through Theorem Proving

Defence Science Journal

S.G.K. Murthy¹  K. Raja Sekharam¹ 

[1] Defence Research & Development Laboratory, Hyderabad – 500 058

关键词: Software reliability;    formal methods;    software testing;    software model checking;    software theorem proving;    stanford temporal theorem prover (STeP);    autopilot software;   

DOI  :  

学科分类：社会科学、人文和艺术（综合）

来源: Defence Scientific Information & Documentation Centre

【 摘 要 】

Improving software reliability of mission-critical systems is widely recognised as one of the major challenges. Early detection of errors in software requirements, designs and implementation, need rigorous verification and validation techniques. Several techniques comprising static and dynamic testing approaches are used to improve reliability of mission critical software; however it is hard to balance development time and budget with software reliability. Particularly using dynamic testing techniques, it is hard to ensure software reliability, as exhaustive testing is not possible. On the other hand, formal verification techniques utilise mathematical logic to prove correctness of the software based on given specifications, which in turn improves the reliability of the software. Theorem proving is a powerful formal verification technique that enhances the software reliability for missioncritical aerospace applications. This paper discusses the issues related to software reliability and theorem proving used to enhance software reliability through formal verification technique, based on the experiences with STeP tool, using the conventional and internationally accepted methodologies, models, theorem proving techniques available in the tool without proposing a new model. Defence Science Journal, 2009, 59(3), pp.314-317, DOI:http://dx.doi.org/10.14429/dsj.59.1527

【 授权许可】

Unknown