Proving Properties of Rich Internet Applications

TL;DR

This paper presents a novel approach using application layer specifications and logic variants to reason about and prove properties of rich Internet applications, ensuring reliability amidst concurrency and networked inputs.

Contribution

It introduces application layer specifications and logic variants for reasoning about Internet applications, demonstrated through example applications and property proofs.

Findings

Able to prove properties of distributed Internet applications

Ensures correctness despite concurrent network inputs

Provides a reliable reasoning framework for application layer protocols

Abstract

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.