Using X-Machines to Model and Test Discrete Event Simulation Programs.

E.Kehris, G.Eleftherakis, and P. Kefalas

Abstract: Simulation is a powerful technique for the study of real-life complex problems. Simulation requires the development of a program, which mimics the problem under consideration. The simulation program development follows closely the software engineering process. Although, many techniques for modelling problems have been proposed, the testing phase of the developed programs has been under-discussed. In this paper, we introduce an alternative framework for modelling and simulation, which will facilitate the phases of the conceptual modelling and the verification of the software. X-machines is a formal technique which extends the Finite State Machines by introducing memory attached to the machine and functions that operate on input symbols and memory values. This is shown to be a powerful model, subsuming other well-known models, since not only the specification of a problem is done in an intuitive manner but also because the method is used to prove that the implementation is correct with respect to the specification.  A simple example is thoroughly investigated in terms of modelling and testing by employing the X-machine formal methodology. A complete set of test-cases is generated and applied in the code which is written in a conventional programming language. It is demonstrated that faults are found in the implementation by comparing the output sequences to those intended by the specification. Finally, a discussion is made in order to propose further course of research in this area, which would add the necessary characteristics in the X-machine theory in order to serve modelling and simulation development to its full extent.

Keywords: Formal specification, Testing, Simulation, Verification

Appeared in: In Proceedings of the 4th World MultiConference on Circuits, Systems, Communications & Computers (CSCC 2000), Athens, July 2000

Available: Hardcopy on request from the authors.

Back to Dept. of Computer Science, CITY Liberal Studies

Back to Petros Kefalas home page