Wed 11 May 2022 20:00 - 20:05 at ICSE room 3-even hours - Validation and Verification 5 Chair(s): Saba Alimadadi
Wed 25 May 2022 09:40 - 09:45 at Room 306+307 - Papers 4: Verification and Analysis Chair(s): Gregory Gay
An important ability of self-adaptive systems is to be able to autonomously understand the environment in which they operate and use this knowledge to control the environment behaviour in such a way that system goals are achieved. How can this be achieved when the environment is unknown? Two phase solutions that require a full discovery of environment behaviour before computing a strategy that can guarantee the goals or report the non-existence of such a strategy (i.e., unrealisability) are impractical as the environment may exhibit adversarial behaviour to avoid full discovery.
In this paper we formalise a control and discovery problem for reactive system environments. In our approach a strategy must be produced that will, for every environment, guarantee that unrealisablity will be correctly concluded or system goals will be achieved by controlling the environment behaviour. We present a solution applicable to environments characterisable as labeled transition systems (LTS). We use modal transition systems (MTS) to represent partial knowledge of environment behaviour, and rely on MTS controller synthesis to make exploration decisions. Each decision either contributes more knowledge about the environment’s behaviour or contributes to achieving the system goals. We present an implementation restricted to GR(1) goals and show its viability.
Tue 10 MayDisplayed time zone: Eastern Time (US & Canada) change
Wed 11 MayDisplayed time zone: Eastern Time (US & Canada) change
Wed 25 MayDisplayed time zone: Eastern Time (US & Canada) change
09:30 - 10:30 | Papers 4: Verification and AnalysisTechnical Track / Journal-First Papers at Room 306+307 Chair(s): Gregory Gay Chalmers and the University of Gothenburg | ||
09:30 5mTalk | Static Stack-Preserving Intra-Procedural Slicing of WebAssembly BinariesBest Artifact Award Technical Track Quentin Stiévenart Vrije Universiteit Brussel, David Binkley Loyola University Maryland, Coen De Roover Vrije Universiteit Brussel DOI Pre-print Media Attached | ||
09:35 5mTalk | Diversity-Driven Automated Formal VerificationDistinguished Paper Award Technical Track DOI Pre-print Media Attached | ||
09:40 5mTalk | Control and Discovery of Environment Behaviour Journal-First Papers Maureen Keegan Intercom, Nicolás D’Ippolito Dept. of Computer Science FCEyN, University of Buenos Aires, Víctor Braberman ICC (UBA-CONICET), Nir Piterman University of Gothenberg, Sebastian Uchitel Universidad de Buenos Aires / Imperial College Link to publication DOI Pre-print Media Attached | ||
09:45 5mTalk | Learning Lenient Parsing & Typing via Indirect Supervision Journal-First Papers Toufique Ahmed University of California at Davis, Prem Devanbu Department of Computer Science, University of California, Davis, Vincent J. Hellendoorn Carnegie Mellon University Link to publication DOI Pre-print Media Attached | ||
09:50 5mTalk | Striking a Balance: Pruning False-Positives from Static Call GraphsNominated for Distinguished Paper Technical Track Akshay Utture University of California, Los Angeles (UCLA), Shuyang Liu University of California, Los Angeles, Christian Gram Kalhauge Technical University of Denmark, Jens Palsberg University of California at Los Angeles DOI Pre-print Media Attached | ||
09:55 5mTalk | SugarC: Scalable Desugaring of Real-World Preprocessor Usage into Pure C Technical Track Zachary Patterson University of Texas at Dallas, Zenong Zhang The University of Texas at Dallas, Brent Pappas University of Central Florida, Shiyi Wei University of Texas at Dallas, Paul Gazzillo University of Central Florida Pre-print Media Attached |