Abstract
| Original language | English |
|---|---|
| Title of host publication | Fifth IEEE International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011 |
| Place of Publication | Piscataway, NJ |
| Publisher | IEEE Computer Society |
| Pages | 31-40 |
| Number of pages | 10 |
| ISBN (Print) | 978-1-4577-0780-3 |
| DOIs | |
| Publication status | Published - 27 Jun 2011 |
Fingerprint
Keywords
- Graph transformations
- Exception handling
- Object-oriented design
- Fault tolerance
- Design verification
Cite this
}
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 proceeding › Conference contribution › Academic › peer-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 -