Treffer: Enabling the runtime assertion checking of concurrent contracts for the Java modeling language.

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. [ABSTRACT FROM AUTHOR]

Copyright of ICSE: International Conference on Software Engineering is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)