Evolvable Behavior Specifications Using Context-Sensitive Wildcards

G. Gülesir

    Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

    38 Downloads (Pure)

    Abstract

    The development and maintenance of today's software systems is an increasingly effort-consuming and error-prone task. A major cause of the effort and errors is the lack of human-readable and formal documentation of software design. In practice, software design is often informally documented, or not documented at all. Therefore, (a) the design cannot be properly communicated between software engineers, (b) it cannot be automatically analyzed for finding and removing faults, (c) the conformance of an implementation to the design cannot be automatically verified, and (d) source code maintenance tasks have to be manually performed, although some of these tasks can be automated using formal documentation. In this thesis, we address these problems for the design and documentation of the behavior implemented in procedural programs. We present the following solutions each addressing the respective problem stated above: (a) A graphical language called VisuaL, which enables engineers to specify constraints on the possible sequences of function calls from a given procedural program, (b) an algorithm called CheckDesign, which automatically verifies the consistency between multiple specifications written in VisuaL, (c) an algorithm called CheckSource, which automatically verifies the consistency between a given implementation and a corresponding specification written in VisuaL, and (d) an algorithm called TransformSource, which uses VisuaL specifications for automatically inserting additional source code at well-defined locations in existing source code. Empirical evidence indicates that CheckSource is beneficial during some of the typical control-flow maintenance tasks: 60% effort reduction, and prevention of one error per 250 lines of source code. These results are statistically significant at the level 0,05. Moreover, the combination of CheckSource and TransformSource is beneficial during some of the typical control-flow maintenance tasks: 75% effort reduction, and prevention of one error per 140 lines of source code. These results are statistically significant at the level 0,01. The main contribution of this thesis is the graphical language VisuaL with its formal underpinning Deterministic Abstract Recognizers (DARs), which defines a new family of formal languages called Open Regular Languages (ORLs). The key feature of VisuaL is the context-sensitive wildcard, which makes VisuaL specifications more evolvable (i.e. less susceptible to changes), and more concise.
    Original languageUndefined
    Awarding Institution
    • University of Twente
    Supervisors/Advisors
    • Akşit, Mehmet , Supervisor
    • Bergmans, Lodewijk, Advisor
    Thesis sponsors
    Award date13 Mar 2008
    Place of PublicationEnschede
    Publisher
    Print ISBNs978-90-365-2633-3
    DOIs
    Publication statusPublished - 13 Mar 2008

    Keywords

    • EWI-12998
    • CR-D.2
    • CR-D.1.7
    • METIS-251050
    • IR-58767
    • CR-D.2.2

    Cite this

    Gülesir, G.. / Evolvable Behavior Specifications Using Context-Sensitive Wildcards. Enschede : University of Twente, 2008. 202 p.
    @phdthesis{da6a170ccd0348dfa4782e59579f1895,
    title = "Evolvable Behavior Specifications Using Context-Sensitive Wildcards",
    abstract = "The development and maintenance of today's software systems is an increasingly effort-consuming and error-prone task. A major cause of the effort and errors is the lack of human-readable and formal documentation of software design. In practice, software design is often informally documented, or not documented at all. Therefore, (a) the design cannot be properly communicated between software engineers, (b) it cannot be automatically analyzed for finding and removing faults, (c) the conformance of an implementation to the design cannot be automatically verified, and (d) source code maintenance tasks have to be manually performed, although some of these tasks can be automated using formal documentation. In this thesis, we address these problems for the design and documentation of the behavior implemented in procedural programs. We present the following solutions each addressing the respective problem stated above: (a) A graphical language called VisuaL, which enables engineers to specify constraints on the possible sequences of function calls from a given procedural program, (b) an algorithm called CheckDesign, which automatically verifies the consistency between multiple specifications written in VisuaL, (c) an algorithm called CheckSource, which automatically verifies the consistency between a given implementation and a corresponding specification written in VisuaL, and (d) an algorithm called TransformSource, which uses VisuaL specifications for automatically inserting additional source code at well-defined locations in existing source code. Empirical evidence indicates that CheckSource is beneficial during some of the typical control-flow maintenance tasks: 60{\%} effort reduction, and prevention of one error per 250 lines of source code. These results are statistically significant at the level 0,05. Moreover, the combination of CheckSource and TransformSource is beneficial during some of the typical control-flow maintenance tasks: 75{\%} effort reduction, and prevention of one error per 140 lines of source code. These results are statistically significant at the level 0,01. The main contribution of this thesis is the graphical language VisuaL with its formal underpinning Deterministic Abstract Recognizers (DARs), which defines a new family of formal languages called Open Regular Languages (ORLs). The key feature of VisuaL is the context-sensitive wildcard, which makes VisuaL specifications more evolvable (i.e. less susceptible to changes), and more concise.",
    keywords = "EWI-12998, CR-D.2, CR-D.1.7, METIS-251050, IR-58767, CR-D.2.2",
    author = "G. G{\"u}lesir",
    note = "http://doc.utwente.nl/58767/",
    year = "2008",
    month = "3",
    day = "13",
    doi = "10.3990/1.9789036526333",
    language = "Undefined",
    isbn = "978-90-365-2633-3",
    publisher = "University of Twente",
    address = "Netherlands",
    school = "University of Twente",

    }

    Evolvable Behavior Specifications Using Context-Sensitive Wildcards. / Gülesir, G.

    Enschede : University of Twente, 2008. 202 p.

    Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

    TY - THES

    T1 - Evolvable Behavior Specifications Using Context-Sensitive Wildcards

    AU - Gülesir, G.

    N1 - http://doc.utwente.nl/58767/

    PY - 2008/3/13

    Y1 - 2008/3/13

    N2 - The development and maintenance of today's software systems is an increasingly effort-consuming and error-prone task. A major cause of the effort and errors is the lack of human-readable and formal documentation of software design. In practice, software design is often informally documented, or not documented at all. Therefore, (a) the design cannot be properly communicated between software engineers, (b) it cannot be automatically analyzed for finding and removing faults, (c) the conformance of an implementation to the design cannot be automatically verified, and (d) source code maintenance tasks have to be manually performed, although some of these tasks can be automated using formal documentation. In this thesis, we address these problems for the design and documentation of the behavior implemented in procedural programs. We present the following solutions each addressing the respective problem stated above: (a) A graphical language called VisuaL, which enables engineers to specify constraints on the possible sequences of function calls from a given procedural program, (b) an algorithm called CheckDesign, which automatically verifies the consistency between multiple specifications written in VisuaL, (c) an algorithm called CheckSource, which automatically verifies the consistency between a given implementation and a corresponding specification written in VisuaL, and (d) an algorithm called TransformSource, which uses VisuaL specifications for automatically inserting additional source code at well-defined locations in existing source code. Empirical evidence indicates that CheckSource is beneficial during some of the typical control-flow maintenance tasks: 60% effort reduction, and prevention of one error per 250 lines of source code. These results are statistically significant at the level 0,05. Moreover, the combination of CheckSource and TransformSource is beneficial during some of the typical control-flow maintenance tasks: 75% effort reduction, and prevention of one error per 140 lines of source code. These results are statistically significant at the level 0,01. The main contribution of this thesis is the graphical language VisuaL with its formal underpinning Deterministic Abstract Recognizers (DARs), which defines a new family of formal languages called Open Regular Languages (ORLs). The key feature of VisuaL is the context-sensitive wildcard, which makes VisuaL specifications more evolvable (i.e. less susceptible to changes), and more concise.

    AB - The development and maintenance of today's software systems is an increasingly effort-consuming and error-prone task. A major cause of the effort and errors is the lack of human-readable and formal documentation of software design. In practice, software design is often informally documented, or not documented at all. Therefore, (a) the design cannot be properly communicated between software engineers, (b) it cannot be automatically analyzed for finding and removing faults, (c) the conformance of an implementation to the design cannot be automatically verified, and (d) source code maintenance tasks have to be manually performed, although some of these tasks can be automated using formal documentation. In this thesis, we address these problems for the design and documentation of the behavior implemented in procedural programs. We present the following solutions each addressing the respective problem stated above: (a) A graphical language called VisuaL, which enables engineers to specify constraints on the possible sequences of function calls from a given procedural program, (b) an algorithm called CheckDesign, which automatically verifies the consistency between multiple specifications written in VisuaL, (c) an algorithm called CheckSource, which automatically verifies the consistency between a given implementation and a corresponding specification written in VisuaL, and (d) an algorithm called TransformSource, which uses VisuaL specifications for automatically inserting additional source code at well-defined locations in existing source code. Empirical evidence indicates that CheckSource is beneficial during some of the typical control-flow maintenance tasks: 60% effort reduction, and prevention of one error per 250 lines of source code. These results are statistically significant at the level 0,05. Moreover, the combination of CheckSource and TransformSource is beneficial during some of the typical control-flow maintenance tasks: 75% effort reduction, and prevention of one error per 140 lines of source code. These results are statistically significant at the level 0,01. The main contribution of this thesis is the graphical language VisuaL with its formal underpinning Deterministic Abstract Recognizers (DARs), which defines a new family of formal languages called Open Regular Languages (ORLs). The key feature of VisuaL is the context-sensitive wildcard, which makes VisuaL specifications more evolvable (i.e. less susceptible to changes), and more concise.

    KW - EWI-12998

    KW - CR-D.2

    KW - CR-D.1.7

    KW - METIS-251050

    KW - IR-58767

    KW - CR-D.2.2

    U2 - 10.3990/1.9789036526333

    DO - 10.3990/1.9789036526333

    M3 - PhD Thesis - Research UT, graduation UT

    SN - 978-90-365-2633-3

    PB - University of Twente

    CY - Enschede

    ER -