Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Checking JML Specifications Using An Extensible Software Model Checking Framework ⋆
Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Checking JML Specifications Using An Extensible Software Model Checking Framework ⋆
复制标题
技术转让软件工具手稿编号（将由编辑插入）使用可扩展软件模型检查框架检查 JML 规范⋆
DOI：
10.1007/s10009-005-0218-5
复制
发表时间：
2006
影响因子：
1.5
通讯作者：
Carlo A. Furia
中科院分区：
文献类型：
--
作者：
N. Polikarpova;Julian Tschannen;Carlo A. Furia
使用断言来表示程序的正确性属性在实践中越来越多。断言提供了一种轻量级的可检查规范，可以非常有效地发现程序中的缺陷，并引导开发人员找到问题的原因。已经开发了各种各样的断言语言和相关的验证技术，但运行时监视通常被认为是唯一实用的解决方案。在本文中，我们描述了如何规范编写的Java建模语言（JML），通用的行为规范和断言语言的Java，可以使用自定义的模型检查器上建立的博戈尔模型检查框架进行验证。我们的经验表明，需要定制的状态空间表示和减少策略的模型检查框架，以有效地检查的那种强大的行为规范，可以写在JML。我们讨论的优势和权衡模型检查相对于其他规范验证技术和目前的数据表明，模型检查强规格的成本是实际的几个真实的程序。
The use of assertions to express correctness properties of programs is growing in practice. Assertions provide a form of lightweight checkable specification that can be very effective in finding defects in programs and in guiding developers to the cause of a problem. A wide variety of assertion languages and associated validation techniques have been developed, but run-time monitoring is commonly thought to be the only practical solution. In this paper, we describe how specifications written in the Java Modeling Language (JML), a general purpose behavioral specification and assertional language for Java, can be validated using a customized model checker built on top of the Bogor model checking framework. Our experience illustrates the need for customized state-space representations and reduction strategies in model checking frameworks in order to effectively check the kind of strong behavioral specifications that can be written in JML. We discuss the advantages and tradeoffs of model checking relative to other specification validation techniques and present data that suggest that the cost of model checking strong specifications is practical for several real programs.