首页> 外文会议>European Conference on Object-Oriented Programming(ECOOP 2005); 20050725-29; Glasgow(GB) >Extending JML for Modular Specification and Verification of Multi-threaded Programs
【24h】

Extending JML for Modular Specification and Verification of Multi-threaded Programs

机译:扩展JML以进行模块化规范和多线程程序的验证

获取原文
获取原文并翻译 | 示例

摘要

The Java Modeling Language (JML) is a formal specification language for Java that allows developers to specify rich software contracts for interfaces and classes, using pre- and postconditions and invariants. Although JML has been widely studied and has robust tool support based on a variety of automated verification technologies, it shares a problem with many similar object-oriented specification languages—it currently only deals with sequential programs. In this paper, we extend JML to allow for effective specification of multi-threaded Java programs. The new constructs rely on the non-interference notion of method atomicity, and allow developers to specify locking and other non-interference properties of methods. Atomicity enables effective specification of method pre- and postconditions and supports Hoare-style modular reasoning about methods. Thus the new constructs mesh well with JML's existing features. We validate the specification language design by specifying the behavior of a number of complex Java classes designed for use in multi-threaded programs. We also demonstrate that it is amenable to automated verification using model checking technology.
机译:Java Modeling Language(JML)是Java的一种正式规范语言,允许开发人员使用前置条件和后置条件以及不变式为接口和类指定丰富的软件协定。尽管已经广泛研究了JML,并且基于各种自动验证技术提供了强大的工具支持,但是JML与许多类似的面向对象的规范语言都存在一个问题-当前仅处理顺序程序。在本文中,我们扩展了JML以允许有效规范多线程Java程序。新构造依赖于方法原子性的无干扰概念,并允许开发人员指定方法的锁定和其他无干扰属性。原子性可以有效地指定方法的前提条件和后置条件,并支持有关方法的Hoare式模块化推理。因此,新构造与JML的现有功能很好地结合在一起。我们通过指定许多设计用于多线程程序的复杂Java类的行为来验证规范语言的设计。我们还证明了它适合使用模型检查技术进行自动验证。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号