Formal Specification Language for Control & Signaling Applications
PiSPEC is a formal language dedicated for control and signaling engineering. It enables you to specify application design, and test and safety requirements. A unique feature in PiSPEC is that it enables you to create application-independent Generic Specifications. These specifications can then be used to automatically generate Application Specifications from Application Configurations (defining track layout, zoning and layout of signals and switches). PiSPEC is used to develop three types of formal specifications:
Generic Safety Specifications
These specifications define safety requirements for applications. For example, a safety requirement can state that two opposing signals shall never show proceed aspects at the same time, regardless of application inputs.
Generic Test Specifications
These specifications define functional requirements for applications. For example, a test requirement may state that a route lock for a track circuit should unlock within 5 seconds after a train has vacated the track of the route.
Generic Design Specifications
These specifications define application design details and equations for all system functions, including route locks, speed indications, display of signal aspects and requests and indications.
-
FeaturePurpose
-
Typed Predicate LogicCreate generic specifications (application-independent) to enable reuse
-
Object orientation (using classes), inheritance (a class may inherit a more general class in order to provide more specialized behavior), encapsulation (defining the interface, hiding irrelevant detail), name spaces (enabling definition of library specifications that are reused)Structure specifications and allow for high degree of reuse
-
State machines, function blocks, equationsDefine data flow, requirements and formulas
-
Boolean, integer, timer and a variety of other data typesSupport a wide variety of application types (interlocking, CBTC, etc) for multiple hardware targets and their executive software
