PROMELA

aus Wikipedia, der freien Enzyklopädie
Dies ist die aktuelle Version dieser Seite, zuletzt bearbeitet am 25. Februar 2022 um 06:57 Uhr durch imported>KnightMove(135966) (Kategorie:Abkürzung).
(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)

PROMELA (Process/Protocol Meta Language) ist eine Spezifikationssprache, die synchrone und asynchrone verteilte Algorithmen und Protokolle mittels nichtdeterministischer, endlicher Automaten beschreibt. PROMELA wird hauptsächlich im Bereich der Verifikation eingesetzt, zum Beispiel im Modellprüfer SPIN.

PROMELA und der Model Checker SPIN wurden u. A. bei der Software-Entwicklung für die Marssonde Curiosity eingesetzt.[1]

Einzelnachweise

  1. Gerard J. Holzmann: Mars Code (= Commun. ACM. Band 57, Nr. 2). ACM, Februar 2014, ISSN 0001-0782, S. 64–73, doi:10.1145/2560217.2560218 (englisch).