Alloy Analyzer

Alloy Analyzer
Alloy Analyser
Screenshot of Alloy Analyzer.png
Screenshots mit Beispiel
Basisdaten
Maintainer Daniel Jackson
Aktuelle Version 4.1.10
(19. März 2009)
Betriebssystem plattformunabhängig
Programmier­sprache Java
Lizenz MIT-Lizenz
Deutschsprachig nein
alloy.mit.edu

Der Alloy Analyzer ist ein in der Informatik und Softwaretechnik eingesetztes Programm, das dazu genutzt werden kann, um Spezifikationen, die in der gleichnamigen Sprache geschrieben sind, zu analysieren.[1] Das Analyseprogramm kann Instanzen der Modelinvarianten erzeugen, die Ausführung von Operationen simulieren, die als Teil des Models definiert wurden, und benutzerdefinierte Eigenschaften des Models überprüfen. Es unterstützt auch die Analyse von Teilmodellen, ebenso die inkrementelle Analyse von Modellen, so wie sie erstellt werden, und Rückgabe direkter Ergebnisse an den Anwender.

Das Analyseprogramm und die zugehörige Alloy-Sprache wurden unter Leitung von Daniel Jackson am Massachusetts Institute of Technology in den USA entwickelt. Der erste Prototyp wurde bereits 1997 entwickelt.

Analyseansatz

Der Alloy Analyser wurde insbesondere entwickelt für sogenannte leichte Formale Methoden ("lightweight formal methods"). Beispielsweise ist es beabsichtigt vollständige, automatische Analyse zu unterstützen, im Gegensatz zu interaktiven Theorembeweistechniken, die im Allgemeinen von ähnlichen Sprachen wie Alloy benutzt werden. Die Entwicklung von Alloy wurde beeinflusst von der automatischen Analyse, die von Model Checkern angeboten wird. Jedoch ist Model Checking ungeeignet für die Art von Modellen, die mit Alloy entwickelt werden. Demnach wurde der Kern der Anwendung letztlich als Model-finder auf einem SAT-Solver aufgebaut.[1]

In Version 3.0 umschloss der Alloy Analyser einen eingebauten SAT-basierten Model-finder, der auf einem Standardsolver beruht. Mit der Version 4.0 wurde allerdings der Kodkod Model-finder integriert, für den der Alloy Analyser als Front-End dient. Beide Model-finder übersetzen hauptsächlich ein Model von Relationaler Logik in eine entsprechende Formel der Booleschen Algebra und berufen sich dann auf einen Standard-SAT-Solver. In Falle, dass der Solver eine Lösung findet, wird das Ergebnis zurück in die entsprechende Bindung von Konstanten zu Variablen im Relationalen Model transformiert.[2]

Um sicherzustellen, dass das Problem der Modellsuche entscheidbar ist, führt der Alloy Analyzer eine Modellsuche über einem beschränktem Gültigkeitsbereich bestehend aus einer endlichen Anzahl benutzerdefinierten Objekte aus. Dies hat zur Folge, dass die Allgemeingültigkeit der Ergebnisse eingeschränkt ist. Jedoch begründen die Entwickler von Alloy Analyzer die Entscheidung zur Einschränkung des Gültigkeitsbereichs unter Berufung auf die small scope hypothesis[1], die besagt, dass ein hoher Anteil an Programmfehlern bereits gefunden werden kann, wenn man das Programm für alle Eingabewerte eines kleinen Gültigkeitsbereichs prüft.[3]

Einzelnachweise

  1. a b c Daniel Jackson: Software Abstrations: Logic, Language, and Analysis. MIT Press, 2006, ISBN 978-0-262-10114-1.
  2. Torlak, E.; G. Dennis (April 2008). "Kodkod for Alloy Users" (PDF). First ACM Alloy Workshop. Portland, Oregon, Aufgerufen am 24. Dezember 2009
  3. Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid und Darko Marinov (2002), "Evaluating the small scope hypothesis"

Weblinks


Wikimedia Foundation.

Игры ⚽ Нужна курсовая?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Alloy Analyzer — In computer science and software engineering, the Alloy Analyzer is a software tool which can be used to analyze specifications written in the Alloy specification language.cite book|last=Jackson|first=Daniel |authorlink=Daniel Jackson (computer… …   Wikipedia

  • Alloy — bezeichnet: Alloy Analyzer, ein in der Informatik und Softwaretechnik eingesetztes Programm Alloy Creek, ein Fluss im US Bundesstaat Montana Diese Seite ist eine Begriffsklärung zur Unterscheidung mehrerer mit demselben Wort bezeichneter Begriffe …   Deutsch Wikipedia

  • Alloy (specification language) — In computer science and software engineering, the Alloy specification language is a declarative language for expressing complex structural constraints and behavior in a software system. Alloy provides a simple structural modeling tool based on… …   Wikipedia

  • Формальные методы — Пример формальной спецификации с использованием Z нотации В информатике и инженерии программного обеспечения формальными методами называется группа техник, основанных на математическом аппарате для …   Википедия

  • Daniel Jackson (computer scientist) — Daniel Jackson (born 1963) is a Professor of Computer Science at the Massachusetts Institute of Technology (MIT). He is the principal designer of the Alloy modelling language, and author of the book Software Abstractions: Logic, Language, and… …   Wikipedia

  • 7439-92-1 — Plomb Pour les articles homonymes, voir Plomb (homonymie) et Pb.  Pour l’article homophone, voir Plon …   Wikipédia en Français

  • Plomb — Pour les articles homonymes, voir Plomb (homonymie) et Pb.  Pour l’article homophone, voir Plon …   Wikipédia en Français

  • Corrosion — v · d · e Materials failure modes Buckling · …   Wikipedia

  • ISS-Expedition 8 — Missionsemblem Missionsdaten Mission: ISS Expedition 8 Besatzung: 2 Rettungsschiffe …   Deutsch Wikipedia

  • X-ray photoelectron spectroscopy — [ right|thumb|350px|Basic components of a monochromatic XPS system.] X ray photoelectron spectroscopy (XPS) is a quantitative spectroscopic technique that measures the elemental composition, empirical formula, chemical state and electronic state… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”