Sciweavers

Share
VLSID
2003
IEEE

Automating Formal Modular Verification of Asynchronous Real-Time Embedded Systems

9 years 10 months ago
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...
Pao-Ann Hsiung, Shu-Yu Cheng
Added 01 Dec 2009
Updated 01 Dec 2009
Type Conference
Year 2003
Where VLSID
Authors Pao-Ann Hsiung, Shu-Yu Cheng
Comments (0)
books