Incremental verification methodology for DEVS models
Wan Bok Lee, Changhyun Roh · International Conference on Signal Processing · 2005
Systems design has been an iterative process which involves several steps such as modelling, logical analysis, performance evaluation and implementation. If each step requires different model, it would be a major hurdle to a seamless design process. Therefore a unified modelling framework which provides a basis to specify models at different steps in common semantics is desirable. In our methodology, an implementation model is reduced to an observational equivalent model through a series of stepwise compositions and minimizations. This incremental approach alleviates the state explosion problem in a verification process. Once a final operational CDEVS model is obtained, it can be verified by an equivalence checking algorithm. The proposed approach is much promising when analyzing large systems. If a component should be changed due to a design error, the overall composed model can be rebuilt by just composing the changed model with the unchanged ones together. An example of development of alternating bit protocol within the framework demonstrates effectiveness of the methodology.