Designing monitoring environments for verifiability using abstraction

Complex monitoring environments are commonly used to check that a system implementation conforms to the properties in the specification of the system. Monitor state machines in these environments check conformance with respect to individual properties. A novel, automated approach to design monitoring environments guided by the verifiability of the environment itself is proposed. Variables and predicates appearing in specification properties are abstracted by boolean and bit vector variables to produce abstract properties. Verifiable monitor state machines whose state spaces are manageable for verification are generated from the abstracted properties. Rules are developed to automatically split an abstract property when the monitor state machine produced from it is too large to be verified. Verifiable monitor state machines communicating the results of their checks with each other are automatically generated from split property such that these machines collectively check the original property. To produce environments with a manageable number of verifiable monitors, a method that combines verifiable monitors by automatically computing a least refinement of abstractions is described. The proposed approach has been successfully applied to an Infiniband I/O switch and generates a verifiable monitoring environment with four communicating monitors that check conformance with over a hundred specification properties.