The use of Ada PDL as the basis for validating a system specified by control flow logic

A specification for the control processes that constitute the Advanced Train Control System (ATCS) is considered. The process of validating the logic contained in those control processes is addressed. The evolution of the specifications describing the control processes in the ATCS has been from a high-level, operational view of railroad operations to a detailed logical description of a transaction-based event-response system. That process has required much functional decomposition and evaluation of design approaches. A description is given of a validation process that is feasible because the system logic exists in the compilable Ada PDL language used. In this approach, the specifications themselves become the engine for their own validation