Opera Software AB Linköping, Göteborgs Universitet = University of Gothenburg (GU), Compiler Optimization and Run-time Systems (CORSE), Centre Inria de l'Université Grenoble Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP), Université Grenoble Alpes (UGA), ANR-20-CE39-0009,SEVERITAS,Systèmes de tests et evaluations sûrs et vérifiables(2020)
Source:
RV 2022 - 22nd International Conference on Runtime Verification ; https://inria.hal.science/hal-03911794 ; RV 2022 - 22nd International Conference on Runtime Verification, Sep 2022, Tbilisi, Georgia. pp.1-19
International audience ; Kotlin was introduced to Android as the recommended language for development. One of the unique functionalities of Kotlin is that of coroutines, which are lightweight tasks that can run concurrently inside threads. Programming using coroutines is difficult, among other things, because they can move between threads and behave unexpectedly. We introduce runtime verification in Kotlin. We provide a language to write properties and produce runtime monitors tailored to verify Kotlin coroutines. We identify, formalise and runtime verify seven properties about common runtime errors that are not easily identifiable by static analysis. To demonstrate the acceptability of the technique in real applications, we apply our framework to an in-house Android app and microbenchmarks and measure the execution time and memory overheads.
