Beyond model checking of idealized Lustre in Kind 2

This paper describes several new features of the open-source model checker Kind 2. Its input language and model checking engines have been extended to allow users to model and reason about systems with machine integers. In addition, Kind 2 can now provide traceability information between specification and design elements, which can be used for several purposes, including assessing the quality of a system specification, tracking the safety impact of model changes, and analyzing the tolerance and resilience of a system against faults or cyber-attacks. Finally, Kind 2 is also able to check whether a component contract is realizable or not, and provide a deadlocking computation and a set of conflicting guarantees when the contract is unrealizable.