Execution Constraint Verification of Exception Handling on UML Sequence Diagrams

Selim Ciraci, Hasan Sözer, Mehmet Aksit, Wilke Havinga

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)

    Abstract

    Exception handling alters the control flow of the program. As such, errors introduced in exception handling code may influence the overall program in undesired ways. To detect such errors early and thereby decrease the programming costs, it is worthwhile to consider exception handling at design level. Preferably, design models must be extended to incorporate exception handling behavior and the control flow must be verified accordingly. Common practices for verification require a formal model and semantics of the design. Defining semantics and manually converting design models to formal models are costly. We propose an approach for verifying exception handling in UML design models, where we extend UML with exception handling notations, define execution and exception handling semantics, and automatically transform UML models to a formal model. The formal model is used for generating execution paths. Constraints are specified (as temporal logic formulas) on execution paths and are verified.
    Original languageEnglish
    Title of host publicationFifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011
    Place of PublicationPiscataway, NJ
    PublisherIEEE Computer Society
    Pages31-40
    Number of pages10
    ISBN (Print)978-1-4577-0780-3
    DOIs
    Publication statusPublished - 27 Jun 2011

    Fingerprint

    Semantics
    Flow control
    Temporal logic
    Costs

    Keywords

    • Graph transformations
    • Exception handling
    • Object-oriented design
    • Fault tolerance
    • Design verification

    Cite this

    Ciraci, S., Sözer, H., Aksit, M., & Havinga, W. (2011). Execution Constraint Verification of Exception Handling on UML Sequence Diagrams. In Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011 (pp. 31-40). Piscataway, NJ: IEEE Computer Society. https://doi.org/10.1109/SSIRI.2011.13
    Ciraci, Selim ; Sözer, Hasan ; Aksit, Mehmet ; Havinga, Wilke. / Execution Constraint Verification of Exception Handling on UML Sequence Diagrams. Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011. Piscataway, NJ : IEEE Computer Society, 2011. pp. 31-40
    @inproceedings{6a7eb04a80c54f2bba7d7351caaf59f0,
    title = "Execution Constraint Verification of Exception Handling on UML Sequence Diagrams",
    abstract = "Exception handling alters the control flow of the program. As such, errors introduced in exception handling code may influence the overall program in undesired ways. To detect such errors early and thereby decrease the programming costs, it is worthwhile to consider exception handling at design level. Preferably, design models must be extended to incorporate exception handling behavior and the control flow must be verified accordingly. Common practices for verification require a formal model and semantics of the design. Defining semantics and manually converting design models to formal models are costly. We propose an approach for verifying exception handling in UML design models, where we extend UML with exception handling notations, define execution and exception handling semantics, and automatically transform UML models to a formal model. The formal model is used for generating execution paths. Constraints are specified (as temporal logic formulas) on execution paths and are verified.",
    keywords = "Graph transformations, Exception handling, Object-oriented design, Fault tolerance, Design verification",
    author = "Selim Ciraci and Hasan S{\"o}zer and Mehmet Aksit and Wilke Havinga",
    year = "2011",
    month = "6",
    day = "27",
    doi = "10.1109/SSIRI.2011.13",
    language = "English",
    isbn = "978-1-4577-0780-3",
    pages = "31--40",
    booktitle = "Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011",
    publisher = "IEEE Computer Society",
    address = "United States",

    }

    Ciraci, S, Sözer, H, Aksit, M & Havinga, W 2011, Execution Constraint Verification of Exception Handling on UML Sequence Diagrams. in Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011. IEEE Computer Society, Piscataway, NJ, pp. 31-40. https://doi.org/10.1109/SSIRI.2011.13

    Execution Constraint Verification of Exception Handling on UML Sequence Diagrams. / Ciraci, Selim; Sözer, Hasan; Aksit, Mehmet; Havinga, Wilke.

    Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011. Piscataway, NJ : IEEE Computer Society, 2011. p. 31-40.

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Execution Constraint Verification of Exception Handling on UML Sequence Diagrams

    AU - Ciraci, Selim

    AU - Sözer, Hasan

    AU - Aksit, Mehmet

    AU - Havinga, Wilke

    PY - 2011/6/27

    Y1 - 2011/6/27

    N2 - Exception handling alters the control flow of the program. As such, errors introduced in exception handling code may influence the overall program in undesired ways. To detect such errors early and thereby decrease the programming costs, it is worthwhile to consider exception handling at design level. Preferably, design models must be extended to incorporate exception handling behavior and the control flow must be verified accordingly. Common practices for verification require a formal model and semantics of the design. Defining semantics and manually converting design models to formal models are costly. We propose an approach for verifying exception handling in UML design models, where we extend UML with exception handling notations, define execution and exception handling semantics, and automatically transform UML models to a formal model. The formal model is used for generating execution paths. Constraints are specified (as temporal logic formulas) on execution paths and are verified.

    AB - Exception handling alters the control flow of the program. As such, errors introduced in exception handling code may influence the overall program in undesired ways. To detect such errors early and thereby decrease the programming costs, it is worthwhile to consider exception handling at design level. Preferably, design models must be extended to incorporate exception handling behavior and the control flow must be verified accordingly. Common practices for verification require a formal model and semantics of the design. Defining semantics and manually converting design models to formal models are costly. We propose an approach for verifying exception handling in UML design models, where we extend UML with exception handling notations, define execution and exception handling semantics, and automatically transform UML models to a formal model. The formal model is used for generating execution paths. Constraints are specified (as temporal logic formulas) on execution paths and are verified.

    KW - Graph transformations

    KW - Exception handling

    KW - Object-oriented design

    KW - Fault tolerance

    KW - Design verification

    U2 - 10.1109/SSIRI.2011.13

    DO - 10.1109/SSIRI.2011.13

    M3 - Conference contribution

    SN - 978-1-4577-0780-3

    SP - 31

    EP - 40

    BT - Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011

    PB - IEEE Computer Society

    CY - Piscataway, NJ

    ER -

    Ciraci S, Sözer H, Aksit M, Havinga W. Execution Constraint Verification of Exception Handling on UML Sequence Diagrams. In Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011. Piscataway, NJ: IEEE Computer Society. 2011. p. 31-40 https://doi.org/10.1109/SSIRI.2011.13