Designing monitoring environments for verifiability using abstraction

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 10th IASTED International Conference on Software Engineering and Applications, SEA 2006
Pages45-50
Number of pages6
StatePublished - 2006
Event10th IASTED International Conference on Software Engineering and Applications, SEA 2006 - Dallas, TX, United States
Duration: Nov 13 2006Nov 15 2006

Publication series

NameProceedings of the 10th IASTED International Conference on Software Engineering and Applications, SEA 2006

Conference

Conference10th IASTED International Conference on Software Engineering and Applications, SEA 2006
CountryUnited States
CityDallas, TX
Period11/13/0611/15/06

Keywords

  • Abstraction
  • Model checking
  • Monitors
  • Protocols

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Designing monitoring environments for verifiability using abstraction'. Together they form a unique fingerprint.

Cite this