Portal de Periódicos da CAPES

Formal Modeling and Validation Applied to a Commercial Coherent Bus: A Case Study

1997; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-0-387-35190-2_4

1868-422X

Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdelillah Mokkedem, Ratan Nalumasu,

Software Testing and Debugging Techniques

The degree to which formal verification methods are adopted in practice depends on concrete demonstrations of their applicability on real-world examples. In this paper, we present our efforts in this regard involving a commercial high-speed split-transaction bus called the Runway. Modern busses such as the Runway deal with so many inter-twined and complex issues that successful application of formal method requires separation of concerns, and the use of the most appropriate tool for each concern. We report our experiments towards this end through the use of the PVS theorem-prover to formally analyze the high-level functional behavior of the bus and the HDL-based model-checker VIS to verify the pipelined arbitration protocol of the bus. The high degree of effort found necessary, as well as the specific abstraction mechanisms found useful in obtaining these formal models are discussed in detail.