https://wiki-de.moshellshocker.dns64.de/index.php?action=history&feed=atom&title=SPINSPIN - Versionsgeschichte2026-06-01T19:51:55ZVersionsgeschichte dieser Seite in Wikipedia (Deutsch) – Lokale KopieMediaWiki 1.43.8https://wiki-de.moshellshocker.dns64.de/index.php?title=SPIN&diff=1681095&oldid=previmported>Invisigoth67: form2023-08-01T09:48:54Z<p>form</p>
<p><b>Neue Seite</b></p><div>{{Begriffsklärungshinweis|Zu anderen Bedeutungen siehe [[Spin (Begriffsklärung)]]}}<br />
'''SPIN''' (ursprünglich ein [[Akronym]] für ''Simple [[PROMELA]] Interpreter'') ist eines der bekanntesten Werkzeuge zur [[Modellprüfung]] ({{enS|Model Checking}}). SPIN prüft [[Endlicher Automat|endliche Zustandsautomaten]] (engl. ''Finite State Machines'') mit der temporalen Logik [[Lineare temporale Logik|LTL]]. Zusätzlich bietet SPIN viele Optimierungsmethoden, zum Beispiel [[Partial Order Reduction]], Komprimierungen und Bitstate Hashing.<br />
<br />
== Geschichte ==<br />
SPIN wurde 1980 von [[Gerard J. Holzmann]] entwickelt, anfangs am Computing Sciences Research Center der [[Bell Labs]]. Der Quellcode zu SPIN wurde 1991 unter einer eigenen Lizenz offengelegt.<ref>[http://www.spinroot.com/spin/spin_license.html Lizenz von SPIN]</ref><br />
<br />
Der jährlich seit 1995 stattfindende ''SPIN Workshop'' behandelt mittlerweile nicht nur SPIN, sondern Modellprüfung im Allgemeinen.<ref>[http://spinroot.com/spin/Workshops/index.html Vergangene SPIN-Workshops auf der SPIN-Website]</ref> Im Jahre [[2001]] wurde Holzmann für seine Arbeit an SPIN mit dem [[ACM Software System Award]] der [[Association for Computing Machinery]] (ACM) ausgezeichnet.<ref>{{Webarchiv|url=http://awards.acm.org/citation.cfm?id=0750084&srt=all&aw=149&ao=SOFTWSYS |wayback=20091223063435 |text=Software System Award |archiv-bot=2019-05-11 13:33:10 InternetArchiveBot }} auf acm.org</ref><br />
<br />
[[PROMELA]] und der Model Checker SPIN wurden u.&nbsp;a. bei der Software-Entwicklung für die Marssonde [[Mars Science Laboratory|Curiosity]] eingesetzt.<ref name="Holzmann:2014:MC:2556647.2560218" /><br />
<br />
== Siehe auch ==<br />
* [[Symbolic Model Verifier]]<br />
<br />
== Literatur ==<br />
* Gerard J. Holzmann: ''The SPIN Model Checker: Primer and Reference Manual''. Addison-Wesley, 2004. ISBN 0-321-22862-6.<br />
<br />
== Weblinks ==<br />
* [http://www.spinroot.com/ Website von SPIN]<br />
* [http://spinroot.com/spin/whatispin.html#S6 Literaturliste]<br />
<br />
== Einzelnachweise ==<br />
<references><br />
<ref name="Holzmann:2014:MC:2556647.2560218"><br />
{{Literatur<br />
|Autor=Gerard J. Holzmann<br />
|Titel=Mars Code<br />
|Reihe=Commun. ACM<br />
|BandReihe=57<br />
|NummerReihe=2<br />
|Verlag=ACM<br />
|Ort=New York<br />
|Jahr=2014-02<br />
|ISSN=0001-0782<br />
|Seiten=64–73<br />
|Sprache=en<br />
|DOI=10.1145/2560217.2560218}}<br />
<br />
</ref><br />
</references><br />
<br />
[[Kategorie:Automatentheorie]]</div>imported>Invisigoth67