Verification of Embedded Software: Problems and Perspectives

Niveau: Supérieur
Verification of Embedded Software: Problems and Perspectives Patrick Cousot1 and Radhia Cousot2 1 École normale supérieure Département d'informatique 45 rue d'Ulm 75230 Paris cedex 05, France 2 Laboratoire d'informatique CNRS & École polytechnique 91128 Palaiseau cedex, France Abstract. Computer aided formal methods have been very successful for the verification or at least enhanced debugging of hardware. The cost of correction of a hardware bug is huge enough to justify high investments in alternatives to testing such as correctness verification. This is not the case for software for which bugs are a quite common situation which can be easily handled through online updates. However in the area of embedded software, errors are hardly tolerable. Such embedded software is often safety-critical, so that a software failure might create a safety hazard in the equipment and put human life in danger. Thus embedded software verification is a research area of growing importance. Present day software verification technology can certainly be useful but is yet too limited to cope with the formidable challenge of complete software verification. We highlight some of the problems to be solved and envision possible abstract interpretation based static analysis solutions. 1 Introduction Since the origin of computer science, software in general, whence embedded soft? ware in particular, expands continuously to consume available processor cycles and memory.

• abstract interpretation


• embedded software


• model checking


• checkers can verify


• based static analysis


• often only


• software verification


• verification tools