Linux Driver Verification

IMHO, at the moment rather bad way is used to "wake up" rule models in accordance with events in the environment model. I suggest following common interface for that:

• (The most adequate among others) ldv_initialize and ldv_check_final_state functions can be simply replaced with the named pointcut ENTRY_POINT which is "execution/definition($ entry_point(..))" (wildcards are likely to be replaced with actual types since they are known). Then ldv_initialize is "before: ENTRY_POINT" while ldv_check_final_state is "after: ENTRY_POINT".
• Interrupts are triggered by setting flag IN_INTERRUPT (or something similar). Like above, this can be replaced with the named pointcut INTERRUPT which is "call($ handler1(..)) || call($ handler2(..)) || ..." (the same with wildcards). The same things with tasklets, timers, completions, usb_fill_bulks, and so on.
• Other interesting handlers are additionally processed with something like calling check_probe_ret_val function. Obviously we have after recommendations for this. They will work if DEG will provide appropriate named pointcuts, like "PROBE: call($ usb_probe(..))" and so on.
• Whatever possible can be triggered in the similar way.