Safe Reasoning with Logic LTS

In der Praxis ist es oft wünschenswert, einen deklarativen mit einem operationalen Spezifikationsstil zu mischen. Damit kann man in einer Spezifikation eine gewünschte operationale Architektur vorgeben und zugleich Komponenten sowie Anforderungen an das Gesamtsystem logisch spezifizieren; man kann auch eine Spezifikation in einer geeigneten Logik schrittweise in einen operationalen Entwurf umsetzen.

Ziel unseres gegenwärtigen Projekts ist es, eine Spezifikationssprache für nebenläufige Systeme zu entwickeln, in der man prozessalgebraische und temporal-logische Operatoren beliebig mischen kann. Die zugehörige Implementierungssrelation soll (1) kompositionales Vorgehen unterstützen, (2) sich auf Prozessen in das bekannte Spektrum der Concurrency-Semantiken einordnen, (3) auf logischen Formeln der Implikation entsprechen, und (4) zwischen einem Prozess und einer Formel ausdrücken, dass jener diese erfüllt.

Zunächst haben wir beschriftete Transitionssysteme (LTS) in geeigneter Weise auf Logic LTS erweitert und eine geringe Zahl von Operatoren auf diesen definiert. Ausgehend von einer sehr einfachen Basis-Relation haben wir gezeigt, dass die auf sog. Ready-Simulationen gestützte Präordnung genau richtig für die Behandlung der Konjunktion und der Parallelkomposition ist; diese erfüllt dann auch für weitere Opera- tionen die genannten Anforderungen an eine Implementierungssrelation. Schließlich haben wir unserem Ansatz auch temporal-logische Operationen für Sicherheitseigenschaften hinzugefügt.