217 Pages
English

Model transformation for validation of software design [Elektronische Ressource] / vorgelegt von Shadi Al Dehni

-

Gain access to the library to view online
Learn more

Description

ModelTransformationForValidationOfSoftwareDesignShadiAlDehniMunchen,¨ 20082Institutfur¨ Informatik LMULudwigLehr-undForschungseinheitfur¨ MaximiliansUniversitätProgrammierungundSoftwaretechnikMünchenDissertationimFachInformatikanderFakultat¨ fur¨ Mathematik,undStatistikderLudwig Maximilians Universit at¨ Munchen¨vorgelegtvonShadi AlDehniausDamaskus,Syrien4Programmierung und Softwaretechnik Institut für InformatikPST LMUErstgutachter: Prof. Dr. MartinWirsingZweitgutachter: Dr. rer. nat. habil. StephanMerzPrufer:¨ Prof. Dr. Hans PeterKriegelPrufer:¨ Prof. Dr. RolfHennickerTagdermundlichen¨ Prufung:¨ 08. Juli2008AbstractModelcheckingisamethodforformallyverifyingfinite stateconcurrentsystemssuchascircuitdesigns and communication protocols. System specification is expressed as temporal logic for-mula, where efficient symbolic algorithms are used to traverse the model defined by the systemand check if the specification holds or not. Large state space can often be traversed in min utes. Graphicalnotationplaysanimportantroleinsoftwaremodelinganddesigns. TheUnifiedModelingLanguage(UML)isastandardlanguageforspecifying,visualizing,constructing,anddocumentingtheartifactsofsoftwaresystems. Nowadaysgraphgrammarsenableahighlevelofabstraction of software architecture and form a basis for various analysis and transformations.Their methods, techniques, and results have already been applied in many fields of computerscience.

Subjects

Informations

Published by
Published 01 January 2008
Reads 16
Language English
Document size 3 MB

