Laden...

Verifizierung einer RS232 Implementierung in C#

Erstellt von Tarion vor 12 Jahren Letzter Beitrag vor 12 Jahren 1.738 Views
T
Tarion Themenstarter:in
381 Beiträge seit 2009
vor 12 Jahren
Verifizierung einer RS232 Implementierung in C#

Ich bin nach einiger Zeit mal wieder hier im Forum gelandet. Ich beschäftige mich aktuell mit der Verifizierung und Verifizierten Implementierung eines Protokolls.

Ich habe mich die letzte Woche intensiv damit beschäftigt wie man Software und Protokolle Spezifiziert, Verifiziert, Testet und Simuliert. Ziel des Threads soll es sein weitere Ideen und Anregungen zu dem Thema zu sammeln und meine Gedanken ein wenig zu ordnen. Da das Thema sehr weit gestreut ist, möchte ich meine bisherigen Ergebnisse ein wenig zusammenfassen:

Modelierung
Es gibt viele Tools die basierend auf verschiedenen Logiken wie LTL, CTL, CTL* mit denen sich Automaten und Systeme mit Modellen auf bestimmte Eigenschaften testen lassen können.
Ich habe das Protokoll bis zu einem bestimmten Abstraktionslevel bereits mit dem Tool Uppaal modelliert. Ich bin sicher, dieses Modell lässt sich noch erweitern und auch mit anderen Modelcheckern auf weitere Eigenschaften prüfen. Uppaal ist nicht optimal weil es eher auf Zeitkritische Anwendungen ausgelegt ist, was mein Protokoll nur bedingt ist (Nur Timeouts). Das größte Problem ist dabei eher ein korrektes Modell zu erstellen und zu wissen auf welche Eigenschaften es ankommt.
An Tools habe ich mir bisher näher angesehen: Alloy (Analyze Structures), Uppaal (timed automata), Spin (LTL), Enterprise Architect (Simulation), und es gibt noch viele mehr die ich nur kurz angesehen habe.

Verifizierung
Zwei Dinge müssen Verifiziert werden: Das Protokoll und die Implementierung.
Mit Code Contracts, Pex und automatischer Testgenerierung kommt man ja schon sehr weit. Dennoch handelt es sich um Testen und nicht um verifizieren. Hier ist die Frage, wie weit kann man überhaupt gehen? Wo sind die Grenze?
Man kann Runtime verfication über die Contracts machen und mit generierten Testcases eine Hohe Codecoverrage erreichen. Wie weit ist solch ein Vorgehen von formalen Verifikationen noch entfernt?

Welche Erfahrungen habt ihr in der Praxis gemacht?

Ausblick
Interessant wären Techniken um Modelle aus dem C# Code zu bekommen. Vielleicht kann man auch ein Modell der Spezifikation bauen und mit der Ausführung der Implementierung synchronisieren. Dann könnte man auf dem Modell Verifikationen durchführen und über die Laufzeitsynchronisation feststellen wie nahe das Modell an der Implementierung ist oder ob Zustände/Übergänge fehlen.

Über das Protokoll an sich kann ich hier aus verschiedenen Gründen nichts sagen. Es gibt natürlich auch einige Konkrete Probleme im Protokoll die ich angehen werden. Ich suche aktuell aber noch auf einer allgemeineren Ebene nach Lösungen und Problemen zum Thema "Verifikation".

49.485 Beiträge seit 2005
vor 12 Jahren

Hallo Tarion,

ich weiß nicht, wieviele Leute sich hier schon mit formaler Spezifikation und Programmverifikation beschäftigt haben. Ich habe mich nur im Studium damit beschäftigt (hauptsächlich algebraische Spezifikation und Theorembeweisen und das ist schon ziemlich lange her, damals konnte man - wenn überhaupt - die Korrektheit einzelner Funktionen beweisen) und habe es nie praktisch eingesetzt. Ich habe zwar davon gehört, dass es einige wesentliche Fortschritte auf dem Gebiet gegeben hat (z.B. formale Verifikation des Windows Kernels oder zumindest des Hypervisors), kenne diese aber nicht genauer. Trotzdem will ich versuchen, deine Fragen zu beantworten.

Hier ist die Frage, wie weit kann man überhaupt gehen? Wo sind die Grenze?

Das hängt in erster Linie davon ab, viele Zustände bzw. Zustandsfolgen es gibt. Ist diese unendlich oder sehr groß, kann man immer nur einen verschwindenden bzw. sehr kleinen Ausschnitt testen. Hast du eine überschaubare Menge, kann man u.U. alle Möglichkeiten testen. Dann ist man genauso gut oder besser als bei einer Verifikation.

