Wozu PROMELA when man auf plain C schreiben kann?

klte
Windoof-User
Windoof-User
Beiträge: 31
Registriert: 7. Sep 2011 15:22

Wozu PROMELA when man auf plain C schreiben kann?

Beitrag von klte »

Hi Leute!

Die drei Zeilen in PROMELA-Sprache sagen viel aus:

c_code {
\#include "someheaders.h"
\#include "someCcode.c"
};

:mrgreen:

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Wozu PROMELA when man auf plain C schreiben kann?

Beitrag von yourmaninamsterdam »

Man kann das schon machen, aber C-Code wird vom Verifier als korrekt angenommen. Da es hier nicht im Kern um Programmierung, sondern um Modellierung und Verifikation geht, hast du nichts davon, dass Promela embedded C unterstützt. Promela selbst hat andere Kerneigenschaften als C, z. B. Nichtdeterminismus der Ausführung.

Antworten

Zurück zu „Archiv“