Using X-Machines to Model and Test Discrete Event Simulation
Programs.
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