English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Developing interactive applications (apps) against event-driven softwareframeworks such as Android is notoriously difficult. To create apps that behaveas expected, developers must follow complex and often implicit asynchronousprogramming protocols. Such protocols intertwine the proper registering ofcallbacks to receive control from the framework with appropriateapplication-programming interface (API) calls that in turn affect the set ofpossible future callbacks. An app violates the protocol when, for example, itcalls a particular API method in a state of the framework where such a call isinvalid. What makes automated reasoning hard in this domain is largely whatmakes programming apps against such frameworks hard: the specification of theprotocol is unclear, and the control flow is complex, asynchronous, andhigher-order. In this paper, we tackle the problem of specifying and modelingevent-driven application-programming protocols. In particular, we formalize acore meta-model that captures the dialogue between event-driven frameworks andapplication callbacks. Based on this meta-model, we define a language calledlifestate that permits precise and formal descriptions ofapplication-programming protocols and the callback control flow imposed by theevent-driven framework. Lifestate unifies modeling what app callbacks canexpect of the framework with specifying rules the app must respect when callinginto the framework. In this way, we effectively combine lifecycle constraintsand typestate rules. To evaluate the effectiveness of lifestate modeling, weprovide a dynamic verification algorithm that takes as input a trace ofexecution of an app and a lifestate protocol specification to either produce atrace witnessing a protocol violation or a proof that no such trace isrealizable.

Lifestate: Event-Driven Protocols and Callback Control Flow (Extended Version)