Automating Formal Modular Verification of Asynchronous Real-Time Embedded Systems

Most verification tools and methodologies such as model checking, equivalence checking, hardware verification, software verification, and hardware-software coverification often flatten out the behavior of a target system before verification. Inherent modularities, either explicit or implicit, functional or structural, are not exploited by these tools and algorithms. In this work, we show how assume-guarantee reasoning (AGR) can be used for such exploitations by integrating AGR into a verification tool. Targeting at realtime embedded systems, we propose procedures to automatically generate assumptions, guarantees, and time constraints, which otherwise require manual efforts and human creativity. Through a complex but comprehensible real-time embedded system example such as a Vehicle Parking Management System (VPMS), we illustrate the feasibility of the AGR approach and the extremely large reduction possible in state-space sizes when AGR is applied. Due to AGR, we also found five errors...

• Type: Conference
• Year: 2003
• Where: VLSID
• Authors: Pao-Ann Hsiung, Shu-Yu Cheng
• Keywords: AGR Approach, Computer Architecture, Hardware Verification, Most Verification Tools, VLSID 2003