Hardware versus Software Model Checking

Question

Explain Hardware versus Software Model Checking?

Answer 1

Model checking can be applied to both hardware and software. In fact, at the system level it can be applied to both at the same time. The Intel Pentium bug in 1994 was the “disaster” that inspired the hardware industry to pursue formal verification of hardware designs by trying new techniques such as model checking, with the goal of preventing such expensive mistakes in the future. Since that time, model checking has been used extensively in the industry for hardware verification.

Model checking can also be applied to software systems at different stages of the development lifecycle. Used early in the lifecycle, it can analyze software requirements specifications (e.g., Holzmann 1990; Atlee and Gannon 1993; Chan et al. 1998; Chan et al.1999; Heitmeyer et al. 1998) and software design models (e.g., Allen, Garlan, and Ivers 1998; Dang and Kemmerer 1999; Holzmann 1997). This can work well because these models can be both interesting and small enough to avoid model checking’s performance limitations. Early use of model checking is effective since many safety-critical software defects are introduced early in the lifecycle (Lutz et al. 1998) and are expensive to correct later.

While early lifecycle analysis has its clear benefits, some software errors cannot be discovered in the requirements and design stages. Sometimes the details of the system are not sufficiently elaborated to reveal problems until implementation. Also, many errors are introduced during implementation.

NASA has encountered a number of software problems that were traced to implementation issues. For example, in 1999 the Mars Polar Lander (MPL) was lost during its final descent to the Martian surface at an estimated cost of $165 million. The most likely cause of failure was identified as a software-related problem—a single bad line of code. A variable that was not re-initialized after a spurious sensor signal associated with the craft’s legs falsely indicated that the craft had touched down when in fact it was some 130 feet above the surface. This caused the descent engines to shut down prematurely; MPL was destroyed in the subsequent impact.

Such errors result from software becoming a pervasive component of aerospace systems. There are similar trends in other industries, such as the growing use of Integrated Modular Avionics (IMA) in civil aviation, which allows applications of varying criticality levels to execute on a shared computing platform. The increased scope and complexity of software naturally make it more difficult to design and validate. This suggests that changes need to be made in how aerospace systems are verified and validated (Rushby 1999).