李钦副教授成果获SEKE2022国际会议最佳论文奖

作为保证软件符合预期需求的重要手段之一，模型检查技术在现代系统，尤其是反应式实时系统的开发与验证中显得越发重要，被证明是对软件质量的有效且重要的保障手段。在围绕该类系统的典型建模语言Lustre的模型检测研究中，往往只考虑了安全性性质的验证，而忽略了对活性性质的验证，因此对其在涉及活性性质的协议验证等领域的应用造成了一定的限制。

为了解决这一问题，实验室李钦副教授团队设计并实验实现了一种模型检查工具，对Lustre语言的活性性质验证提供了支持。该工具采用多个验证算法引擎并行执行的结构，并将无限状态活性算法整合到验证框架中，从而填补了在该领域的空白。

这项研究成果在7月1日以“NKind: a model checker for liveness property verification on Lustre programs” 为题发表于国际会议 International Conference on Software Engineering and Knowledge Engineering (SEKE 2022)，并获得会议最佳论文奖。