F. Ucman and M. Subramaniam (USA)
Monitors, Abstraction, Model checking, Protocols.
ION Frank Ucman Department of Computer Science University of Nebraska at Omaha Omaha, NE 68118 email: [email protected] Mahadevan Subramaniam Department of Computer Science University of Nebraska at Omaha Omaha, NE 68118 email:[email protected] ABSTRACT Complex monitoring environments are commonly used to check that a system implementation conforms to the prop erties in the specification of the system. Monitor state machines in these environments check conformance with respect to individual properties. A novel, automated ap proach to design monitoring environments guided by the verifiability of the environment itself is proposed. Vari ables and predicates appearing in specification properties are abstracted by boolean and bit vector variables to pro duce abstract properties. Verifiable monitor state machines whose state spaces are manageable for verification are gen erated from the abstracted properties. Rules are developed to automatically split an abstract property when the moni tor state machine produced from it is too large to be veri fied. Verifiable monitor state machines communicating the results of their checks with each other are automatically generated from split property such that these machines col lectively check the original property. To produce environ ments 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.
Important Links:
Go Back
