University of Twente Student Theses


Reasoning about Active Object Programs

Zeilstra, J. (2016) Reasoning about Active Object Programs.

[img] PDF
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.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page