ISSN:
1572-8102
Keywords:
I/O systems
;
formal design
;
theorem-proving
;
model checking
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract The transaction ordering problem of the original PCI 2.1 standard bus specification violates the desired correctness property of maintaining the so called ‘Producer/Consumer’ relationship between writers and readers of data. This violation stems mainly from the so called completion stealing problem, first identified and solved by Corella et al. [4], and supported by a formal paper and pencil argument. In this paper, we develop a flexible graph theory library in PVS for modeling computer bus structures, formalize the PCI 2.1 protocol containing the solution of [4] in it, and mechanically prove the absence of completion stealing. Next, we define the Producer/Consumer property in PVS and sketch its mechanical proof. Noting the complexity of this proof effort (unfinished as yet), we explore a combination of theorem proving and model-checking in which the model used for model-checking is made tractable by exploiting the formal theorems established during theorem-proving as well as several intuitively justified assumptions. The theorem-proving infrastructure we have built for modeling CPU interconnect structures is highly reusable. Our work is one example of a natural division of labor between theorem-proving and model-checking in tackling system-level verification problems under realistic time budgets.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1008729625855
