Search Results

Documents authored by Mover, Sergio

Document
Artifact
DOI: 10.4230/DARTS.5.2.13
Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact)

Authors: Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.
Cite as

Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{meier_et_al:DARTS.5.2.13,
  author =	{Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
  title =	{{Lifestate: Event-Driven Protocols and Callback Control Flow}},
  pages =	{13:1--13:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.13},
  URN =		{urn:nbn:de:0030-drops-107902},
  doi =		{10.4230/DARTS.5.2.13},
  annote =	{Keywords: domain-specific languages, event-based programming, language implementation, new programming models or languages, object-oriented programming, semantics, testing, verification, automated}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2019.1
Lifestate: Event-Driven Protocols and Callback Control Flow

Authors: Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.
Cite as

Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 1:1-1:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{meier_et_al:LIPIcs.ECOOP.2019.1,
  author =	{Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
  title =	{{Lifestate: Event-Driven Protocols and Callback Control Flow}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{1:1--1:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.1},
  URN =		{urn:nbn:de:0030-drops-107932},
  doi =		{10.4230/LIPIcs.ECOOP.2019.1},
  annote =	{Keywords: event-driven systems, application-programming protocols, application framework interfaces, callbacks, sound framework modeling, predictive dynamic verification}
}
Document
Informal Presentation
DOI: 10.4230/OASIcs.SynCoP.2015.106
Parameter Synthesis with IC3 (Informal Presentation)

Authors: Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Parametric systems arise in many application domains, from real-time systems to software to cyber-physical systems. Parameters are fundamental to model unknown quantities at design time and allow a designer to explore different instantiation of the system (i.e. every parameter valuation induces a different system), during the early development phases. A key challenge is to automatically synthesize all the parameter valuations for which the system satisfies some properties. In this talk we focus on the parameter synthesis problem for infinite-state transition systems and invariant properties. We describe the synthesis algorithm Param IC3, which is based on IC3, one of the major recent breakthroughs in SAT-based model checking, and lately extended to the SMT case. The algorithm follows a general approach that first builds the set of "bad" parameter valuations and then obtain the set of "good" valuations by complement. The approach enumerates the counterexamples that violate the property, extracting from each counterexample a region of bad parameter valuations, existentially quantifying the state variables. ParamIC3 follows the same principles, but it overcomes some limitations of the previous approach by exploiting the IC3 features. First, IC3 may find a set of counterexamples s_o, ..., s_k, where each state in s_i is guaranteed to reach some of the bad states in s_k in k-i steps; this is exploited to apply the expensive quantifier elimination on shortest, and thus more amenable, counterexamples. Second, the internal structure of IC3 allows our extension to be integrated in a fully incremental fashion, never restarting the search from scratch to find a new counterexample. While various approaches already solve the parameter synthesis problem for several kind of systems, like infinite-state transition systems, timed and hybrid automata, the advantages ParamIC3 are that: it synthesizes an optimal region of parameters, it avoids computing the whole set of the reachable states, it is incremental and applies quantifier elimination only to small formulas. We present the results of an experimental evaluation performed on benchmarks from the timed and hybrid systems domain. We compared the approach with similar SMT-based techniques and with techniques based on the computation of the reachable states. The results show the potential of our approach.
Cite as

Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter Synthesis with IC3 (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 106-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cimatti_et_al:OASIcs.SynCoP.2015.106,
  author =	{Cimatti, Alessandro and Griggio, Alberto and Mover, Sergio and Tonetta, Stefano},
  title =	{{Parameter Synthesis with IC3}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{106--107},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.106},
  URN =		{urn:nbn:de:0030-drops-56144},
  doi =		{10.4230/OASIcs.SynCoP.2015.106},
  annote =	{Keywords: Parameter Synthesis, Infinite-state Transition Systems, Satisfiability Modulo Theories, IC3}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact