Specification of Embedded Monitors for Property Checking
Allara, A. and Bombana, M. and Josko, S. Comai and B. and Schlör, R. and Sciuto, D.
Proceedings, Forum on Design Languages, FDL'99
In the formal verification domain the use of monitors represents a powerful technique where model I/O sequences are monitored and triggers are raised to allow a simplification in the construction of formal properties. This reduces the chances of incorrect system specifications and can sometimes reduce also the actual model checking time. The drawback of this technique lies in its heterogeneity. In fact, usually monitors are defined at the implementation level of the device model under test. In this paper we present a more general approach based on the idea of abstracting monitors definition from the model level up to the specification level without imposing further constraints on the current model checking techniques. A test case from the telecom domain is used to illustrate the definition and use of this type of embedded monitors, showing advantages and benefits related to their application.
01 / 1999
inproceedings
117-126
