+ All Categories
Home > Documents > Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Date post: 02-Feb-2016
Category:
Upload: avi
View: 30 times
Download: 1 times
Share this document with a friend
Description:
Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement. Prof. Dr. Holger Schlingloff Institut für Informatik der Humboldt Universität und Fraunhofer Institut für Rechnerarchitektur und Softwaretechnik. Hinweise. - PowerPoint PPT Presentation
30
8.2.2006 Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement Prof. Dr. Holger Schlingloff Institut für Informatik der Humboldt Universität und Fraunhofer Institut für Rechnerarchitektur und Softwaretechnik
Transcript
Page 1: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

8.2.2006

Software-Engineering IIEingebettete Systeme, Softwarequalität, Projektmanagement

Prof. Dr. Holger SchlingloffInstitut für Informatik der Humboldt Universität

und

Fraunhofer Institut für Rechnerarchitektur und Softwaretechnik

Page 2: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 2H. Schlingloff, Software-Engineering II 8.2.2006

Hinweise

•Nochmal Werbung:Blockseminar im Sommersemester

„spezifikationsbasierter Softwaretest“(Vorbespr. + Sa., 10.6. und Sa., 17.6. 2006 ganztägig)

•Ab Sommer neue Jobs bei FraunhoferEU-Projekt „Evolutionäre Testerzeugung“

•Fr.: Automotive Software Engineering III•nächste Wo. Freitag letzte Vorlesung

Page 3: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 3H. Schlingloff, Software-Engineering II 8.2.2006

Verifikation: Hoare-Logik

•Aus dem Grundstudium bekannt?

•Kalkül zum Beweis der partiellen Korrektheit von (imperativen) Programmen

•Anwendbar z.B. auf C ohne dynamische Speicherverwaltung

•Erweiterungen für parallele Programme

•ToolunterstützungDarstellung folgt www1.isti.cnr.it/~bolognesi/Siena/Lucidi0102/16-HoareLogic.ppt

Page 4: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 4H. Schlingloff, Software-Engineering II 8.2.2006

While-Programme

•Zuweisungen: y:=t

•Komposition: S1; S2

• if-then-else: if e the S1 else S2 fi

•while: while e do S od

• for, repeat

•switch

•goto

Page 5: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 5H. Schlingloff, Software-Engineering II 8.2.2006

Beispiel: ggT (größter gem. Teiler)

{x1>0 /\ x2>0}y1:=x1;y2:=x2;while ¬(y1=y2) do if y1>y2 then y1:=y1-y2 else y2:=y2-y1 fiod{y1=ggT(x1,x2)}

Page 6: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 6H. Schlingloff, Software-Engineering II 8.2.2006

Warum funktioniert das?

Angenommen y1 und y2 sind nichtnegative Integer.

• Wenn y1>y2 dann ggT(y1,y2)=ggT(y1-y2,y2)• Wenn y2>y1 dann ggT(y1,y2)=ggT(y1,y2-y1)• Wenn y1=y2 dann ggT(y1,y2)=y1=y2

{ggT(y1,y2)=k /\ y1>0 /\ y2>0 /\ y1>y2}y1:=y1-y2

{ggT(y1,y2)=k /\ y1>0 /\ y2>0}

Page 7: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 7H. Schlingloff, Software-Engineering II 8.2.2006

{p[t/y]} y:=t {p}Beispiele:

{y+5=10} y:=y+5 {y=10}{y+y<z} x:=y {x+y<z}{2*(y+5)>20} y:=2*(y+5) {y>20}

Begründung: Setze p mit y’ statt y, und füge die Bedingung y’=t hinzu. Ersetze y’ durch t.

Im Beispiel gilt: {ggT(y1-y2,y2)=k /\ y1-y2>0 /\ y2>0}

y1:=y1-y2 {ggT(y1,y2)=k /\ y1>0 /\ y2>0}

Zuweisungsaxiom

Page 8: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 8H. Schlingloff, Software-Engineering II 8.2.2006

Vorwärtsrechnung

{p} y:=t {?}

Regel: Setze für ? ein (p /\ y=t), wobei y in p und t durch y’ ersetzt wird, eliminiere y’.

{y>5} y:=2*(y+5) {?} {p} y:=t {y’ (p[y’/y] /\ t[y’/y]=y)}(y’>5 /\ y=2*(y’+5)) y>20

Page 9: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 9H. Schlingloff, Software-Engineering II 8.2.2006

Kompositionsregel

{p} S1 {r}, {r} S2 {q} {p} S1;S2 {q}Beispiel: Voraussetzungen1. {x+1=y+2} x:=x+1 {x=y+2}2. {x=y+2} y:=y+2 {x=y}ergibt {x+1=y+2} x:=x+1; y:=y+2 {x=y}

Page 10: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 10H. Schlingloff, Software-Engineering II 8.2.2006

