Proving Properties of Rich Internet Applications

James Smith

We introduce application layer specifications, which allow us to reason about the state and transactions of rich Internet applications. We define variants of the state/event based logic UCTL* along with two example applications to demonstrate this approach, and then look at a distributed, rich Internet application, proving properties about the information it stores and disseminates. Our approach enables us to justify proofs about abstract properties that are preserved in the face of concurrent, networked inputs by proofs about concrete properties in an Internet setting. We conclude that our approach makes it possible to reason about the programs and protocols that comprise the Internet's application layer with reliability and generality.

In António Ravara and Josep Silva: Proceedings 9th International Workshop on Automated Specification and Verification of Web Systems (WWV 2013), Florence, Italy, 6th June 2013, Electronic Proceedings in Theoretical Computer Science 123, pp. 49–63.
Published: 31st July 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: