It’s Time to Start Using Formal Methods for Engineering Embedded Systems

Executive Summary

If embedded systems are to function effectively and safely, that software must be extremely reliable. To meet ever-increasing reliability demands, new methodologies for specifying, designing, and coding software in embedded systems – methods like model-based design – have evolved. Yet software verification, for the most part, has remained rooted in the same methods from 40 years ago. We’re still defining test cases and monitoring test coverage. In other words, our procedures for the verification of software have not kept pace with our advances in designing and implementing it.

As the complexity of embedded systems and their reliance on software for mission-critical and safety-critical functions continue to grow, the organizations that develop these systems will eventually be forced to adopt more robust methodologies for their verification.

Fortunately, recent advances have made verification techniques known as formal methods a viable alternative to traditional testing. We believe the use of formal methods for model-based design verification will offer systems and software engineers – and the companies they work for – a much higher level of confidence in the accuracy and robustness of the embedded systems they design and produce.

We believe the time to begin transitioning to formal methods for model-based design verification is now. In this article, we’ll explain why. But first, let’s look at what we mean by formal methods.

Download the White Paper