Model-Checking zur Analyse von Message Sequence Charts über Statecharts

Die Unified Modeling Language (UML) enthält sowohl Statecharts als auch mit Sequence Diagrams eine Variante von Message Sequence Charts (MSCs). Da beide eingesetzt werden können, um verschiedene Aspekte eines Systems zu beschreiben, ist es sinnvoll, die Konsistenz zwischen beiden Beschreibungstechniken zu prüfen. Im vorliegenden Bericht werden beide Ansätze miteinander notationell und semantisch integriert und eine formale Konsistenzbeziehung formuliert. Zu diesem Zweck werden hier die MSC-Notation zu MSC_CTL erweitert, die Semantik von Statecharts in Termini von Transitionssystemen beschrieben und in MSC_CTL formulierte Anforderungen nach CTL* abgebildet. Die eigentliche Analyse erfolgt unter Einsatz eines Model-Checkers. Dazu sind hier Abbildungsvorschriften für einen speziellen Model-Checker angegeben. Aufgrund der mit der Prüfung von CTL*-Formeln verbundenen Komplexität ist hier zudem ein Verfahren angegeben, um die Beweisverpflichtungen in eine einfacher zu handhabende Form zu umzusetzen.

Available as gzipped Postscript file (124 KB).
 

BibTeX Entry

@techreport{Canver99:MCAMSCSC,
  author = "Canver, Ercüment",
  title = "Model-Checking zur Analyse von Message Sequence Charts über Statecharts",
  institution = "Universität Ulm",
  type = "UIB",
  number = "99-04",
  note = "ISSN 0939-5091",
  year = "1999"
}