Logo des Repositoriums

Auflistung nach Autor:in "Ammann, Christian"

1 - 4 von 4
  • Zeitschriftenartikel
    Formal Verication of Web Applications
    (Softwaretechnik-Trends: Vol. 32, No. 1, 2012) Ammann, Christian
  • Konferenzbeitrag
    From business modeling to verified applications
    (INFORMATIK 2011 – Informatik schafft Communities, 2011) Ammann, Christian; Kleuker, Stephan; Pulvermüller, Elke
    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.
  • Zeitschriftenartikel
    Integration von Model-Driven Development und formaler Verifikation in den Softwareentwicklungsprozess - eine Fallstudie mit einem 3D-Tracking-System
    (Softwaretechnik-Trends Band 30, Heft 4, 2010) Ammann, Christian
    Bei modellgetriebener Softwareentwicklung werden Modelle entwickelt und aus diesen ausführbare Software generiert. Durch die Verknüpfung mit formaler Verifikation können Fehler in den Modellen gefunden und so der Ansatz der modellgetriebenen Softwareentwicklung verbessert werden. Diese Arbeit untersucht anhand von zwei Fallstudien, wie aktuelle Forschungsergebnisse im Bereich der Modellierung und Verifikation auf Verhaltensebene in den Softwareentwicklungsprozess integriert werden können.
  • Zeitschriftenartikel
    Verifikation von UML-Statecharts unter besonderer Berücksichtigung von Speicherverbrauch und Laufzeit des Model Checkers
    (Softwaretechnik-Trends Band 31, Heft 3, 2011) Ammann, Christian
    Ein Model Checker verifiziert, ob ein Modell bestimmte Anforderungen erfüllt. Eine Möglichkeit, das Verhalten von Softwaresystemen zu modellieren, sind endliche Automaten. Diese finden Einzug in die Unified Modelling Language in Form von Statecharts. UML-Statecharts können ein hohes Maß an Komplexitt erreichen, so dass sich ihr Zustandsraum nicht mehr komplett in den Hauptspeicher abbilden lsst. Dies führt dazu, dass eine vollstndige Verifikation mit einem Model Checker nicht mehr möglich ist, da der gesamte Zustandsraum nicht mehr untersucht werden kann. Um diesem Problem zu begegnen, stellt diese Arbeit die domnenspezifische Sprache UDL (UML-Statechart Description Language), sowie eine Transformation von UDL in die Model Checker Eingabesprache Promela vor. Der Schwerpunkt der Sprache UDL und des Übersetzungsprozesses liegt dabei auf der Generierung von effizientem Promelacode, der beim Verifizieren einen möglichst kleinen Zustandsraum belegt. Der Vorteil ist, dass durch diesen Ansatz auch größere Modelle wieder verifizierbar werden. Die Machbarkeit des Ansatzes und die daraus entstehenden Vorteile werden anhand einer Fallstudie mit dem 3D-Bewegungstrackingsystem AssyControl demonstriert.