NKind: a model checker for liveness property verification on Lustre programs

Modeling and verification of real-time reactive systems is getting greater concern in industrial field, especially in safety-critical applications. As a representative language for modeling real-time reactive systems, Lustre has been extensively used in the development of control systems in vehicles and aircraft. Existing model checking tools for Lustre like Kind2 and JKind have good support for verifying safety properties, but they lack explicit support for liveness properties. Thus we present NKind, an SMT-based infinite-state model checker, which accepts models and properties written in Lustre and is capable of verifying both safety and liveness properties. NKind is inspired by many existing model checker and adds liveness support based on their common techniques, which provides more flexibility. It is written in Java, providing good compatibility, and lays emphasis on modularity and extensibility. The results and performance of NKind on benchmark examples demonstrate that it is competitive comparing to other existing tools.