Modelling Java concurrency with Object-Z

In this paper, we present a formal model of Java concurrency using the Object-Z specification language. This model captures the Java thread synchronization 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.

Incremental derivation of abstraction relations for data refinements

Data refinements are refinement steps in which a program’s local data structures are changed. Data refinement proof obligations require the software designer to find an abstraction relation that relates the states of the original and new program. In this paper we describe an algorithm that helps a designer find an abstraction relation for a proposed refinement. Given sufficient time and space, the algorithm can find a minimal abstraction relation, and thus show that the refinement holds. As it executes, the algorithm displays mappings that cannot be in any abstraction relation. When the algorithm is not given sufficient resources to terminate, these mappings can help the designer find a suitable abstraction relation. The same algorithm can be used to test an abstraction relation supplied by the designer.

Developing relational navigation to effectively understand software

Effective comprehension of complex software systems requires understanding of both the individual documents that represent software and the complex relationships that exist within and between documents. Relationships of all kinds play a vital role in a software engineer's comprehension of, and navigation within and between, software documents. User-determined relationships have the additional role of enabling the engineer to create and maintain relational documentation that cannot be generated by tools or derived from other relationships. We argue that for a software development environment to effectively support the understanding of complex software systems, relational navigation must be supported at both the document-focused (intra-document) and relation-focused (inter-document) levels. The need for a relation-focused approach is highlighted by an evaluation of an existing document-focused relational interface. We conclude with the requirements for a relation-focused approach to relational navigation. These requirements focus on the user's perspective when interacting with a collection of related documents. We define the requirements for a software development environment that effectively supports the understanding of the software documents and relationships that define a complex software system.