The development of embedded software encompasses a wide range of best practices and development methodologies. For quality-critical projects intended for highly reliable applications, delivery of high quality software is an absolute requirement. In these situations, development and test teams must complete code reviews, perform unit and regression test, and testing on the target system. But is it enough? What if a critical defect escapes to software deployment and then to production? Formal methods based mathematical techniques may alleviate some of the doubt. Application of formal methods based code verification may provide precision in guiding software engineering teams to know which parts of code will not fail and isolate those aspects of code that will fail or most likely to fail. This paper will discuss the practical application of these techniques for the verification of software. As part of the application of this improvement process, the paper will explore how these techniques enable the creation of high quality embedded software.
展开▼
