Verifying embedded software functionality: Why it’s necessary
Formal verification in the auto industry
In order to see what the possibilities and opportunities are in terms of integrating validation into embedded system design flows, we can look at the automobile industry. It is widely recognized that automotive electronics is a wide market, with more and more functionalities in modern-day cars being software-controlled. Indeed, innovations
in automotive software can bring about new designs, a point often articulated by car manufacturers themselves. The by-now famous quotes such as “more than 90% of the innovation in a modern-day car is from the software” stand testimony to the importance of embedded software/systems in the design of a modern-day car.
Naturally, because of the importance of the various car components (brakes, airbags, etc.) functioning “correctly” during the driving of a car, rigorous validation of the hardware/software controlling these components is crucial. In other words, reliable and robust embedded system design flows that integrate extensive debugging/validation are a must.
To see further the importance of validation in embedded systems for automobiles, we can delve deeper into the various components of a car, which can be computer-controlled. Roughly speaking, these can be divided into three categories— engine features, cabin features, and entertainment.
Clearly, the engine features are the most safety-critical and the features related to in-vehicle entertainment are the least safety-critical. The engine features include critical features such as the brake and steering wheel; usually these features involve hard real-time constraints.
The cabin features include less critical (but important) features such as power windows and air conditioning. The entertainment or infotainment features include control of in-car devices such as GPS navigation systems, CD player, and in-car television, as well as communication between these devices.
Clearly, the computing component controlling the engine features (such as brakes) needs very rigorous validation—to the extent that the behavior of these computing components could be subjected to formal modeling and verification. For the cabin features, we at least need modeling and extensive testing of the computing components controlling the cabin features. For the infotainment features, we need performance analysis methods to ensure that the soft real-time constraints are satisfied.
Thus, as we can see from the discussion on the specific domain of automotive software, validation of different kinds are required for a complex embedded system. For the more safety-critical parts of the system, rigorous modeling and formal verification may be needed. For the less safety-critical parts, more extensive testing may be sufficient. Moreover, for the parts of the system controlling or ensuring real-time responses to/from the environment, detailed performance validation needs to be carried out.
Thus, the validation methods we employ can range from formal methods (such as model checking) to informal ones (such as testing). Moreover, the level of abstraction at which we employ the validation may vary—model-level validation or high-level implementation validation (where we consider only the inter-component behavior without looking inside the components); or low-level implementation validation (where we also look inside the system components). Finally, the criteria for validation may also vary—we may perform validation at different levels, to check for functionality errors, timing errors, and so on.
Figure 5-1 below visually depicts the intricacies of embedded system validation. In particular, Figure 5-1.1a shows the different levels (model/implementation) and criteria (performance/functionality) of system validation.
Click on image to enlarge.
Figure 5-1b illustrates the complications in functionality validation. For an embedded system that we seek to construct, we may design and elaborate it at different levels of details (or different levels of abstraction). If we are seeking functionality validation, then the higher the level of detail, the lower the formality of the validation method.
Thus, for system design at higher levels of abstraction, we may try out fully formal validation methods. On the other hand, as we start fleshing out the implementation details of the system under construction, we may settle for more informal validation methods such as extensive testing.As opposed to functionality validation, the picture appears somewhat different for timing validation—see Figure 5-1c.
As is well understood, embedded systems often incorporate hard or soft real-time constraints on interaction of the system with its physical environment—or, for that matter, interactions between the different components of the system. Hence, timing validation involves developing accurate estimates of the “system response time” (in response to some event from the environment).
Clearly, as the details of the embedded system are fleshed out, we can develop more accurate timing estimates and, in that sense, perform more detailed timing validation. Thus, Figure 5-1 shows the issues in validating functionality versus validating timing properties—both of which are of great importance in embedded system design flows. Two different aspects are being highlighted here:
1 - Formal verification of functionality is better conducted at higher levels of abstraction. As we start considering lower level details, formal approaches do not scale up, and informal validation methods such as testing come into play.
2 - For performance validation, as we consider lower level details, our performance estimates are more accurate.
The reader should note that other criteria along which embedded system validation may proceed, such as estimating the energy or area requirements of a system, also have certain basic similarities with timing validation. As the system design is elaborated in more detail, we can form a better idea about its timing, energy, and area requirements.
Loading comments... Write a comment