Correctness

Bitte beschreibe das System-Model, welches der formalen Spezifikation von Publish/Subscribe-Systemen zugrunde liegt!
Wie ist ein Systemzustand und ein system trace definiert?
Was ist eine Spezifikation und wann erfüllt ein System diese Spezifikation?
Erkläre die Sicherheits- und Lebendigkeitseigenschaften!
Was ist die Semantik der Temporaloperatoren always, eventually und next?
Bitte beschreibe die Lebendigkeits- und Sicherheitseigenschaften eines korrekten Publish/Subscribe-Systems!
Was ist der Unterschied zwischen einem validen Routing-Agorithmus und einem monoton validen Routing-Agorithmus?
Wie sind die Invarianten von simple routing und covering based routing definiert?

Kommentare

Nur angemeldete Nutzer dürfen kommentieren. Hier geht's zur kostenlosen Registrierung.