Specification, Coding, Simulation and Formal Verification of Control and Signaling Applications

The Prover Process is based on the PiSPEC and Prover iLock solutions. It covers specification, coding, simulation and formal verification of control and signaling applications. The diagram below illustrates the engineering savings from the Prover Process compared to a non-formal traditional process. There is an up-front effort associated with creating the PiSPEC libraries, but after that the engineering is highly automated. The result: dramatic cost savings.

The up-front cost shown in the chart comes from gathering the signaling know-how and capturing it using the unambiguous, formal and proven PiSPEC language. This exercise forces engineers to resolve ambiguities and inconsistencies in existing signaling documentation, once and for all. This in turn frees up valuable engineering resources, ensures crystal clear requirements, and enables highly automated application engineering down the road. While people may leave or retire, the PiSPEC libraries will remain, ensuring that new staff can be brought up to speed quickly.

The diagram below gives an overview of the development process. The individual steps are covered in more detail below.

Step 1: Safety and Test Specification using PiSPEC

The first step in an application engineering process is requirements specification. For control and signaling systems, there are two categories of logic requirements.

• Test requirements: test scenarios expressed in terms of inputs and expected outputs
• Safety requirements: Forbidden or unsafe states

Before these requirements are clearly defined, an engineer cannot design a quality application. In a traditional process, these requirements can be split into two categories: explicit and implicit requirements. The explicit requirements are captured in various non-formal natural language documents. These documents are typically inconsistent and ambiguous. The implicit requirements are undocumented, and part of an organization’s “tribal knowledge”. These requirements typically differ depending on whom you ask. The result: projects deliver inconsistent results, exceed budgeted costs, and fail to meet (unclear) customer expectations.

This problem is resolved by creating Generic Test and Safety Specifications using PiSPEC. The Generic Test and Safety Specifications are then provided to the engineers responsible of application design, ensuring that the design process starts with a crystal clear picture of the requirements.

Step 2: Design Specification using PiSPEC

PiSPEC is also used to specify design and implementation details in a Generic Design Specification. The Generic Design Specification enables suppliers to automate coding. This in turn ensures 100% consistently coded applications that do not suffer from individual algorithmic, structural and naming preferences.

Step 3: Coding and Simulation using Prover iLock

Once the design rules have been captured in the Design Specification, not a single line of code needs to be written by hand. An application engineer instead uses Prover iLock to generate the code. The process is rapid and accurate. All the engineer needs to do is to draw a graphical track plan in Prover iLock, set some parameters, and the tool then generates and simulates the Application Code.

Step 4: Safety Verification using Prover iLock

Testing is a suitable method for establishing that a system copes with the expected operational scenarios. It is NOT suitable for safety verification. It is incomplete, and hence by definition risky to rely on. Formal safety verification on the other hand is an approach that verifies that the Application Code will never enter an unsafe or forbidden state, for ANY scenario. This enables elimination of all unsafe logic. For this reason, formal verification is strongly recommended by standards (such as CENELEC) and required by several leading operators.

Prover iLock Verifier seeks out input scenarios that will cause the Application Code to enter an unsafe/forbidden state and displays them graphically. This ensures that you detect and fix logic problems that may cause accidents prior to revenue service.