Composition-based verification methodology for discrete event systems

Abstract

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 this thesis we propose a new composition-based verification methodology for the DEVS (Discrete EVent Systems specification) models. The suggested composition-based technique is applicable not only to the formal verification area but also to the area of simulation-based verification. Therefore it provides an axis of a unified framework based on the DEVS formalism. For the formal verification of discrete event systems we defined the CDEVS (Communicating Discrete Event Systems) formalism which is an extended version of the DEVS formalism providing the nondeterministic representation of a system. As a means of a systematic proof technique, two operations, namly composition and minimization, are defined. These operations are compatible with the meaning of the communication semantics of the DEVS models, thus they incorporate the feature of spontaneity of output events in an 10 (Input/Output) system. 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 either by an equivalence checking algorithm or by a valid implementation relationship which investigates both the functional correctness and the timeliness property. 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 unchange...