{p} S1 {r}, {r} S2 {q} {p} S1;S2 {q}

{x1>0 /\ x2>0} y1:=x1{ggT(x1,x2)=ggT(y1,x2) /\ y1>0 /\ x2>0}

{ggT(x1,x2)=ggT(y1,x2) /\ y1>0 /\ x2>0} y2:=x2{ggT(x1,x2)=ggT(y1,y2) /\ y1>0 /\ y2>0}

{x1>0 /\ x2>0} y1:=x1 ; y2:=x2{ggT(x1,x2)=ggT(y1,y2) /\ y1>0 /\ y2>0}

weitere Beispiele

Page 11: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 11H. Schlingloff, Software-Engineering II 8.2.2006

{p /\ e} S1 {q}, {p /\ ¬e} S2 {q} {p} if e then S1 else S2 fi {q}

Beispiel:

p sei ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0 /\ ¬(y1=y2)

q sei ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0

{p /\ y1>y2} y1:=y1-y2 {q}, {p /\ ¬y1>y2} y2:=y2-y1 {q}

{p} if y1>y2 then y1:=y1-y2 else y2:=y2-y1 fi {q}

If-then-else-Regel

Page 12: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 12H. Schlingloff, Software-Engineering II 8.2.2006

While-Regel

_______{p /\ e} S {p}_______ {p} while e do S od {p /\ ¬e}

Beispiel:

S sei if y1>y2 then y1:=y1-y2 else y2:=y2-y1 fi

{ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0 /\ ¬(y1=y2)} S {ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0}______

{p} while ¬(y1=y2) do S od {p /\ y1=y2}

Page 13: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 13H. Schlingloff, Software-Engineering II 8.2.2006

Implikationsregeln

•Verstärkung einer Voraussetzung rp, {p} S {q} {r} S {q}

•Abschwächung einer Konsequenz {p} S {q}, qr {p} S {r}

Page 14: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 14H. Schlingloff, Software-Engineering II 8.2.2006

Wir wollen beweisen{x1>0 /\ x2>0} y1:=x1

{ggT(x1,x2)=ggT(y1,x2) /\ y1>0 /\ x2>0}

Verstärkungsregel:x1>0 /\ x2>0 ggT(x1,x2)=ggT(x1,x2) /\ x1>0 /\ x2>0

Zuweisungsregel:{ggT(x1,x2)=ggT(x1,x2) /\ x1>0 /\ x2>0} y1:=x1 {ggT(x1,x2)=ggT(y1,x2) /\ y1>0 /\ x2>0}

Anwendung der Implikationsregel

Page 15: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 15H. Schlingloff, Software-Engineering II 8.2.2006

Noch‘n Beispiel

Beispiel:

{ggT(y1,y2)=k /\ y1>0 /\ y2>0 /\ y1>y2} {ggT(y1-y2,y2)=k /\ y1-y2>0 /\ y2>0}

{ggT(y1-y2,y2)=k /\ y1-y2>0 /\ y2>0} y1:=y1-y2 {ggT(y1,y2)=k /\ y1>0 /\ y2>0}

ergibt

{ggT(y1,y2)=k /\ y1>0 /\ y2>0 /\ y1>y2} y1:=y1-y2 {ggT(y1,y2)=k /\ y1>0 /\ y2>0}

Page 16: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 16H. Schlingloff, Software-Engineering II 8.2.2006

Zusammensetzung zum Programm

{x1>0 /\ x2>0} y1:=x1; y2:=x2; {ggT(x1,x2)=ggT(y1,y2) /\ y1>0 /\ y2>0} while ¬(y1=y2) do {ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0 /\ ¬(y1=y2)} if y1>y2 then {ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0 /\ ¬(y1=y2) /\ y1>y2} y1:=y1-y2 {ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0} else {ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0 /\ ¬(y1=y2) /\

¬y1>y2} y2:=y2-y1 {ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0} fi {ggT(y1,y2)=ggT(x1,x2) /\ y1>0 /\ y2>0} od {ggT(x1,x2)=ggT(y1,y2) /\ y1>0 /\ y2>0 /\ y1=y2}

Page 17: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 17H. Schlingloff, Software-Engineering II 8.2.2006

Noch nicht ganz fertig

{x1>0 /\ x2>0} y1:=x1; y2:=x2; while ¬(y1=y2) do if y1>y2 then y1:=y1-y2 else y2:=y2-y1 fi od {ggT(x1,x2)=ggT(y1,y2) /\ y1>0 /\ y2>0 /\

y1=y2}

Aber wir wollten zeigen:{x1>0 /\ x2>0} Prog {y1=ggT(x1,x2)}

Page 18: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 18H. Schlingloff, Software-Engineering II 8.2.2006

Abschwächungsregel

