|
Why write monitors?
Why write monitors?
- Some properties are hard or impossible to express in CTL. Example: Store -Load order. Let X be a memory location. “If load_req X follows store_req X , then the store must be serviced before the load.”
- Undesired behavior: store_req X . . . load_req X . . . load_service X . . .
- Note: In the initial state, we non-deterministically start checking for the bad sequence. Undesired behavior can be detected anywhere along the trace.
|
