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. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||