Enabling the Runtime Assertion Checking of Concurrent Contracts for the Java']Java Modeling Language

被引：0
|
作者：
Araujo, Wladimir [1 ]
Briand, Lionel C. [2 ]
Labiche, Yvan [3 ]
机构：
[1] Juniper Networks, 700 Silver 7 Rd, Ottawa, ON K2V 1C3, Canada
[2] Univ Oslo, Simula Res Lab, N-0316 Oslo, Norway
[3] Carleton Univ, Ottawa, ON K1S 5B6, Canada
来源：
2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE) | 2011年
关键词：
Design by contract; concurrency; object-oriented programming; !text type='Java']Java[!/text; JML;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Though there exists ample support for Design by Contract (DbC) for sequential programs, applying DbC to concurrent programs presents several challenges. In previous work, we extended the Java Modeling Language (JML) with constructs to specify concurrent contracts for Java programs. We present a runtime assertion checker (RAC) for the expanded JML capable of verifying assertions for concurrent Java programs. We systematically evaluate the validity of system testing results obtained via runtime assertion checking using actual concurrent and functional faults on a highly concurrent industrial system from the telecommunications domain.
引用
收藏
页码：786 / 795
页数：10
相关论文
共 34 条
  • [1] Implementing Java']Java Modeling Language Contracts with AspectJ
    Rebelo, Henrique
    Lima, Ricardo
    Cornelio, Marcio
    Soares, Sergio
    Ferreira, Leopoldo
    APPLIED COMPUTING 2008, VOLS 1-3, 2008, : 228 - 233
  • [2] Checking and Correcting Behaviors of Java']Java Programs at Runtime with Java']Java-MOP
    Chen, Feng
    d'Amorim, Marcelo
    Rosu, Grigore
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (04) : 3 - 20
  • [3] Faster and More Complete Extended Static Checking for the Java']Java Modeling Language
    James, Perry R.
    Chalin, Patrice
    JOURNAL OF AUTOMATED REASONING, 2010, 44 (1-2) : 145 - 174
  • [4] Using runtime analysis to guide model checking of Java']Java programs
    Havelund, K
    SPIN MODEL CHECKING AND SOFTWARE VERIFICATON, 2000, 1885 : 245 - 264
  • [5] Model Checking of Concurrent Algorithms: From Java']Java to C
    Artho, Cyrille
    Hagiya, Masami
    Leungwattanakit, Watcharin
    Tanabe, Yoshinori
    Yamamoto, Mitsuharu
    DISTRIBUTED, PARALLEL AND BIOLOGICALLY INSPIRED SYSTEMS, 2010, 329 : 90 - +
  • [6] Concurrent programming in Java']Java: Language and libraries
    Holmes, D
    TECHNOLOGY OF OBJECT-ORIENTED LANGUAGES AND SYSTEMS (TOOLS 25) - PROCEEDINGS, 1998, : 371 - 371
  • [7] Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems
    Din, Crystal Chang
    Owe, Olaf
    Bubel, Richard
    PROCEEDINGS OF THE 2014 2ND INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT (MODELSWARD 2014), 2014, : 480 - 487
  • [8] JCML: A specification language for the runtime verification of Java']Java Card programs
    da Costa, Umberto Souza
    Moreira, Anamaria Martins
    Musicante, Martin A.
    Souza Neto, Placid A.
    SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (04) : 533 - 550
  • [9] SeSFJava']Java harness: Service and assertion checking for protocol implementations
    Elsharnouby, T
    Shankar, AU
    IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS, 2004, 22 (10) : 2035 - 2047
  • [10] A framework for model checking concurrent Java components
    School of Maths, Physics and Information Technology, James Cook University , Australia
    J. Softw., 2009, 8 (867-874):
1234