Practical verification of embedded software

Advances in processor speed, memory capacities, sensors, and peripherals ha ve enabled the inexpensive fabrication of sophisticated products. They rang e from simple controllers in applications such as mobile phones and hi-fi e quipment to highly complex software in cars and airplanes. Unfortunately, t he lack of good design methods and tools is a major bottleneck in the devel opment of these products, particularly those with a short life cycle such a s consumer electronics and household appliances. Developing embedded softwa re for large, complicated applications requires models that are both intell ectually manageable and physically realizable. Choosing a modeling techniqu e is a compromise between conflicting goals. Models must not only be easy t o comprehend and construct, but they also must be practicable and provide p latforms for analysis. Using a new verification algorithm called the compos itional backward technique, the authors demonstrate that they can exhaustiv ely verify even the largest industrial applications-comprising more than 1, 000 components-in a few minutes on a standard PC.