Files in this item



application/pdfMANSKY-DISSERTATION-2020.pdf (475kB)
(no description provided)PDF


Title:Verified collection-based regression test selection via an extended Jinja semantics
Author(s):Mansky, Susannah Elizabeth
Director of Research:Gunter, Elsa L
Doctoral Committee Chair(s):Gunter, Elsa L
Doctoral Committee Member(s):Rosu, Grigore; Marinov, Darko; Lochbihler, Andreas
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):interactive theorem proving
regression test selection
small-step semantics
formal methods
Abstract:The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. Regression Test Selection (RTS) algorithms select which tests to rerun on revised code, reducing the time required to check for newly introduced errors. An RTS algorithm is considered safe if and only if all deselected tests would have unchanged results. Ekstazi [1] is a Java library for regression testing. Its algorithm adds print statements to JVM code in order to collect the names of classes used by a test during its execution on a program. When the program is changed, tests are only rerun if a class they used changed. The main insight in their algorithm is that not all uses of classes must be noted, as many necessarily require previous uses, such as when using an object previously created. This thesis presents JinjaDCI, which extends Klein and Nipkow's Jinja [2] to include support for static instructions and dynamic class initialization. Related proofs are extended and updated, including Java-level and JVM-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. The semantics of this extension are based on the Java SE 8 specification. This extension is then used in a formal proof of safety of an RTS algorithm based on that used by Ekstazi. The algorithm formally defined and proved safe here uses an instrumented semantics to collect touched classes in an even smaller set of locations. Problems with Ekstazi's current collection location set that make it not safe are identified, and a modified set that will make it equivalent to the safe set is presented. The theorems given in this thesis have been formalized in the theorem prover Isabelle. The RTS algorithms were modeled via instrumentation of JinjaDCI's JVM semantics. These instrumentations are given via a general definition for Collection Semantics, small-step semantics instrumented to collect information during execution. A formal general definition of RTS algorithms, including a definition of safety, is also given.
Issue Date:2020-11-30
Rights Information:Copyright 2020 Susannah Mansky
Date Available in IDEALS:2021-03-05
Date Deposited:2020-12

This item appears in the following Collection(s)

Item Statistics