University of Twente Student Theses
Reasoning about Active Object Programs
Zeilstra, J. (2016) Reasoning about Active Object Programs.
|
PDF
460kB |
| 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: | https://purl.utwente.nl/essays/71180 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page