Henzinger, Thomas AIST Austria ; Qadeer,Shaz ; Rajamani, Sriram K
Refinement checking is used to verify implementations against more abstract specifications. Assume-guarantee reasoning is used to decompose refinement proofs in order to avoid state-space explosion. In previous approaches, specifications are forced to operate on the same time scale as the implementation. This may lead to unnatural specifications and inefficiencies in verification. We introduce a novel methodology for decomposing refinement proofs of temporally abstract specifications, which specify implementation requirements only at certain sampling instances in time. Our new assume-guarantee rule allows separate refinement maps for specifying functionality and timing.We present the theory for the correctness of our methodology, and illustrate it using a simple example. Support for sampling and the generalized assume-guarantee rule have been implemented in the model checker Mocha and successfully applied to verify the VGI multiprocessor dataflow chip with 6 million transistors.
208 - 221
CAV: Computer Aided Verification
Henzinger TA, Qadeer S, Rajamani S. Assume-guarantee refinement between different time scales. In: Vol 1633. Springer; 1999:208-221. doi:10.1007/3-540-48683-6_20
Henzinger, T. A., Qadeer, S., & Rajamani, S. (1999). Assume-guarantee refinement between different time scales (Vol. 1633, pp. 208–221). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/3-540-48683-6_20
Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Assume-Guarantee Refinement between Different Time Scales,” 1633:208–21. Springer, 1999. https://doi.org/10.1007/3-540-48683-6_20.
T. A. Henzinger, S. Qadeer, and S. Rajamani, “Assume-guarantee refinement between different time scales,” presented at the CAV: Computer Aided Verification, 1999, vol. 1633, pp. 208–221.
Henzinger TA, Qadeer S, Rajamani S. 1999. Assume-guarantee refinement between different time scales. CAV: Computer Aided Verification, LNCS, vol. 1633. 208–221.
Henzinger, Thomas A., et al. Assume-Guarantee Refinement between Different Time Scales. Vol. 1633, Springer, 1999, pp. 208–21, doi:10.1007/3-540-48683-6_20.