Verification of a parameterized bus arbitration protocol

Abstract

Model Checking is well established as a verification technique for finite-state systems. Many protocols, while composed of finite-state processes, are parameterized by the number of such processes, hence Model Checking cannot be applied directly to determine correctness of the inherently infinite-state parameterized system. We present a case study on the verification of such a parameterized protocol, the SAE-J1850 data transfer procotol. This is a standard in the automobile industry, where it is used to transmit data between various sensors and micro-controllers in an automobile. The protocol communicates data over a single-wire bus, and provides on-the-fly arbitration between competing transmissions. Our verification effort is interesting from many aspects: it proves correctness for arbitrary instances, is largely automated, and uses abstraction in an essential way. The abstractions used are exact, in the sense that a property is true of the parameterized protocol if and only if it is true of the finite-state abstraction.