Programmiersprache: Microsoft stellt P unter Open-Source-Lizenz

Microsoft hat kürzlich die Programmiersprache P unter die MIT License gestellt. Das Softwareunternehmen beschreibt P als domänenspezifische Sprache, mit der sich offenbar die Kommunikation zwischen den Komponenten von asynchronen Embedded-, Netzwerk- und verteilten Systemen modellieren lassen soll. Bei Microsoft kam P beispielsweise bei der Entwicklung und Verifizierung der USB-Gerätetreibersoftware von Windows 8 und Windows Phone zum Einsatz.

Mit P erstellte Systeme werden als Sammlung miteinander agierender Zustandsmaschinen (finite state machine) definiert, von denen jede aus Input Queue, Status, Transitionen und einem maschinenlokalen Speicher besteht. Die Maschinen können jeweils asynchron miteinander kommunizieren. Eine Operation in P aktualisiert entweder einen lokalen Speicher, sendet eine Nachricht oder erstellt eine neue Maschine.

Laut Microsoft lassen sich P-Programme über Model Checking verifizieren, wodurch Entwickler die Gewährleistung darüber haben, dass jedes Event eines Systems in angemessener Zeit abgearbeitet wird. Damit sich P-Programme responsiv verhalten, müssen ihre State Machines die Events, die sich aus der Wartescheife nehmen lassen, in jedem Zustand angehen können. Doch besteht auch die Möglichkeit, einige Events zu verschieben; jedoch gibt die Sprache dann vor, dass sich ein Event potenziell nicht für immer verzögern lässt.

P kann C-Code generieren, der sich dann über einen C-Compiler ausführen lässt. Der P-Compiler selbst gibt ein Zing-Modell aus, das Entwickler für systematische Tests nutzen können. Zing ist wiederum eine quelloffene Modellprüfungssoftware für nebenläufige Programme, die in der Lage ist, alle möglichen Zustände eines Modells zu untersuchen. (ane)