|
Published Articles >> Table of Contents >> Abstract
First International Conference on Software Engineering and Formal Methods (SEFM'03)
p. 173
Modelling Java Concurrency with Object-Z
Roger Duke, University of Queensland
Luke Wildman, University of Queensland
Brad Long, University of Queensland
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2003.1236219
Send link to a friend
| Abstract |
|
In this paper we present a formal model of Java concurrency using the Object-Z specification language. This model captures the Java thread synchronisation concepts of locking, blocking, waiting and notification. In the model we take a viewpoints approach, first capturing the role of the objects and threads, and then taking a system view where we capture the way the objects and threads cooperate and communicate. As a simple illustration of how the model can in general be applied, we use Object-Z inheritance to integrate the model with the classical producer-consumer system to create a specification directly incorporating the Java concurrency constructs.
|
 Additional Information
|
Citation:
Roger Duke, Luke Wildman, Brad Long,
"Modelling Java Concurrency with Object-Z,"
sefm,
p. 173,
First International Conference on Software Engineering and Formal Methods (SEFM'03),
2003
|
|
