Abstract

Proving the correctness is important to ensure faultless functionality. To prove the correctness of Active Object programs in Java, this research translates them to message passing programs. Active Object are not a build-in feature of the Java programming language. For asynchronous method calls, we used the Java Future interface to return result values. We created a formal specification for the Java Future interface and proved a simple implementation correct using the VerCors tool set. We implemented the communication to Active Objects using message passing with the MPJ Express library. To verify this implementation, the message passing library has been annotated and a definition of valid messages in this program is given. We also annotated our implementation, however we encountered problems annotating the returning of result values. The annotations require a lot of administrative overhead and are hard to get correct. Also the existing VerCors tool set is not capable yet to automatically verify the program, mainly because it lacks support for output parameters or sum notation in the process algebra for futures.

Additional Resources

1. The paper
2. Source codes