No.102 Reverse Execution in Testing –Improving Security and Reliability

NII Shonan Meeting:

@ Shonan Village Center, July 3-6, 2017

Organizers

  • Michael Kirkedal Thomsen, DIKU, University of Copenhagen, Danmark
  • Kazutaka Matsuda, Tohoku University, Japan
  • Mohammad Reza Mousavi, Halmstad University, Sweden

Overview

Introduction

Implementing programs without errors is important for reliably and security of software. But though it is important it is also a hard task. Many approaches to this have over the years been developed, exemplified by numerous testing techniques, formal verification, and static program analysis. These techniques can be used identify problematic parts of programs or to some degree verify the correctness of them. However, achieving any guarantees is often impossible or (at the least) very cumbersome, which to some extend is due to the complexity of the conventional deterministic computation model. So using a more restricted computation model have the potential to improve this.

A way to achieve this is to use a computation model that have a notion of reverse execution. Here, the ability of compute from any reached state back to any previous state is the restriction over a deterministic model; but at the same time the restriction gives the possibility for better reasoning within the model. There exist several different notions of which on can achieve reverse execution. Two of the most widely researched area are Reversible Computations and Bidirectional Transformations.

Reversible Computations are often designed to be on completely information lossless and information generating. The initial studies can be dated back to the years around 1960 with three different studies that based on quite different computation models and motivations: Huffman studied information lossless finite state machines for their applications to data transmission, Landauer came to study reversible logic in his quest to determine the sources of energy dissipation in a computing system, and Lecerf studied reversible Turing machines for their theoretical properties. The field is often motivated by Landauer’s work that based on a gedankenexperiment found that, theoretically, the energy consumption of computations is not correlated with how much information is processed, but only with the amount of information that is lost during the computations. A result that have since been experimentally verified. However, modern research in the area have a larger focus on applications where the information preservation has an advantage.

Bidirectional Transformations are transformations, or more generally mechanisms, that keep the consistency of two ore more data. Originally, bidirectional transformation was studied mainly around 80s in the database community as the view-update problem, in which one transformation is a usual query and the other transformation is translation of updates on a view to updates on the original table. Recently, the problem draws our attention again, influenced by the rise of programming languages and techniques for bidirectional transformations (such as lenses), and the needs in software development processes being complex, especially in model-driven software development.

Testing meets Reversible Computations and Bidirectional Transformations

While both reversible computations and bidirectional transformations are small but growing research fields, testing is large and well established. No one will doubt that testing is immensely important to reliability of software and new techniques are often presented; from finite state-machine based models to recent years frameworks for automatic randomized test generation.

It is interesting that all three fields share the possibility to improve reliability of programs, though there is a difference in the foundations behind. This is why we find that increased cross-collaboration can result in interesting new research. This both researching test algorithms for reversible and bidirectional programming models, and exploiting the structures of backward execution models in testing subsets programs without backwards execution.

Goals and results of the meeting

Within the European networking project COST Action IC1405 on reversible computations some of this work has been initiated. Initial collaborations crossing between these fields have been established, also involving organisers of this Shonan meeting. However, this is primarily a European project.

A focused Shonan meeting will, firstly, give a better possibility to push the ideas and discussion out to a wider audience and, secondly, give better involvement of the international community (and more specifically the Japanese) in the fields. The four days is the perfect opportunity for networking between the areas. We expect that the invited experts will bring back a view into a new area and ideas for future collaborations.