caa a22 4500 475797477 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000101xx s 000 0 eng 10.1023/A:1008729625855 doi (NATIONALLICENCE)springer-10.1023/A:1008729625855 Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem [Elektronische Daten] [Abdel Mokkedem, Ravi Hosabettu, Michael Jones, Ganesh Gopalakrishnan] 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. Kluwer Academic Publishers, 2000 I/O systems nationallicence formal design nationallicence theorem-proving nationallicence model checking nationallicence Mokkedem Abdel Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut Hosabettu Ravi Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut Jones Michael Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut Gopalakrishnan Ganesh Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 93-119 0925-9856 16:1<93 2000 16 10703 https://doi.org/10.1023/A:1008729625855 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008729625855 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Mokkedem Abdel Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut NATIONALLICENCE 700 1- Hosabettu Ravi Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut NATIONALLICENCE 700 1- Jones Michael Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut NATIONALLICENCE 700 1- Gopalakrishnan Ganesh Department of Computer Science, University of Utah, 84112-9205, Salt Lake City, UT, USA aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 93-119 0925-9856 16:1<93 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer