A Model-Checked (IC)-C-2 Specification

(IC)-C-2 is a pervasive bus protocol used for querying sensors and actuators, but it is plagued with incompatible devices, violating the specification at various levels. Interacting with partially compliant devices poses several challenges. Compatibility of the controller interface, as well as the driver code, must be checked manually and potentially changed. This is a difficult process, as interactions with other bus devices must also be considered. We propose a model checking approach to quickly write high-assurance drivers and layers of the (IC)-C-2 stack. We do not propose a single, true formalization of (IC)-C-2, but a framework that allows rapid modelling of non-compliant devices and verify the correct interaction with a host driver process. Our contribution is twofold: First, we develop a framework that allows the specification of device and driver behavior together, and verification of their correct interaction. Second, we provide already verified, fine-grained building blocks, representing layers of the (IC)-C-2 stack that can be reused to interact with partially-compliant devices, as well as reducing model checking complexity. Our specifications are stated in a machine-readable, executable, and layered DSL. From the DSL, we generate both Promela and C code. The Promela is used to apply model checking to ensure the layer implementations follow the abstract specifications. The C code is used to build and verify an EEPROM model and driver running on a Raspberry Pi.