A comparison of two different model checking techniques

[摘要] ENGLISH ABSTRACT:Model checking is a computer-aided verification technique that is used to verify propertiesabout the formal description of a system automatically. This technique has been appliedsuccessfully to detect subtle errors in reactive systems. Such errors are extremely difficult todetect by using traditional testing techniques. The conventional method of applying modelchecking is to construct a model manually either before or after the implementation of asystem. Constructing such a model requires time, skill and experience. An alternative methodis to derive a model from an implementation automatically.In this thesis two techniques of applying model checking to reactive systems are compared,both of which have problems as well as advantages. Two specific strategies are compared inthe area of protocol development:1. Structuring a protocol as a transition system, modelling the system, and then derivingan implementation from the model.2. Automatically translating implementation code to a verifiable model.Structuring a reactive system as a transition system makes it possible to verify the control flowof the system at implementation level-as opposed to verifying the control flow at abstractlevel. The result is a closer correspondence between implementation and specification (model).At the same time testing, which is restricted to small, independent code fragments thatmanipulate data, is simplified significantly.The construction of a model often takes too long; therefore, verification results may no longerbe applicable when they become available. To address this problem, the technique of automatedmodel extraction was suggested. This technique aims to reduce the time required toconstruct a model by minimising manual input during model construction.A transition system is a low-level formalism and direct execution through interpretation isfeasible. However, the overhead of interpretation is the major disadvantage of this technique.With automated model extraction there are disadvantages too. For example, differencesbetween the implementation and specification languages-such as constructs present in theimplementation language that cannot be expressed in the modelling language-make thedevelopment of an automated model extraction tool extremely difficult.In conclusion, the two techniques are compared against a set of software development considerations.Since a specific technique is not always preferable, guidelines are proposed to helpselect the best approach in different circumstances.

[发布机构] Stellenbosch University