Graph-based software specification and verification

TY - THES

T1 - Graph-based software specification and verification

AU - Kastenberg, H.

N1 - 10.3990/1.9789036527347

PY - 2008/10/3

Y1 - 2008/10/3

N2 - The (in)correct functioning of many software systems heavily influences the way we qualify our daily lives. Software companies as well as academic computer science research groups spend much effort on applying and developing techniques for improving the correctness of software systems. In this dissertation we focus on using and developing graph-based techniques to specify and verify the behaviour of software systems in general, and object-oriented systems more specifically. We elaborate on two ways to improve the correctness (and thereby the quality) of such systems. On the one hand, we investigate the potential of using the graph transformation technique to formally specify the dynamic semantics of (object-oriented) programming languages. On the other hand, we develop techniques to verify systems of which the behaviour is specified as graph production systems. Most of the techniques developed in this work have been implemented in the Groove Tool Set. Typically, a system’s state is identified by the values assigned to the system’s state variables (often of primitive types such as integer and Boolean). In the object-oriented paradigm, objects (i.e., instances of classes) can be seen as state variables of which the internal state depends on the values of its attributes (or fields). We start with introducing a uniform framework for the specification and transformation of attributed graphs. In this framework, attributed graphs and their transformations are specified in terms of graph structures and graph morphisms only. One of the main advantages of such an approach is that it reduces the effort to implement a graph transformation engine for attributed graphs when compared to existing approaches. Additionally, we show that our uniform framework provides a natural way to deal with abstraction over the supported data domains, without the need to restrict to algebra homomorphisms. Once a system has been designed it must be implemented in some programming language that best fits to the type of system to be produced. Examples of popular programming languages are Java, C, and C♯. The semantics of such programming languages are typically specified in natural language. Unfortunately, such specifications are often hard to understand. More importantly, they often leave room for multiple interpretations. That is to say, they are ambiguous. In this work we show how the graph transformation framework provides formal and intuitive means to specify operational semantics of programming languages. For that, we introduce an artificial, object-oriented programming language called Taal, and define its control flow and execution semantics in terms of graph transformation rules. We also provide the necessary tool support to actually simulate the behaviour of any Taal-program. Once a system has been specified as a graph production system, its behaviour must be verified for correctness. Therefore, we introduce an algorithm that combines a well-known on-the-fly model checking algorithm with ideas from bounded model checking. We aim at verifying the temporal behaviour of such systems. This means that the properties to be verified are expressed as formulae in some (linear) temporal logic, e.g., LTL; the names of the graph transformation rules form the set of atomic propositions. We have extended the Groove Tool Set with verification functionality instead of performing the model checking procedure using an existing model checking tool. The main motivation for this is the ability to investigate how to optimally benefit from the potential of the graph transformation framework, especially in the context of combating the state-explosion problem using partial order reduction techniques. Unfortunately, many such existing techniques are based on assumptions that do not hold in our setting, e.g., regarding the number of actions (or operations) that can be performed. Therefore, we have developed a new dynamic partial order reduction algorithm based on selecting so-called probe sets. The algorithm is based on asymmetric stimulation and disabling relations. We have developed the algorithm in the context of entity-based systems in which states are uniquely characterized as sets of entities and actions can read, delete, create entities and forbid the existence of entities. This setting has been chosen because of its nice match with the graph transformation framework. In fact, we describe how graphs can be encoded as set of entities and how rule applications can be translated to corresponding entity-manipulating actions. We show that our algorithm produces a correctly reduced state space in the sense that all possible system executions are preserved. As yet, our algorithm is not accompanied with an implementation and therefore we have no figures on the reduction that can be obtained for different types of systems.

AB - The (in)correct functioning of many software systems heavily influences the way we qualify our daily lives. Software companies as well as academic computer science research groups spend much effort on applying and developing techniques for improving the correctness of software systems. In this dissertation we focus on using and developing graph-based techniques to specify and verify the behaviour of software systems in general, and object-oriented systems more specifically. We elaborate on two ways to improve the correctness (and thereby the quality) of such systems. On the one hand, we investigate the potential of using the graph transformation technique to formally specify the dynamic semantics of (object-oriented) programming languages. On the other hand, we develop techniques to verify systems of which the behaviour is specified as graph production systems. Most of the techniques developed in this work have been implemented in the Groove Tool Set. Typically, a system’s state is identified by the values assigned to the system’s state variables (often of primitive types such as integer and Boolean). In the object-oriented paradigm, objects (i.e., instances of classes) can be seen as state variables of which the internal state depends on the values of its attributes (or fields). We start with introducing a uniform framework for the specification and transformation of attributed graphs. In this framework, attributed graphs and their transformations are specified in terms of graph structures and graph morphisms only. One of the main advantages of such an approach is that it reduces the effort to implement a graph transformation engine for attributed graphs when compared to existing approaches. Additionally, we show that our uniform framework provides a natural way to deal with abstraction over the supported data domains, without the need to restrict to algebra homomorphisms. Once a system has been designed it must be implemented in some programming language that best fits to the type of system to be produced. Examples of popular programming languages are Java, C, and C♯. The semantics of such programming languages are typically specified in natural language. Unfortunately, such specifications are often hard to understand. More importantly, they often leave room for multiple interpretations. That is to say, they are ambiguous. In this work we show how the graph transformation framework provides formal and intuitive means to specify operational semantics of programming languages. For that, we introduce an artificial, object-oriented programming language called Taal, and define its control flow and execution semantics in terms of graph transformation rules. We also provide the necessary tool support to actually simulate the behaviour of any Taal-program. Once a system has been specified as a graph production system, its behaviour must be verified for correctness. Therefore, we introduce an algorithm that combines a well-known on-the-fly model checking algorithm with ideas from bounded model checking. We aim at verifying the temporal behaviour of such systems. This means that the properties to be verified are expressed as formulae in some (linear) temporal logic, e.g., LTL; the names of the graph transformation rules form the set of atomic propositions. We have extended the Groove Tool Set with verification functionality instead of performing the model checking procedure using an existing model checking tool. The main motivation for this is the ability to investigate how to optimally benefit from the potential of the graph transformation framework, especially in the context of combating the state-explosion problem using partial order reduction techniques. Unfortunately, many such existing techniques are based on assumptions that do not hold in our setting, e.g., regarding the number of actions (or operations) that can be performed. Therefore, we have developed a new dynamic partial order reduction algorithm based on selecting so-called probe sets. The algorithm is based on asymmetric stimulation and disabling relations. We have developed the algorithm in the context of entity-based systems in which states are uniquely characterized as sets of entities and actions can read, delete, create entities and forbid the existence of entities. This setting has been chosen because of its nice match with the graph transformation framework. In fact, we describe how graphs can be encoded as set of entities and how rule applications can be translated to corresponding entity-manipulating actions. We show that our algorithm produces a correctly reduced state space in the sense that all possible system executions are preserved. As yet, our algorithm is not accompanied with an implementation and therefore we have no figures on the reduction that can be obtained for different types of systems.

KW - METIS-252059

KW - EWI-13615

KW - IR-59779

U2 - 10.3990/1.9789036527347

DO - 10.3990/1.9789036527347

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-2734-7

PB - University of Twente

CY - Enschede

ER -