Transcript
Überblick
Verlässliche Echtzeitsysteme Übungen zur Vorlesung
1
Abstrakte Interpretation mit Astrée
2
Aufgabenstellung
3
Softwareentwurf
Florian Franzmann, Martin Hoffmann, Isabella Stilkerich Friedrich-Alexander-Universität Erlangen-Nürnberg Lehrstuhl Informatik 4 (Verteilte Systeme und Betriebssysteme) http://www4.cs.fau.de
15. Mai 2013
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
1 – 45
Astrée [1]
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
2 – 45
Astrée weist nach
Ziel: Nachweis der Abwesenheit von Laufzeitfehlern
Überschreitung von Array-Grenzen
findet alle potentiellen Laufzeitfehler
Ganzzahldivision durch Null
leider auch falsch-positive ; wegen Gödelschem Unvollständigkeitstheorem
ungültige Dereferenzierung, arithmetische Überläufe
Jedes hinreichend mächtige formale System ist entweder widersprüchlich oder unvollständig.
ungültige Gleitkommaoperationen dass Code nicht erreichbar ist
Programm ist korrekt, wenn
Lesezugriff auf nicht initialisierte Variabeln
Astrée keine Alarme meldet
Verletzung benutzerdefinierter Zusicherungen ; assert()
oder für alle Alarme nachgewiesen, dass falsch-positiv
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
3 – 45
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
4 – 45
Was Astrée nicht kann
Einschränkungen
Astrée nimmt an, dass als Einschränkungen gelten:
Astrée kann nicht umgehen mit
1. der C99-Standard
Rekursionen
2. implementierungsabhängiges Verhalten Größe von Datentypen Gleitkommastandard ...
dynamischem Speicher ; kein malloc()
3. benutzerdefinierte Einschränkungen z. B. ob statische Variablen mit 0 initialisiert werden
Aber das will man im Echtzeitbereich ja sowieso nicht haben ,
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
4. außerdem benutzerspezifizierte Zusicherungen
5 – 45
Franzmann, Hoffmann, Stilkerich
Benutzerdefinierte Zusicherungen 1 2 3
wird nicht weiter überprüft
6 – 45
# if 0 # include < astree .h > // Astree - Makros abschalten # endif
4 5
Analyzer warnt, falls B nie wahr
6 7 8
__ASTREE_assert((B))
9 10
alterntiv auch assert()
11
Analyzer erzeugt Alarm, falls B nicht immer wahr
13
12
float filter ( Alpha_State *s , float val ) { __ASTREE_known_fact (( val == val )); __ASTREE_known_fact (( -10.0 f < val && val < 10.0 f )); __ASTREE_known_fact (( s - > val == s - > val )); __ASTREE_known_fact (( FLT_MIN < s - > val && s - > val < FLT_MAX )); __ASTREE_assert ((0 < s - > alpha )); __ASTREE_assert (( s - > alpha < 1)); float residual = val - s - > val ; s -> val = s - > val + s - > alpha * residual ;
14
B kann nicht von der Form e1 ? e2 : e3 sein
15 16
__ASTREE_assert (( s - > val == s - > val )); // ... return s - > val ;
17
Analyzer nimmt danach an, dass B wahr ist
18 19
die doppelten Klammern sind wichtig! VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
Beispiel
__ASTREE_known_fact((B))
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
20
7 – 45
} Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
8 – 45
Variable auf „unbekannter Wert“ setzen
volatile __ASTREE_volatile_input((V))
zeigt an, dass V sich jederzeit ändern kann __ASTREE_modify((V1, ..., Vn)) __ASTREE_volatile_input((Vp, r))
zeigt an, dass Variablen V1 bis Vn unbekannten Wert haben ; braucht man um Stubs zu bauen
p ist Pfad in der Variablen, z. B. V.a[3-4].b ; Variable V, Arrayelemente a[3] und a[4], Struct-Element b [i] ; Element i [i-j] ; Elemente i bis j [] ; alle Elemente r schränkt Wertebereich ein [i, j] ; von i bis j
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
9 – 45
Analyse untersuchen
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
10 – 45
Astrée verwenden
__ASTREE_analysis_log(())
Astrée im CIP:
gibt Zustand der Analyse an dieser Stelle aus
% /proj/i4ezs/tools/astree_c-13.04/bin/astreec
Anmeldung mit Benutzername und Passwort
__ASTREE_log_vars((V1, ..., Vn))
zeigt Zustand der Analyse in Bezug auf einzelne Variabeln an
; Passwort wird bei der ersten Anmeldung festgelegt gute merken ,
Dokumentation unter /proj/i4ezs/tools/astree_c-13.04/share/astree_c/help
__ASTREE_print(("text"))
gibt Text aus
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
11 – 45
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
12 – 45
Anmelden Host Port Username Passwort
Projekt anlegen
faui48d.informatik.uni-erlangen.de 36000 nach Belieben bei der ersten Anmeldung festlegen und gut merken
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
13 – 45
Präprozessoreinstellungen
Quelldateien zum Projekt hinzufügen
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
14 – 45
Table of Contents
Include-Pfade festlegen
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Abstrakte Interpretation mit Astrée
15 – 45
1
Abstrakte Interpretation mit Astrée
2
Aufgabenstellung
3
Softwareentwurf
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung
16 – 45
Aufgabenstellung
Festkommaarithmetik – Q-Notation kaum ein Mikrocontroller hat eine Gleitkommaeinheit ; Festkommaarithmethik mit Ganzzahlen
einfaches Filter implementieren
Zahlenformat häufig in Q-Notation [8] angegeben Qm.n ; Festkommazahl mit
Korrektheit der Implementierung nachweisen
m Bit vor dem Komma n nach dem Komma und einem Vorzeichenbit Wertebereich: [−2m , 2m − 2−n ] Auflösung: 2−n
; Astrée
zunächst mit Gleitkommaarithmetik
; float
dann für einen 8 Bit-Mikrocontroller mit Festkommaarithmetik
Implementierung als Integer ; welches Q-Format Verwendung findet, ist dem Anwendungsprogrammierer überlassen
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung
17 – 45
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung – Festkommaarithmetik
Q-Notation – Beziehung zu Gleitkommazahlen
Operationen – Addition/Subtraktion
von Gleitkomma nach Qm.n
Addition und Subtraktion wie bei Ganzzahlen
1. Multiplikation mit 2n
18 – 45
Addition
2. Runden auf die nächste Ganzzahl
1 2 3
int8_t a = ...; int8_t b = ...; int8_t result = a + b ;
von Qm.n nach Gleitkomma Subtraktion
1. Umwandlung in Gleitkommazahl ; cast
1
2. Multiplikation mit 2−n
2 3
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung – Festkommaarithmetik
19 – 45
int8_t a = ...; int8_t b = ...; int8_t result = a - b ;
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung – Festkommaarithmetik
20 – 45
Operationen – Multiplikation/Division
Größe von Datentypen bestimmen I
braucht Zwischenergebnis von doppelter Bitbreite
% cat test.c
Multiplikation 1 2 3 4 5 6
# define K (1 int8_t a = int8_t b = int16_t temp = temp += int8_t result =
<< ( n - 1)) ...; ...; ( int16_t ) a * ( int16_t ) b; K; temp >> n ;
1 2
# include < stddef .h >
3
static size_t short_size static size_t ushort_size static size_t int_size static size_t uint_size static size_t long_size static size_t ulong_size static size_t longlong_size static size_t float_size static size_t double_size static size_t longdouble_size static size_t ptr_size static size_t fptr_size void main ( void ) {}
4 5 6 7 8 9 10 11
Division 1 2 3 4 5
int8_t int8_t int16_t
a = b = temp = temp += int8_t result =
Franzmann, Hoffmann, Stilkerich
12
...; ...; ( int16_t ) a << n ; b / 2; temp / b ;
VEZS (15. Mai 2013)
Aufgabenstellung – Festkommaarithmetik
13 14 15
= = = = = = = = = = = =
sizeof ( short ); sizeof ( unsigned short ); sizeof ( int ); sizeof ( unsigned int ); sizeof ( long ); sizeof ( unsigned long ); sizeof ( long long ); sizeof ( float ); sizeof ( double ); sizeof ( long double ); sizeof ( void *); sizeof ( void (*)( void ));
% avr-gcc -O0 -S -c test.c
21 – 45
Größe von Datentypen bestimmen II
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung – Größe von Datentypen
22 – 45
VEZS (15. Mai 2013)
Aufgabenstellung – Größe von Datentypen
24 – 45
ABI ABI festlegen
% cat test.s
... 1 2 3 4 5 6
short_size : .word 2 ← short zwei Byte lang .subsection 2 .align 2 .type ushort_size , @object .size ushort_size ,4
...
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung – Größe von Datentypen
23 – 45
Franzmann, Hoffmann, Stilkerich
α-β-Filter [4]
Beispiel α-β-Filterung 4 Regler
α-β-Filter
Sensor
Eingang Ausgang
3
Aktor
−→
2 ω rad/s
Rauschunterdrückungsfilter geeignet zur Schätzung von physikalischen Größen mit Ableitung 6= 0 z. B. Position eines Flugzeugs, Lagewinkel . . . im I4Copter
0 -1
liefern Sensoren häufiger Werte als diese später verarbeitet werden ; α-β-Filter für Ratenwandlung verwendet ; nutzt gewonnene Information vollständig
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
1
Aufgabenstellung – α-β-Filter
-2 0
25 – 45
Franzmann, Hoffmann, Stilkerich
1.5
2
2.5
3
VEZS (15. Mai 2013)
Aufgabenstellung – α-β-Filter
26 – 45
Filterparameter
wird für jeden Messwert ausgeführt
T Abtastintervall ; in welchem Zeitabstand gemessen wird
y [κ]: Eingabewert für Abtastschritt κ xˆ [κ]: Schätzung der Messgröße zum Abtastschritt κ
σw2 Prozessvarianz ; wie lebhaft der gemessene Prozess ist
T Abtastintervall, α, β Filterparameter ˆ˙ Initialisierung: z. B. xˆ [0] = x[0] =0 r [κ] = y [κ] − xˆ [κ − 1] ˆ˙ ˆ˙ − 1] + β · r [κ] x[κ] = x[κ T ˆ˙ xˆ [κ] = xˆ [κ − 1] + T · x[κ] + α · r [κ]
; Schätzfehler
(1)
; Schätzwert
(3)
; 1. Ableitung
(2)
sinnvolle Werte für α und β? Literatur beschreibt viele Verfahren ; hier beispielhaft nur eines [6, 5] VEZS (15. Mai 2013)
1
t/s−→
Filteralgorithmus
Franzmann, Hoffmann, Stilkerich
0.5
Aufgabenstellung – α-β-Filter
27 – 45
σv2 Rauschvarianz ; wie verrauscht das Signal ist
σw T 2 σv √ 4 + λ − 8λ + λ2 θ= 4 α = 1 − θ2 √ β = 2 (2 − α) − 4 1 − α λ=
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
; Tracking Index
(4)
; Dämpfungsparameter
(5)
; Gewicht für Ableitung
(7)
; Gewicht für Wert
Aufgabenstellung – α-β-Filter
(6)
28 – 45
Sinnvolle Wertebereiche
Korrektheitsbedingung Filter ist nur dann korrekt, wenn es auch stabil ist ; für wertbegrenzte Eingabe erfolgt wertbegrenzte Ausgabe [7] ; für Eingabe 0 geht der Filterausgang asymptotisch gegen 0
Erfahrungen mit dem I4Copter haben gezeigt, dass sich die Parameter in folgenden Bereichen bewegen: Abtastintervall T ∈ (0 . . . 1] Prozessvarianz σw2 ∈[0.5 . . . 2.0] Rauschvarianz σv2 ∈ 10−3 . . . 10−1 Wert y [κ] ∈ [−10 . . . 10]
α-β-Filter stabil, wenn gilt 0<α≤1
(8)
0<β≤2
(9)
0 < 4 − 2α − β
(10)
Außerdem: laut [2] Rauschunterdrückung nur dann, wenn
; Korrektheit mindestens für diese Wertebereiche zeigen!
0<β<1
(11)
andernfalls wird das Rauschen verstärkt! Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung – α-β-Filter
29 – 45
Literatur I
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Aufgabenstellung – α-β-Filter
30 – 45
Literatur II
[1] AbsInt Angewandte Informatik GmbH. The Static Analyzer Astrée, April 2012. [2] C. Frank Asquith. Weight selection in first-order linear filters. Technical report, Army Intertial Guidance and Control Laboratory Center, Redstone Arsenal, Alabama, 1969.
[6] Paul R. Kalata. The tracking index: A generalized parameter for α-β and α-β-γ target trackers. IEEE Transactions on Aerospace and Electronic Systems, AES-20(2):174–181, mar 1984.
[3] Grady Booch. Software Engineering with Ada. The Benjamin/Cummings Publishing Company, Inc., 2nd edition, 1987.
[7] Richard G. Lyons. Understanding Digital Signal Processing. Prentice Hall, 3rd edition, 11 2010.
[4] Eli Brookner. Tracking and Kalman Filtering Made Easy. Wiley-Interscience, 1st edition, 4 1998.
[8] Erick L. Oberstar. Fixed-point representation & fractional math. Technical report, Oberstar Consulting, August 2007.
[5] E. Gray, J. and W. Murray. A derivation of an analytic expression for the tracking index for the alpha-beta-gamma filter. IEEE Trans. on Aerospace and Electronic Systems, 29:1064–1065, 1993.
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Literatur
31 – 45
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Literatur
32 – 45
Table of Contents
1
Ziele des Softwareentwurfs Modifizierbarkeit: lokale Veränderbarkeit ; Änderungen an Anforderungen umsetzbar ; Fehler korrigierbar
Abstrakte Interpretation mit Astrée
Effizienz: optimaler Betriebsmittelbedarf wird häufig zu früh berücksichtigt
2
Aufgabenstellung
3
Softwareentwurf
Verlässlichkeit: über lange Zeit Funktionsfähigkeit ohne menschlichen Eingriff gutmütiges Ausfallverhalten muss von Anfang an eingeplant sein! Verständlichkeit: Isolierung von Daten Algorithmen
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
33 – 45
Prinzipien des Softwareentwurfs
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
34 – 45
Fragestellung
Abstraktion: wichtige Details hervorheben
Wie komme ich von der Beschreibung zur Software?
Kapselung: unnötige Details verbergen
Objektorientierter/Objektbasierter Entwurf [3]
Einheitlichkeit: konsistente Notation
1. identifiziere Objekte und deren Attribute 2. identifiziere Operationen jedes Objekts
Vollständigkeit: alle wichtigen Aspekte berücksichtigt
3. lege Sichtbarkeit fest
Testbarkeit: muss von Anfang an eingeplant werden
4. lege Objektschnittstellen fest 5. implementiere Objekte
C macht es einem hier nicht leicht ; disziplinierte Herangehensweise notwendig!
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
35 – 45
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
36 – 45
Beispielbeschreibung – α-Filter
1. Objekte und Attribute identifizieren Herangehensweise:
x[κ] Schätzung, α Filterparameter, y [κ] Messwert Initialisierung: xˆ [0] = 0
Hauptwortextraktion aus Anforderungsdokument für kleinere Probleme: Intuition
Filterschritt: r [κ] = y [κ] − xˆ [κ − 1] xˆ [κ] = xˆ [κ − 1] + α · r [κ]
Was ist das Objekt? ; Filter
(12)
Attribute? Welche Information brauche ich für jeden Filterschritt?
(13)
Schätzung aus der Vorrunde xˆ [κ − 1] Filterparameter α aktuellen Messwert y [κ] ; kein Zustand, kommt von aussen
Optimale Parameter (σw2 Prozessvarianz, T Abtastintervall, σv2 Rauschvarianz): λ = σw · T 2 /σv p α = −λ2 + λ4 + 16λ2 /8
Vorläufige Objektschablone
(14) 1
(15)
2 3 4
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
37 – 45
typedef struct _Alpha_Filter { AF_Value_t x ; AF_Value_t alpha ; } Alpha_Filter ; Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
2. Operationen identifizieren
3. Sichtbarkeit festlegen
Herangehensweise:
in modernen Programmiersprachen private, public, . . .
Verbenextraktion für kleinere Probleme: Intuition
38 – 45
in C nur eingeschränkt möglich modulintern vs. modulextern
Leben eines Objekts: 1. Initialisierung ; Betriebsmittel anfordern 2. Verwendung 3. Beseitigung ; Betriebsmittel freigeben
Leitfaden: möglichst wenig sichtbar machen Was soll bei unserem Filter öffentlich sein? Initialisierung Filterschritt Schätzung abfragen
Was möchten Benutzer mit dem Filter machen? Filter initialisieren Filterschritt ausführen Schätzwert erfragen Betriebsmittelfreigabe nicht notwendig
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
alle anderen Operationen modulintern ; Hilfsfunktionen static 39 – 45
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
40 – 45
4. Schnittstelle festlegen
5. Implementierung – Header alpha_filter.h 1
zwischen Modul und Außenwelt
2
# ifndef ALPHA_FILTER_H_INCLUDED # define ALPHA_FILTER_H_INCLUDED
3
statische Semantik
4 5 6
Schnittstelle 1 2 3 4
7
void afilter_init ( Alpha_Filter * filter , AF_Value_t process_variance , AF_Value_t noise_variance , AF_Value_t sampling_interval );
8 9 10 11
5 6 7 8 9
12
void afilter_step ( Alpha_Filter * filter , AF_Value_t measurement );
13 15 16 17 18 19
VEZS (15. Mai 2013)
Softwareentwurf
3 4 5 6 7 8 9 10
Softwareentwurf
r [κ] = y [κ] − xˆ [κ − 1] xˆ [κ] = xˆ [κ − 1] + α · r [κ]
(17)
42 – 45
(19) (20)
(18)
alpha_filter.c 1
void afilter_init ( Alpha_Filter * filter , AF_Value_t process_variance , AF_Value_t noise_variance , AF_Value_t sampling_interval ) { filter - > x = 0; AF_Value_t l = sqrt ( process_variance ) * sampling_interval * sampling_interval / sqrt ( noise_variance ); filter - > alpha = ( - l * l + sqrtf ( l * l * l * l + 16.0 f * l * l )) / 8.0 f; } Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
5. Implementierung – Filterschritt
alpha_filter.c 2
AF_Value_t afilter_get_estimate ( Alpha_Filter * filter ); # endif // ALPHA_FILTER_H_INCLUDED
(16)
λ = σw · T 2 /σv p α = −λ2 + λ4 + 16λ2 /8
1
void afilter_step ( Alpha_Filter * filter , AF_Value_t measurement );
Franzmann, Hoffmann, Stilkerich
41 – 45
5. Implementierung – Initialisierung xˆ [0] = 0
void afilter_init ( Alpha_Filter * filter , AF_Value_t process_variance , AF_Value_t noise_variance , AF_Value_t sampling_interval );
14
AF_Value_t afilter_get_estimate ( Alpha_Filter * filter );
Franzmann, Hoffmann, Stilkerich
typedef float AF_Value_t ; typedef struct _Alpha_Filter { AF_Value_t x ; AF_Value_t alpha ; } Alpha_Filter ;
VEZS (15. Mai 2013)
Softwareentwurf
2 3 4 5
void afilter_step ( Alpha_Filter * filter , AF_Value_t measurement ) { AF_Value_t r = measurement - filter - > x ; filter - > x = filter - > x + filter - > alpha * r ; }
6 7 8 9 10
43 – 45
AF_Value_t afilter_get_estimate ( Alpha_Filter * filter ) { return filter - > x ; } Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Softwareentwurf
44 – 45
Fragen?
Franzmann, Hoffmann, Stilkerich
VEZS (15. Mai 2013)
Fragen?
45 – 45
