First International Conference on Software Engineering and Formal Methods (SEFM'03)
Modelling Java Concurrency with Object-Z
Brisbane, Australia
September 22-September 27
ISBN: 0-7695-1949-0
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.
Citation:
Roger Duke, Luke Wildman, Brad Long, "Modelling Java Concurrency with Object-Z," sefm, pp.173, First International Conference on Software Engineering and Formal Methods (SEFM'03), 2003
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||