Research
Semiformal Verification of embedded Software
The verification of complex systems, like embedded systems as well as SoCs, can not be considered only on hardware module level anymore. The amount of software has increased significantly over the last years and therefore, the verification of embedded software has become a fundamental importance. The most commonly used approaches to verify embedded software are based on co-debugging or co-simulation, which have the coverage problem. Formal verification assures complete coverage but is limited to the size of module that can be verified. In this paper, we present a new semiformal verification approach in order to verify temporal properties of embedded software, based on the combination of simulation and formal verification approaches.
Hardware verification techniques have advanced considerably over the last few years. Mature approaches based on Formal Methods, Assertion-Based Verification and Coverage Driven Verification (CDV) are used with success for the verification of small, medium and large hardware systems. On the other hand, verification of software, especially software with strong hardware dependencies, is still in its infancy. Considering the experience made in the area of hardware verification, it would be desirable to use the same principles to the verification of embedded software and its boundary with the hardware.
The current practiced methods for embedded software verification are still mostly based on co-debug, co-simulation or co-verification. These methods usually provide certain inputs and observe the corresponding outputs for software. The efficiency of dynamic verification is directly proportional to the cost. The main advantage of simulation based verification is that we can traverse further deep into the system state space. However, it often faces a coverage problem. One way to overcome this problem is by using the formal verification on software. The formal verification explores the state space exhaustively but frequently suffers from the state space explosion problem.
The semiformal verification approach can be used to overcome the drawbacks of both dynamic and static verification. This approach combines the benefits of going deeper and covers exhaustively the state space of the system. However, to the best of our knowledge, semiformal verification approaches have been applied only to hardware verification but not to the embedded software area. They used one step interaction between dynamic and static verification i.e. first start with the simulation and then later the formal verification.
