Shanghai Konan SmartRocket series product introduction (3): SmartRocket iVerifier computer interlocking system verification tool

Industry background

In the modern public transportation system, the rail transit system has an irreplaceable and prominent position.As the number of station signal equipment becomes larger and the station operation tasks become more and more complex, how to ensure the safe, fast and efficient operation of trains is a prominent problem facing the relevant technicians.The computer interlocking system is a very important subsystem in the railway and urban rail transit signal system. It is a typical data-driven safety-critical system. During the development process, it is necessary to verify the system behavior and confirm the safety of the data.The data is not only related to the correct realization of the computer interlocking function, but also related to the safety integrity level of the entire signal system.Traditional interlocking system development, design and testing can only guarantee the correctness of its logic from the function, but cannot guarantee that its safety requirements are completely satisfied. Ensuring that safety requirements are fully met through formal methods is the key to improving the safety of interlocking systems.SmartRocket iVerifier, as a formal verification tool of computer interlocking system with independent patent technology of Shanghai Konan, has broken the monopoly position of foreign products in the field of formal verification of computer interlocking system, and has become a guarantee for the safety of interlocking system in the field of domestic rail transit.The first formal verification tool for sex.

Product overview

SmartRocket iVerifier is a computer interlocking system verification tool used in the field of rail transit.The tool supports automatic parsing of the security requirements described by the LSpec specification language, and automatically verifies whether the requirements are established in combination with interlocking data.The tool uses a formal method for verification, so that the authenticity of each security requirement is based on strict model checking. If it proves to be false, the tool provides timing simulation and debugging functions for users to deduce the complete process of security requirements being violated.Formal verification is automatically run by tools based on general applications and specific station configurations, high execution efficiency, easy debugging, and saving a lot of labor costs.

Product Features

01Automatic Verification

Supports checking instantiated devices for one-key authentication.The verification method is simpleCAR, where verification strategy includes forward search and backward search, verification strategystrong>Verification results include Verification Passed, Verification Failed, and Verification Not OK.For devices that pass the verification, they pass the verification under any circumstances; for devices that fail to pass the verification, the tool provides counter-examples that do not meet the verification nature.verify.

02Auxiliary Counter-Example Debugging

Support to view the cycle diagram of all variables under the device that has not passed the verification. Click on a cycle to change the assignment of the variables on the BOOL logic ladder diagram, and the station diagram will also display the devices under this cycleIt supports viewing the ladder diagram and the station diagram at the same time, and supports searching and locating the equipment in the station diagram.

03Security Requirements Management

Support online import of security requirements files or add, delete, check and modify security requirements, support searching for the corresponding formal language LSpec description and natural language description according to the requirement number, support one-click parsing of security requirements, find grammatical errors through parsing, andLocate the error.

Features

01Formal Verification

The whole process adopts an automatic model checking method. This method quickly locates the state space that violates the security requirements by means of conflict guidance, and at the same time deduces the full state space from the partial search state through the abstract reduction technology.correctness, improve proof efficiency.

02 LSpecSpecification Language

Designed the LSpec specification language based on Linear temporal logic (LTL).The language combines quantifiers in predicate logic with delays in temporal logic, which can express relational properties and temporal properties, so as to unambiguously describe the safety requirements of interlocking systems.

03Visual Debugging

Supports the simulation of the station floor plan, supports the presentation of the state space that violates the safety requirements in the form of a period diagram, supports the interaction between the ladder diagram and the station yard diagram, Provide user-friendly counter-example debugging tools for testers.

04Incremental Validation

Provide an online editor of LSpec specification language, support to modify the formal security requirements according to the verification results in the development cycle, support to re-verify some modified requirements, and reduce the time cost.

Application of results

Rail Transit

SmartRocket iVerifier provides industry-leading customers with formal verification services for interlocking systems to establish sign-off safety verification in compliance with CENELEC EN 50128:2011 SIL4 level.At present, more than 1,000 formal requirements have been parsed, and more than 10,000 instances have been verified. Using this tool, the formal verification of the interlocking system of the pilot station has been realized.