{x1>0/\x2>0} Prog{ggT(x1,x2)=ggT(y1,y2) /\ y1>0 /\ y2>0 /\ y1=y2}

Abschwächung{ggT(x1,x2) = ggT(y1,y2) /\ y1>0 /\ y2>0 /\

y1=y2} y1=ggT(x1,x2)

Daher{x1>0 /\ x2>0} Prog {y1=ggT(x1,x2)}

Page 19: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 19H. Schlingloff, Software-Engineering II 8.2.2006

Erweiterungen

•Totale Korrektheit (Terminierung)•Felder•Prozeduren, Subroutinen•Zeiger (aber keine dynamischen

Strukturen)•Parallele Programme, Interferenzfreiheit•Fairness•…

•Werkzeugunterstützung, z.B. Isabelle

Page 20: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 20H. Schlingloff, Software-Engineering II 8.2.2006

ein Beispiel aus der Praxis

Page 21: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 21H. Schlingloff, Software-Engineering II 8.2.2006

Pause!

Page 22: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 22H. Schlingloff, Software-Engineering II 8.2.2006

Modellprüfung

• Überprüfung eines formalen Modells des Systems gegenüber einer formalen Spezifikation der Anforderungen

• vollautomatisch für zustandsendliche Systeme

• Modellierung: Automaten, Petrinetze, StateCharts, SDL, …• Spezifikation: temporale Logik, Erreichbarkeit,

Verklemmungsfreiheit, …

Page 23: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 23H. Schlingloff, Software-Engineering II 8.2.2006

Beispiel (SMV)

Page 24: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 24H. Schlingloff, Software-Engineering II 8.2.2006

Computation Tree Logic CTL

• Formelsprache zur Beschreibung von Eigenschaften (paralleler) Programme

• Basis: Aussagenlogik atomare Aussagen, boolesche Verknüpfungen

• Zusätzlich: temporale Operatoren AG: „für alle Abläufe gilt global“ EF: „es gibt einen Ablauf mit irgendwann“ AX: „für alle möglichen nächsten Schritte“ EX: „es gibt einen nächsten Schritt“ AU: „für alle Abläufe solange bis“ (zweistellig) EU: „es gibt einen Ablauf solange bis“ (zweistellig)

Page 25: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 25H. Schlingloff, Software-Engineering II 8.2.2006

Bedeutung

Page 26: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 26H. Schlingloff, Software-Engineering II 8.2.2006

Beispiele

• Invarianzen x ist immer kleiner als 7: AG (x<7) Es kommt zu keinem Absturz: AG !crash Das Ergebnis ist immer 3: AG (stop erg=3)

• Lebendigkeit Terminierung: AF stop Aushungerungsfreiheit: AG AF eating

• Eventualitäten mögliche Nichtterminierung: EG !stop Rücksetzbarkeit: AG EF init Synchronisationsproblem: EF (request & AG !grant)

• Synchronisation Initialisierung (!read_x AU write_x) Race Condition (!write_P2 AU write_P1)

Page 27: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 27H. Schlingloff, Software-Engineering II 8.2.2006

bekannte Model-Checker

•SMV, nuSMV, Cadence SMV (CTL)•SPIN, COSPAN (LTL)•UPPAAL, Kronos, Rabbit (Realzeit)•HyTech (hybride Systeme)•CBMC (bounded Model Checker for C/C+

+ programs) • Java Pathfinder (für Java Bytecode)

NASA, seit Mitte 2005 open sourcehttp://javapathfinder.sourceforge.net/

Page 28: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 28H. Schlingloff, Software-Engineering II 8.2.2006

Java Pathfinder

• Historie Übersetzung von Java Bytecode nach Promela

(Automaten-Beschreibungssprache) LTL-ModelChecker SPIN

• Aktuell „abstrakte JVM“, die Bytecode symbolisch ausführt Fokus auf Sicherheitseigenschaften (deadlock usw.) Zustandsraumexplosion beherrscht durch

- konfigurierbare Suchstrategien- Zustandsraumreduktionsverfahren (PO Reduction,

Abstraction)- effiziente Zustands-Speicherverfahren (MD5-hashing)

Erweiterbarkeit

Page 29: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 29H. Schlingloff, Software-Engineering II 8.2.2006

Performance

• Programme bis 10 KLOC Bytecode• ~103-104 Zustände/sec analysierbar• ~106-107 Zustände speicherbar (bei 512 MB RAM)• virtueller Speicher kaum nutzbar

Page 30: Software-Engineering II Eingebettete Systeme, Softwarequalität, Projektmanagement

Folie 30H. Schlingloff, Software-Engineering II 8.2.2006

Beispiel

• Abstraktion der Variablen count neues Boolean für

count==event1.count

• Synchronisationsfehler if (count ==…) wird wahr dann signal_event dann unbedingtes wait


Recommended