K. Chang and D. Kung (USA)
model checking, Promela specification language, state-based system verification
Although model checking is a practical and powerful technique for verifying the behavioral aspect of a system, it may suffer state-space explosion problem during system verification. Beside those methods that reduce or decom pose state space to have a more efficient way to save space, we have found that the style of specifying a system also has a great impact on the size of space to store states. In this paper, we have proposed an efficient way to specify a state-based system with Promela specification language. A patient-monitoring example is taken to show that our method has a great improvement in space saving and per formance, compared with the specification method inher ent in Promela language.
Important Links:
Go Back
