Graph-based software specification and verification

H. Kastenberg

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    264 Downloads (Pure)

    Abstract

    The (in)correct functioning of many software systems heavily influences how 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 specically. We elaborate on two ways to improve the correctness (and thereby the quality) of such systems.
    Firstly, we investigate the potential of using the graph transformation technique to formally specify the dynamic semantics of (object-oriented) programming languages. Those semantics are typically specied in natural language. Such specications are often hard to understand or even ambiguous. We show how the graph transformation framework provides formal and intuitive means for their specication.
    Secondly, we develop techniques to verify systems of which the behaviour is specied as graph production systems. For the verication of such systems, we introduce an algorithm that combines a well-known on-the-y model checking algorithm with ideas from bounded model checking. One of the main problems of model checking is the state-explosion problem. This problem is often tackled using partial order reduction techniques. Unfortunately, many such techniques are based on assumptions that do not hold for graph production systems. Therefore, we develop a new dynamic partial order reduction algorithm based on selecting so-called probe sets and prove its correctness.
    Most of the techniques developed in this dissertation have been implemented in the graph transformation tool GROOVE.
    Original languageUndefined
    QualificationDoctor of Philosophy
    Awarding Institution
    • University of Twente
    Supervisors/Advisors
    • Rensink, Arend, Advisor
    • Brinksma, Ed, Supervisor
    • Akşit, Mehmet, Supervisor
    Award date3 Oct 2008
    Place of PublicationEnschede
    Publisher
    Print ISBNs978-90-365-2734-7
    DOIs
    Publication statusPublished - 3 Oct 2008

    Keywords

    • METIS-252059
    • EWI-13615
    • IR-59779

    Cite this