Concurrent contracts for java in JML

Wladimir Araujo, Lionel Briand, Yvan Labiche

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Design by Contract (DbC) is a software development methodology that makes use of assertions to produce better quality object-oriented software. The idea behind DbC is that a method defines a contract stating the requirements a client needs to fulfill to use it, the precondition, and the properties it ensures after its execution, the postcondition. Though there exists ample support for DbC for sequential programs, applying DbC to concurrent programs presents several challenges. The first challenge is interference, the product of multiple threads of execution modifying and accessing shared data. The second is the specification of thread-safety properties in the presence of inheritance. We present a solution to these challenges in the context of Java programs by extending the Java Modeling Language (JML) specification language. We experiment our solution on a large size industrial software system.

Original languageEnglish
Title of host publicationProceedings - 19th International Symposium on Software Reliability Engineering, ISSRE 2008
Pages37-46
Number of pages10
DOIs
Publication statusPublished - 2008
Externally publishedYes
Event19th International Symposium on Software Reliability Engineering, ISSRE 2008 - Seattle, WA, United States
Duration: 10 Nov 200814 Nov 2008

Publication series

NameProceedings - International Symposium on Software Reliability Engineering, ISSRE
ISSN (Print)1071-9458

Conference

Conference19th International Symposium on Software Reliability Engineering, ISSRE 2008
Country/TerritoryUnited States
CitySeattle, WA
Period10/11/0814/11/08

Fingerprint

Dive into the research topics of 'Concurrent contracts for java in JML'. Together they form a unique fingerprint.

Cite this