Validation-directed specification of communications systems

Considerable interest has recently developed in industry in the concepts of life-cycle testing and concurrent engineering. A key component in these concepts is advance planning and preparation for validation activities (primarily testing and verification activities). In this paper, we introduce a new, testability-directed specification method, namely ETAL (Extended Trace Assertion Language) with relative clocks. This method extends and applies work by Parnas on formal specification of software requirements by trace assertions and work by Lamport on logical clocks in distributed systems. As a result, we derive a practical model for specifying and analysing global events with a view towards verification and testing. We give an example of the application of this approach to derive a testability-directed specification of a communications service provider, and illustrate how the approach facilitates conformance test results analysis.