Experimental evaluation of a tool for the verification and transformation of source code in event-driven systems

G. Gülesir, Klaas van den Berg, Lodewijk Bergmans, Mehmet Aksit

    Research output: Contribution to journalArticleAcademicpeer-review

    6 Citations (Scopus)
    97 Downloads (Pure)


    In event-driven systems, separating the reactive part of software (i.e., event-driven control) from the non-reactive part is a common design practice. The reactive part is typically structured according to the states and transitions of a system, whereas the non-reactive part is typically structured according to the concepts of the application domain (e.g., the services provided by the system). In such systems, the non-reactive part of software stimulates the reactive part with event calls. Whenever the non-reactive part is modified (e.g., during evolution), the existing event calls may become invalid, new event calls may become necessary, and the two parts of software may become incompatible. Manually finding and repairing these types of defects is a time-consuming and error-prone maintenance task. In this article, we present a solution that combines source code model checking and aspect-oriented programming techniques, to reduce the time spent by developers and to automatically find defects, while performing the maintenance task mentioned above. In addition, we present controlled experiments showing that the solution can reduce the time by 75%, and enable the prevention of one defect per 140 lines of source code.
    Original languageUndefined
    Article number10.1007/s10664-009-9107-y
    Pages (from-to)720-777
    Number of pages58
    JournalEmpirical software engineering
    Issue number1
    Publication statusPublished - 18 Mar 2009


    • Source code transformation
    • Source code verification
    • EWI-15346
    • METIS-264398
    • IR-65488
    • Event-driven systems
    • Formal experiment

    Cite this