使用KeY对OpenJDK部分API进行形式化验证的经验报告
编程语言
2018-11-28 v1 计算机科学中的逻辑
软件工程
摘要
软件的演绎验证尚未进入工业界，因为复杂性与可扩展性问题需要高度专业化的专家。然而，长远来看是开发验证工具，以帮助工业软件开发人员更快、更容易地发现软件系统中的错误或瓶颈。KeY项目构成了一个用于规约和验证软件系统的框架，旨在使形式化验证工具适用于主流软件开发。为了帮助KeY的开发者、其用户以及演绎验证社区，我们从用户视角总结了使用KeY 2.6.1对来自现实世界的Java代码进行规约与验证的经验。为此，我们聚焦于OpenJDK 6的Collections-API的部分内容，其存在非形式化规约。在描述我们如何桥接非形式化与形式化规约的同时，我们也展示了伴随而来的挑战。我们的经验是：（a）原则上，针对类API代码库的演绎验证是可行的，但需要高度专业知识；（b）为现有代码库开发形式化规约仍然极其困难；（c）Java中某些语言构造的欠规约对工具构建者而言具有挑战性。我们在规约OpenJDK 6部分内容上的初步努力，构成了面向未来研究案例研究的垫脚石。
引用
@article{arxiv.1811.10818,
title = {Experience Report on Formally Verifying Parts of OpenJDK's API with KeY},
author = {Alexander Knüppel and Thomas Thüm and Carsten Pardylla and Ina Schaefer},
journal= {arXiv preprint arXiv:1811.10818},
year = {2018}
}
备注
In Proceedings F-IDE 2018, arXiv:1811.09014