ModelTransformationForValidationOf
SoftwareDesign
ShadiAlDehni
Munchen,¨ 20082Institutfur¨ Informatik LMULudwig
Lehr-undForschungseinheitfur¨ Maximilians
UniversitätProgrammierungundSoftwaretechnik
München
DissertationimFachInformatik
anderFakultat¨ fur¨ Mathematik,undStatistik
derLudwig Maximilians Universit at¨ Munchen¨
vorgelegtvon
Shadi AlDehni
ausDamaskus,Syrien4Programmierung und Softwaretechnik Institut für Informatik
PST LMU
Erstgutachter: Prof. Dr. MartinWirsing
Zweitgutachter: Dr. rer. nat. habil. StephanMerz
Prufer:¨ Prof. Dr. Hans PeterKriegel
Prufer:¨ Prof. Dr. RolfHennicker
Tagdermundlichen¨ Prufung:¨ 08. Juli2008
Abstract
Modelcheckingisamethodforformallyverifyingfinite stateconcurrentsystemssuchascircuit
designs and communication protocols. System specification is expressed as temporal logic for-
mula, where efficient symbolic algorithms are used to traverse the model defined by the system
and check if the specification holds or not. Large state space can often be traversed in min
utes. Graphicalnotationplaysanimportantroleinsoftwaremodelinganddesigns. TheUnified
ModelingLanguage(UML)isastandardlanguageforspecifying,visualizing,constructing,and
documentingtheartifactsofsoftwaresystems. Nowadaysgraphgrammarsenableahighlevelof
abstraction of software architecture and form a basis for various analysis and transformations.
Their methods, techniques, and results have already been applied in many fields of computer
science.
Inthisthesis,weproposenewtechniquesforanefficienttransformationofUMLsoftwarede
signs into a formalization for the model checking software, expressed by the approach of graph
grammars and graph transformation systems. We have implemented our techniques in several
case studies like ATM designs and security protocols. We demonstrate empirically that our
transformationtechniquesarewell suitedtoapplytheminspecificUMLsoftwaredesigns. Our run along two lines: The first line is to transform the UML state ma
chinesintoequivalentsimplerstatemachinescalledexecutablestatemachines,wherethemodel
checker HUGO and SPIN are called upon to verify whether certain required properties are in
deedrealizedbytheUMLstatemachinedesigns. ThesecondlineistotransformtheUMLstate
machines into predicate diagrams, whereas the JML assertions and the Bandera Specification
Language (BSL) are used to verify the desired properties. The model checker DIXIT attempts
to verify the properties against the created predicate diagrams. Our prototype tool DAMAS
is developed to use our transformation strategies to transform and compile the UML software
designsintoformalizationofmodelcheckingsoftwareandviceversa.
6Zusammenfassung
Model Checking ist eine Methode zur formalen Verifikation von nebenlaufigen¨ Systemen mit
endlichem Zustandsraum. Beispiele solcher Systeme sind elektrische Schaltungen oder Kom
munikationsprotokolle. Eine Systemspezifikation ist durch temporallogische Formeln gegeben,
fur¨ die es effiziente symbolische Algorithmen gibt, um das Systemmodell zu durchlaufen und
die Gultigk¨ eit der Spezifikation zu uberpr¨ ufen.¨ Sogar große Zustandsraume¨ konnen¨ mit diesen
Algorithmen in wenigen Minuten uberpr¨ uft¨ werden. Graphische Notationen spielen bei der
Modellierung und beim Entwurf von Software eine große Rolle. Die Unified Modeling Lan
¨guage (UML) bildet dabei einen Standard fur die Spezifikation, Visualisierung, Konstruktion
und Dokumentation von Artifakten von Software Systemen. Heutzutage erlauben Graphgram
matiken einen hohen Grad der Abstraktion von Software Architekturen und bilden eine Basis
fur¨ verschiedene Analysen und Transformationen. Die verwendeten Methoden, Techniken und
ErgebnissewurdenbereitsinvielenBereichenderInformatikangewandt.
In dieser Arbeit wurden neue Techniken zur effizienten Transformation von UML Software
Entwurfsmodellenineinefur¨ eineModelCheckingSoftwaregeeigneteForm,diedurchGraph
grammatikenundGraphtransformationssystemeerzeugtwird,entwickelt. DieseTechnikenwer-
den an verschiedenen Fallstudien, wie u.a. an Entwurfsmodellen von Geldautomaten Software
oder von Sicherheitsprotokollen, erprobt. Die Erfahrung hat gezeigt, dass die entwickelten
TransformationstechnikenbeibestimmtenUML Entwurfsmodellenbesondersgutgeeignetsind.
DieTenarbeitenaufzweiWegen: aufdemerstenwerdenUML Zustands
maschinenzunachst¨ ineinfachereZustandsmaschinen,diesogenanntenausfuhrbaren¨ Zustands transformiert. AufdiesewerdendanndieModelCheckerHUGOundSPINangewen
det, um zu prufen,¨ ob bestimmte geforderte Eigenschaften von den UML Zustandsmaschinen
tatsachlich¨ erfullt¨ werden. AufdemzweitenWegwerdenUML ZustandsdiagrammeinPr adika ¨
tendiagramme transformiert, wobei JML Zusicherungen und die Bandera Specification Lan
¨guage (BSL) zum Nachweis der gewunschten Eigenschaften verwendet werden. Der Model
¨Checker DIXIT kann zur Uberprufung¨ der erzeugten Pradikatendiagramme¨ verwendet werden.
Die vorgestellten Strategien zur Transformation und Kompilation von UML Entwurfsmodellen
in eine fur¨ eine Model Checking Software geeignete Form, und umgekehrt, wurden in dem
Werkzeug PrototypDAMASimplementiert.
7Acknowledgement
ThisPhDthesisistheresultofalmostfiveyearsofworkattheLudwigMaximiliansUniversity
in Munich. The move from Syria to Germany and everything I learned and experienced during
this time is impossible to describe in full. Writing a PhD thesis in another continent is a pro
cess that requires not only hard work but a lot of support from family, friends, and colleagues.
Therefore,itismypleasuretothankthemanypeoplewhomadethisthesispossible.
I am especially grateful to my supervisor, Professor Martin Wirsing, for his patient guidance
into the theoretical, conceptual, and methodological areas of my PhD research. Prof. Wirsing
has supported me not only by providing a research assistantship over the five years, but also he
has provided me with inspiration and motivation to complete this thesis. Herrn Wirsing, Vielen
herzlichenDankanSie!
I would like also to thank Professor Fred Kroger¨ , his recommendations and suggestions have
beeninvaluabletomyresearchproject.
MysincerethanksgoouttoProf. AlexanderKnappforallhishelpandsupportespeciallyinthe
initialperiodofmyresearchstudies. DankeAlex!
Special thanks also go to Dr. Jan Jurjens¨ for the collaborative work in the security systems, and
manythanksforthetimewespenttogetherintheworkshopinUK.
It is an honor to have a thesis committee devised of scholarly and dedicated educators. I would
like to thank Dr. Stephan Merz for his invaluable suggestions to improve my thesis. I am also
highlygratefultoprof. RolfHennickerandprof. Hans PeterKriegelforthegreatdiscussions.
MyprofoundgratitudetothePSTteamintheInstituteofInformaticsinLMUforprovidingme
invaluablescientificassistanceandanexcellentandverystimulatingworkingatmosphere. Iam
verygratefultoMatthiasLudwigforhiscontinuoushelpinLatexduringwritingmydissertation
andmanythanksforDr. HubertBaumeisterforourgreatdiscussions.
The financial support of DAAD (Deutscher Akademischer Austauschdienst) allowed the real
ization of my PhD at the LMU Munchen.¨ Many thanks to DAAD for the help and care during
myresearchstudyatLMU.
8A special word of thanks goes to my parents, my brothers Fadi and Nour. Mum and dad,
thankyouforteachingmetohavethepatienttoachievethisscientificwork. Manythankstomy
twinbrotherDr. Fadiforhisconstantsupportandencouragementofmyacademicpursuits,and
forNourforallhishelp. Aboveall,thankstomyfriendsfortheirwarmfriendship.
ShadiAl Dehni,
Munchen,¨ 05.06.2008
910