From business modeling to verified applications
| dc.contributor.author | Ammann, Christian | |
| dc.contributor.author | Kleuker, Stephan | |
| dc.contributor.author | Pulvermüller, Elke | |
| dc.contributor.editor | Heiß, Hans-Ulrich | |
| dc.contributor.editor | Pepper, Peter | |
| dc.contributor.editor | Schlingloff, Holger | |
| dc.contributor.editor | Schneider, Jörg | |
| dc.date.accessioned | 2018-11-27T09:59:14Z | |
| dc.date.available | 2018-11-27T09:59:14Z | |
| dc.date.issued | 2011 | |
| dc.description.abstract | UML activity diagrams can be used to model business processes which are implemented in a software project. It is a worthwhile goal to automatically transform at least parts of UML diagrams into software. Automated code generation reduces the total amount of errors in a software project but the model itself can still violate specified requirements. A quality improvement is the usage of a model checker which searches through the whole state space of model and checks whether all requirements are met. A model checker requires a formal description of a model for a complete verification. Activity diagrams often describe processes informally which is difficult to verify with a model checker. We therefore propose the transformation of activityto statechart diagrams which allow a more detailed and formal description. Several algorithms exist to map UML statecharts into a model checker input language for a successful formal verification. Afterwards, the model checker searches through the whole state space of a statechart and therefore has to store each state in memory. UML statecharts can reach a high degree of complexity which is problematic for a complete state space traversal because the total amount of available memory is exhausted. Ac- cordingly, we present the domain specific language UDL (UML Statechart Modeling Language) and a transformation from UDL into the Spin model checker input language Promela. UDL contains features for property preserving abstraction which reduces the models state space and therefore the memory consumption of a model checker. Furthermore, we introduce an optimisation technique for the transformation process from UDL to Promela which focuses on a reduced model checker run-time. A case study with a movement tracking system demonstrates how our approach could significantly reduce the memory consumption of a model checker and allows the verification of complex models. | en |
| dc.identifier.isbn | 978-88579-286-4 | |
| dc.identifier.pissn | 1617-5468 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/18661 | |
| dc.language.iso | en | |
| dc.publisher | Gesellschaft für Informatik e.V. | |
| dc.relation.ispartof | INFORMATIK 2011 – Informatik schafft Communities | |
| dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Proceedings, Volume P-192 | |
| dc.title | From business modeling to verified applications | en |
| dc.type | Text/Conference Paper | |
| gi.citation.endPage | 312 | |
| gi.citation.publisherPlace | Bonn | |
| gi.citation.startPage | 312 | |
| gi.conference.date | 4.-7. Oktober 2011 | |
| gi.conference.location | Berlin | |
| gi.conference.sessiontitle | Regular Research Papers |
Dateien
Originalbündel
1 - 1 von 1