Außerdem hängt es davon ab, wie unterschiedlich die Zustände sind. Wenn man z.B. String.Length vollständig testen wollte, müsste man das für a, b, aa, ab, ba, bb, aaa, aab, aba, abb, ... tun, also für alle Kombinationen und das nicht nur die Kombinationen aus a und b, sondern für die aus allen (Unicode-)Zeichen. Das kann man natürlich vergessen. Allerdings ist es ja vollkommen egal, welche Zeichen in dem String enthalten sind, es kommt nur auf die Länge an (ok, in gewissem Sinne beißt sich die Katze hier in den Schwanz, weil das eigentlich nur gilt, wenn man von der Korrektheit ausgeht). Da String.Length einen Int32 liefert, würde man einen (quasi) vollständigen Test über alle ca. 4 Milliarden Fälle (=unterschiedlichen Längen) in akzeptabler Zeit durchführen können.

Man kann Runtime verfication über die Contracts machen und mit generierten Testcases eine Hohe Codecoverrage erreichen. Wie weit ist solch ein Vorgehen von formalen Verifikationen noch entfernt?

Das hängt zum einen von dem bisher Gesagten ab, zum anderen davon, ob man es schafft, alle Punkte der Spezifikation auch als Contract zu formulieren. Und nicht nur das, sondern man muss auch sicher sein, dass der Contract auch wirklich das aussagt, was man aussagen will (bzw. eben das, was in der Spezifikation steht). Da Contracts in C# formuliert werden müssen, ist das nicht immer trivial. Bei den Contracts zur Parameterprüfung geht das oft noch, aber bei Contracts, die die Korrektheit des Ergebnissen sichern sollen, wird es oft haarig. Das kann schnell auf eine Art Multiversionprogramming hinauslaufen, bei der der Contract dann nur aussagt, ob alle Versionen das gleiche Ergebnis berechnet haben.

Aber das Problem hat man nicht nur bei Contracts. Auch beim Erstellen einer Spezifikation (oder des Modells, sofern dieses nicht mit dem Quellcode identisch ist), kann man Fehler machen. Das ist dann auch die ultimative Grenze der Programmverifikation: Es wird "nur" geprüft, ob zwei verschiedene Beschreibungen derselben Aufgabenstellung (Quellcode bzw. Modell auf der einen Seite und die formale Spezifikation auf der anderen Seite) beweisbar übereinstimmen. Es sagt nichts darüber aus, ob die Spezifikation mit dem in der realen Welt gewünschten Systemverhalten übereinstimmt.

Ein Programm ist korrekt, wenn es (beweisbar) der Spezifikation entspricht. Aber keiner kann beweisen, ob die Spezifikation überhaupt beschreibt, was man beschreiben wollte.

Und es ist auch nicht sicher, ob ein Beweis korrekt ist, siehe auch Variable in Thread erhalten (Absatz über Edsger Dijkstra). Je formaler ein Beweis ist, desto wahrscheinlicher ist er korrekt, bzw. desto leichter findet man den Fehler, wenn er es nicht ist.

Interessant wären Techniken um Modelle aus dem C# Code zu bekommen.

Da sind wir wieder bei dem Punkt, dass ich nicht auf dem aktuellen Stand bin. Ich weiß nicht, wie realistisch das ist. Bei reinem C#-Code mag es ja noch angehen. Aber wenn Klassen und Methoden aus dem .NET Framework verwendet werden, wirds haarig, weil man dann deren Korrektheit beweisen müsste, bzw. zumindest eine exakte formale Beschreibung dessen haben müsste, was die Methoden überhaupt tun.

Für interessanter und gleichzeitig realistischer - gerade wenn es um ein Protokoll geht - halte ich es, dass man aus dem Modell den Quellcode generiert.

herbivore

C
1.214 Beiträge seit 2006
vor 12 Jahren

@Tarion: ich versteh nicht ganz, was du genau beweisen möchtest. Das RS232 Protokoll gibts ja schon ^^ Hast du ein eigenes Protokoll entwickelt, das darauf aufsetzt? Oder willst du das RS232 Protokoll in Hardware implementieren? Oder willst du es als Emulationsschicht in Software implementieren?

Mit der seriellen Schnittstelle habe ich nur praktische Erfahrungen gesammelt, und nur schlechte. Das funktioniert vorne und hinten nicht stabil. Ich kann mir grad schlecht vorstellen, von welcher Korrektheit man da überhaupt sprechen kann...

T
Tarion Themenstarter:in
381 Beiträge seit 2009
vor 12 Jahren

R232 ist kein Protokoll sondern eine Schnittstelle. Wenn du willst, kannst du sogar das TCP/IP Protokoll für RS232 implementieren (wohl nicht sehr sinnvoll).

Wir haben ein eigens entwickeltes Protokoll welches bereits implementiert ist und nun im rahmen einer neuen Softwareversion erneut implementiert wird. Ich beschäftige mich anhand dieses Beispiels mit dem Thema der Verifikation von Modell & Software.

@herbivore: Danke, das sind schöne Realitätsnahe antworten.
Man wird wohl immer davon ausgehen müssen, dass das eigene Modell korrekt ist. Wenn das Modell nicht zu groß ist, ist es zumindest überschaubarer als Quellcode. Das Framework wird man wohl auch als korrekt annehmen müssen.