Warranty requirements
Formal methods for the verification of embedded systems

The criticality of embedded systems varies widely. Applications involving the transport of people (avionics, railways, intelligent automobiles) or supervising hazardous industrial processes (nuclear power plants, chemical processes), or medical processes (surgical assistance) must offer guarantees of correct operation, established by compliance with very strict design procedures and certified by independent bodies. They must also meet robustness requirements in the event of failure of one or more elements of the application or its environment.

On the other hand, cell phone applications do not involve human life in the same way as the aforementioned cases. They do, however, need to guarantee the confidentiality, integrity and availability of the...