Journal article
Beyond model checking of idealized Lustre in Kind 2
ACM SIGAda Ada Letters, Vol.42(2), pp.40-44
04/05/2023
DOI: 10.1145/3591335.3591338
Abstract
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.
Details
- Title: Subtitle
- Beyond model checking of idealized Lustre in Kind 2
- Creators
- Daniel Larraz - University of IowaArjun Viswanathan - University of IowaCesare Tinelli - University of IowaMickaël Laurent - Institut de Recherche en Informatique Fondamentale
- Resource Type
- Journal article
- Publication Details
- ACM SIGAda Ada Letters, Vol.42(2), pp.40-44
- DOI
- 10.1145/3591335.3591338
- ISSN
- 1094-3641
- eISSN
- 1557-9476
- Language
- English
- Date published
- 04/05/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984411062202771
Metrics
85 Record Views