| View previous topic :: View next topic |
| Author |
Message |
manuels
Advocate
Joined: 22 Nov 2003
Posts: 2146
Location: Europe
|
 Posted: Sat May 14, 2011 11:04 am Post subject: Buchempfehlung zur formalen Verifikation von Programmen |
 |
|
Hi,
ich hab mich schon mehrmals gefragt, wie und mit welchen Tools, Computerprogramme formal verifiziert werden.
Leider habe ich bis jetzt im Netz nichts brauchbares gefunden, daher wollte ich mal nachfragen, ob mir jemand von euch einen Buchtipp zu diesem Thema geben kann.
Danke!
Manuel
_________________
Build your own live cd with catalyst 2.0! |
|
| Back to top |
|
 |
schachti
Advocate
Joined: 28 Jul 2003
Posts: 3765
Location: Gifhorn, Germany
|
| Posted: Sat May 14, 2011 12:19 pm Post subject: |
|
|
Einen konkreten Buchtipp habe ich nicht, aber "statische Codeanalyse" als Schlagwort. Ein Tool dafür, das ich kenne, ist Polyspace. Vielleicht hilft Dir das schonmal weiter.
_________________
Never argue with an idiot. He brings you down to his level, then beats you with experience.
How-To: Daten verschlüsselt auf DVD speichern. |
|
| Back to top |
|
|
Knieper
l33t
Joined: 10 Nov 2005
Posts: 846
|
| Posted: Sat May 14, 2011 12:38 pm Post subject: Re: Buchempfehlung zur formalen Verifikation von Programmen |
|
|
| manuels wrote: | | ich hab mich schon mehrmals gefragt, wie und mit welchen Tools, Computerprogramme formal verifiziert werden. |
Vorwiegend mit Brain 1.0. 
Darauf einzugehen ist nicht ganz einfach, weil ich nicht weiß, welche math. Vorbildung Du hast und welcher Bereich Dich interessiert. Es gibt zig Methoden, Programmeigenschaften zu verifizieren. Du kannst schon vorher das mathematische Modell Deiner Lösung auf bestimmte Eigenschaften prüfen (Model Checker, Process Kalküle), zB. das Protokoll einer Ampelanlage, ob nie zwei kreuzende Fahrbahnen gleichzeitig grün erhalten. Wenn Du dann sicher bist, dass Hardware und Compiler (für beides gibt es auch Verifikationsprojekte) und Protokolle funktionieren, stehst Du vor dem eigentlichen Problem. Entweder Du formulierst Deine Algorithmen und Beweise und generierst die Software (Coq), benutzt Spezifikationssprachen (PVS) oder musst ein Modell für Deine Sprache finden. Bei objektorientierten kann das schwierig werden (Cardelli), man benutzt heute vorwiegend Methoden aus der Kategorientheorie und Coalgebren (Jacobs), bei funktionalen ist es einfacher und man kann sich einfacher Methoden aus der Typtheorie zu nutze machen. Für jede der Methoden braucht man ein breites Fundament aus Logik (zB. Modallogiken, Deduktionssysteme) und diskreter Mathematik. Anwendbar ist das Ganze heutzutage nur für gut spezifizierte kleinere Projekte (Microkerne, Steuerungen, einzelne Module). Etwas praxisnäher ist das sogen. symbolic/concolic testing (Klee) - man nimmt keine konkreten Werte, sondern symbolische, wandert die Pfade in einem Programm ab, hängt dabei versch. Eigenschaften an die Variablen und schaut, ob man damit Fehler (Pointerfehler, asserts...) herbeiführen kann. Ob sich das Programm so verhält, wie man will, weiß man dann natürlich nicht.
Wenn man von all dem keine Ahnung hat und nur eine ganz grobe Vorstellung haben möchte, würde ich empfehlen den (ziemlich alten) Hoare-Kalkül anzugucken und sich die Vorträge um Microsofts Spec# anzusehen. Im Allgemeinen findet man an den Unis Vorlesungsunterlagen, die die Themen abhandeln.
Edit: Mir fiel gerade ein, dass ich mal einen recht einsteigerfreundlichen Artikel gelesen habe: Verifying Red-Black Trees. Erwähnenswert sind noch die bekannten Petri Netze und die relativ "neue" Spieltheorie.
_________________
Je dümmer desto Gnome/KDE. |
|
| Back to top |
|
|
Knieper
l33t
Joined: 10 Nov 2005
Posts: 846
|
|
| Back to top |
|
|
manuels
Advocate
Joined: 22 Nov 2003
Posts: 2146
Location: Europe
|
| Posted: Tue Jun 28, 2011 9:56 pm Post subject: |
|
|
Entschuldigung, dass ich mich jetzt erst melde. War schon lang nicht mehr im Gentoo Forum.
Hmm, ok. Am liebsten hätte ich wohl solche Verifikationen:
| Code: | for(int i = 0; i < A.rows(); ++i)
#verify: only access A.row(i)
A.row()*x = b;
|
Ich hoffe man versteht, was gemeint ist: Ich möchte in dem Loop verifizieren, dass nur auf die i-te Zeile der Matrix A zugegriffen wird.
_________________
Build your own live cd with catalyst 2.0! |
|
| Back to top |
|
|
Necoro
Veteran
Joined: 18 Dec 2005
Posts: 1912
Location: Germany
|
| Posted: Tue Jun 28, 2011 10:04 pm Post subject: |
|
|
| manuels wrote: | | Entschuldigung, dass ich mich jetzt erst melde. War schon lang nicht mehr im Gentoo Forum. |
Deswegen kann man ja Topics beobachten, auf dass man Mails bekommt wenn sich an denen was ändert. So kann man einige wichtige Sachen im Auge behalten ohne immer das ganze Forum durchforsten zu müssen.
| Quote: | Hmm, ok. Am liebsten hätte ich wohl solche Verifikationen:
| Code: | for(int i = 0; i < A.rows(); ++i)
#verify: only access A.row(i)
A.row()*x = b;
|
Ich hoffe man versteht, was gemeint ist: Ich möchte in dem Loop verifizieren, dass nur auf die i-te Zeile der Matrix A zugegriffen wird. |
Mhm - für solche Eigenschaften würde ich in der Tat auch auf "statische Codeanalyse" tippen -- zu mindestens haben wir sowas im Rahmen der Vorlesung "Programmoptimierung" damit gemacht. Allein: Dies wird wohl nicht für den allgemeinen Fall gehen -- aber einer gewissen Komplexität und Pointer-Herumschubserei kann das wohl an seine Grenzen kommen.
/edit: Als Buchempfehlung für den theoretischen Hintergrund würde ich evtl mal das Buch von Flemming Nielson in den Raum stellen
_________________
Inter Deum Et Diabolum Semper Musica Est. |
|
| Back to top |
|
|
Knieper
l33t
Joined: 10 Nov 2005
Posts: 846
|
| Posted: Sat Aug 06, 2011 9:12 am Post subject: |
|
|
| manuels wrote: | Hmm, ok. Am liebsten hätte ich wohl solche Verifikationen:
| Code: | for(int i = 0; i < A.rows(); ++i)
#verify: only access A.row(i)
A.row()*x = b;
|
Ich hoffe man versteht, was gemeint ist: Ich möchte in dem Loop verifizieren, dass nur auf die i-te Zeile der Matrix A zugegriffen wird. |
Ich kann mit dem Beispiel leider nichts anfangen. Eine Multiplikation auf der linken Seite einer Zuweisung und der Nachweis, dass nur über einen Index zugegriffen wird, dessen Variable nicht mehr auftaucht?! Für Matrizen und dergleichen sind Dependent Types wie in ATS oft ganz hilfreich, mein Fall sind sie nicht so ganz...
_________________
Je dümmer desto Gnome/KDE. |
|
| Back to top |
|
|
|
|
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
|
|
Deutsches Forum (German) 
