Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking
Business analysts and domain experts are often sketching the behaviors of a software system using high-level models that are technology- and platform-independent. The developers will refine and enrich these high-level models with technical details. As a consequence, the refined models can deviate fr...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1404.0852v1 |
| _version_ | 1831774405437423616 |
|---|---|
| author | Faiz UL Muram Huy Tran Uwe Zdun |
| author_facet | Faiz UL Muram Huy Tran Uwe Zdun |
| author_sort | Faiz UL Muram |
| collection | DOAJ |
| description | Business analysts and domain experts are often sketching the behaviors of a software system using high-level models that are technology- and platform-independent. The developers will refine and enrich these high-level models with technical details. As a consequence, the refined models can deviate from the original models over time, especially when the two kinds of models evolve independently. In this context, we focus on behavior models; that is, we aim to ensure that the refined, low-level behavior models conform to the corresponding high-level behavior models. Based on existing formal verification techniques, we propose containment checking as a means to assess whether the system's behaviors described by the low-level models satisfy what has been specified in the high-level counterparts. One of the major obstacles is how to lessen the burden of creating formal specifications of the behavior models as well as consistency constraints, which is a tedious and error-prone task when done manually. Our approach presented in this paper aims at alleviating the aforementioned challenges by considering the behavior models as verification inputs and devising automated mappings of behavior models onto formal properties and descriptions that can be directly used by model checkers. We discuss various challenges in our approach and show the applicability of our approach in illustrative scenarios. |
| first_indexed | 2024-12-22T08:53:50Z |
| format | Article |
| id | doaj.art-7852e7f0ad964cbd8440793d2fcfb945 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-22T08:53:50Z |
| publishDate | 2014-04-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-7852e7f0ad964cbd8440793d2fcfb9452022-12-21T18:31:53ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-04-01147Proc. FESCA 20149310710.4204/EPTCS.147.7:21Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment CheckingFaiz UL MuramHuy TranUwe ZdunBusiness analysts and domain experts are often sketching the behaviors of a software system using high-level models that are technology- and platform-independent. The developers will refine and enrich these high-level models with technical details. As a consequence, the refined models can deviate from the original models over time, especially when the two kinds of models evolve independently. In this context, we focus on behavior models; that is, we aim to ensure that the refined, low-level behavior models conform to the corresponding high-level behavior models. Based on existing formal verification techniques, we propose containment checking as a means to assess whether the system's behaviors described by the low-level models satisfy what has been specified in the high-level counterparts. One of the major obstacles is how to lessen the burden of creating formal specifications of the behavior models as well as consistency constraints, which is a tedious and error-prone task when done manually. Our approach presented in this paper aims at alleviating the aforementioned challenges by considering the behavior models as verification inputs and devising automated mappings of behavior models onto formal properties and descriptions that can be directly used by model checkers. We discuss various challenges in our approach and show the applicability of our approach in illustrative scenarios.http://arxiv.org/pdf/1404.0852v1 |
| spellingShingle | Faiz UL Muram Huy Tran Uwe Zdun Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking Electronic Proceedings in Theoretical Computer Science |
| title | Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking |
| title_full | Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking |
| title_fullStr | Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking |
| title_full_unstemmed | Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking |
| title_short | Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking |
| title_sort | automated mapping of uml activity diagrams to formal specifications for supporting containment checking |
| url | http://arxiv.org/pdf/1404.0852v1 |
| work_keys_str_mv | AT faizulmuram automatedmappingofumlactivitydiagramstoformalspecificationsforsupportingcontainmentchecking AT huytran automatedmappingofumlactivitydiagramstoformalspecificationsforsupportingcontainmentchecking AT uwezdun automatedmappingofumlactivitydiagramstoformalspecificationsforsupportingcontainmentchecking |