Title

Static Verification Of Ptolemyrely Programs Using Openjml

Keywords

OpenJML; Ptolemy language; PtolemyRely; Static verification

Abstract

In the PtolemyRely language event types define events that, when announced, trigger the execution of handlers, passing along the triggering piece of code for its eventual execution. Verification of PtolemyRely programs poses some particular challenges: (1) handlers must be verified against their corresponding event declaration, (2) event announcement and next-handler invocation must be reasoned about according to PtolemyRely's semantics, (3) the body of refining statements must be checked against their specifications, etc. The original Ptolemy compiler includes run-time assertion checking for dynamic verification, but there has been no static verification tool. In this paper we address the challenge of static verification of PtolemyRely programs by encoding them into JML (the Java Modelling Language) and using a JML static verification tool (Open-JML) to discharge the verification obligations. We argue informally that our encoding is sound in the sense that a PtolemyRely program is valid if and only if its encoding is a valid JML program. Copyright © 2014 ACM.

Publication Date

1-1-2014

Publication Title

FOAL 2014 - Proceedings of the 13th Workshop on Foundations of Aspect-Oriented Languages, Co-located with MODULARITY 2014 (Formerly AOSD)

Number of Pages

13-18

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1145/2588548.2588550

Socpus ID

84900024810 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/84900024810

This document is currently not available here.

Share

COinS