An Example Demonstrating the Requirement of Fully Formal Verification Method

ABSTRACT. Concurrency and synchronization is an important behavior of hardware and software systems. Finding defects in the late phase of system development process is not acceptable anymore in industrial applications because of its highly capital investment in modern complex systems. This paper demonstrates system verification by two approaches: model checking and proof checker. Here verification of a concurrent running architecture is demonstrated in both approaches to exhibit the requirement of fully formal verification method in order to generate a better hardware and software quality. To support this, we will describe how the proof checker is used for complete verification of a system in terms of any input size and complexity.