VALIDATION

Validation loosely refers to the process of determining that a design is correct. Simulation remains the main tool to validate a model, but the importance of formal verification is growing, especially for safety-critical embedded systems. Although still in its infancy, it shows more promise than verification of arbitrary systems, such as generic software programs, because embedded systems are often specified in a more restricted way. For example, they are often finite-state. Many safety properties (including deadlock detection) can be detected in a time-independentway using existing model checking and language containment methods (see, e.g., Kurshan [53] and Burch et al. [54]). Unfortunately, verifying most temporal properties is much more difficult (Alur and Henzinger [55] provide a good summary). Much more research is needed before this is practical.