ABSTRACT
This chapter describes the semi-formal techniques of discrete event simulation and timed Petri nets. These techniques are not independent and can be seen as different languages for expressing the same simulation. Ideally, a design is verified as it is produced; once some of the design decisions have been made, those decisions can be verified to confirm that they meet the system’s requirements. The most obvious case for creating a design retrospectively is where an existing product, developed to a lower standard, needs to be validated for use in a safety-critical system, and where the original design was inadequately recorded or has been lost. Each safety requirement can be traced through the architecture and design, and each facet of the design can be traced back to a requirement. Numbers that are truly random are both hard to generate and difficult to use because they make it impossible to run the same simulation twice for debugging or comparison purposes.
