SmartRocket iVerifier

Product overview

SmartRocket iVerifier is the country's first iLOCK type computer interlocking system verification tool that automatically validates all security requirements formally. In addition, it will give a counter example if the verification fails, and the counter case will be presented on the corresponding model diagram and periodic diagram for the user to deduce the complete process of the nature being violated. In addition to the core validation capabilities, SmartRocket iVerifier has requirements management, model management, and user management capabilities. SmartRocket iVerifier is a complete product.


  • Requirements management

    Supports adding, deleting and modifying properties to be validated

  • Model management

    Variables in system design can generate models automatically

  • Automatic validation

  • Counterexample traceability

    Validation failures provide a counterexample cycle diagram and are traceable

Value advantage

  • Automatic function

    Users only need to click the upload button input to verify safety requirements documents and to verify the system design document, and then click the verify button one-click automatically according to the requirements of security authentication system design, the final results of automatic classification for authentication, verification is not by and by successfully passed the security requirements of three of the following is derived.

  • Full coverage

    The core function of the tool -- verification function is the formal verification method adopted. The formal verification method USES mathematical proof to ensure that the system meets the requirements. The authenticity conclusion of each attribute is based on strict mathematical proof.

  • Provide counter examples

    Click to select each rail transit equipment that fails to verify the safety requirements. The tool will not only provide the verification results of the specific cycle of the equipment (until the last cycle with a counter example), but also provide the logical relationship model diagram of the equipment for the user to click on the equipment associated equipment for tracing.

  • High performance

    Based on the kernel of formal verification method based on model inspection, even for large interlocking system, this tool only needs a little time to carry out complete security verification. Rapid verification can quickly find system design errors and correct them, thus achieving a virtuous cycle and greatly shortening the cycle of system design.

  • Large capacity

    The kernel verification function of this tool adopts the formal verification method based on model inspection. The model inspection technology has been proved to be used in avionics, electronic design automation and other industries, that is, it can verify the very large system, and our tool can also verify the very large interlocking system.

Typical applications

  • Rail traffic