Verification of component-based embedded system designs

dok-tfk-titelsid.en.pdf......Page 1
Dr-sammanst.pdf......Page 307
thesis.pdf......Page 0
E......Page 3
M......Page 5
2.3.3 Theorem Proving 23......Page 7
5.3 Method Calls and Interfaces 64......Page 8
7.2 Objective and Assumptions 137......Page 9
9.6 Verification Methodology Roadmap 206......Page 10
11.3 Discussion 270......Page 11
12.2 Future Work 276......Page 12
PART I Preliminaries......Page 13
1.1 Motivation......Page 15
. They are part of a larger system (host system), hence the term embedded, with which they continuously or frequently interact. Usually, the embedded system serves as a control unit inside the host system.......Page 16
Figure 1.1: Productivity gap......Page 17
1.2 Problem formulation......Page 18
1.2.1 Component Verification......Page 19
. Theoretical framework. A theoretical framework underlying the proposed integration verification methodology has been developed.........Page 20
. Translation of SystemC into a Petri-net based design representation. Translating SystemC into a well-defined design representa.........Page 21
. Chapter 5 describes a translation mechanism from SystemC into the Petri-net based design representation which is used throughout the thesis.......Page 22
. Chapter 12 concludes the thesis and discusses possible directions for future work.......Page 23
2.1 Design of Embedded Systems......Page 25
Figure 2.1: Embedded systems design flow......Page 27
2.2.1 IP Provider......Page 28
Figure 2.2: Impact of IP generality on various other parameters [Gaj00]......Page 29
Figure 2.3: Two components interconnected by a glue logic......Page 30
Figure 2.4: Verification Intent Overview [Piz04]......Page 31
2.3.1 Model Checking......Page 33
2.3.2 Equivalence Checking......Page 34
(2.1)......Page 35
Figure 2.5: Simulation overview......Page 36
2.4 Verification of IP-based Designs......Page 37
(2.3)......Page 38
2.4.2 Modelling the Environment in the Property Formulas......Page 39
2.5 Remarks......Page 40
3.1 SystemC......Page 43
3.1.1 Processes......Page 44
3.1.3 Channels and Signals......Page 45
. Time: The process is declared ready again when the specified amount of simulated time has elapsed.......Page 46
3.2 The Design Representation: PRES+......Page 47
1. A token has values and timestamps, where is the value and is the timestamp. In Figure 3.1, the token in place has the value 4.........Page 48
5. The preset (postset ) of a transition is the set of all places from which there are arcs to (from) transition . Similar definitions can be formulated for the preset (postset) of places. In Figure 3.1, , , and .......Page 49
. A transition is enabled iff there is one token in each input place, there is no token in any of its output places and its guard is satisfied.......Page 50
Figure 3.2: Examples of the dynamic behaviour of PRES+......Page 51
Definition 3.3: Component. A component is a subgraph of the graph of the whole system such that:......Page 52
1. Two components , may only overlap with their ports (Definition 3.4), , where......Page 53
Definition 3.5: Interface. An interface of component is a set of ports where .......Page 54
3.3 Computation Tree Logic......Page 55
Figure 3.5: Illustration of different CTL formulas......Page 56
T......Page 59
Figure 4.1: Relationship between component and integration verification......Page 60
Figure 4.2: Component verification overview......Page 61
Figure 4.3: Integration verification overview......Page 62
Figure 4.4: Several examples of glue logics constellations......Page 63
Figure 4.5: Several ways how to view the glue logics illustrated in Figure 4.4 (c) and (e) respectively......Page 64
Figure 4.6: Overview of the proposed methodology......Page 66
PART II Component Verification......Page 69
S......Page 71
5.1 Related Work......Page 72
5.2 Basic Concepts......Page 73
Figure 5.1: Translation of statements and variables......Page 74
Figure 5.2: Example of an if statement......Page 75
5.3 Method Calls and Interfaces......Page 76
Figure 5.4: Translation of method calls......Page 77
2. Update all signals.......Page 79
3. Update signals.......Page 80
. in the current delta cycle (immediate)......Page 81
Figure 5.6: A scheduler......Page 82
Figure 5.7: The interface of an event......Page 84
Figure 5.8: An event......Page 85
Figure 5.9: Translation of a time-triggered wait statement......Page 86
Figure 5.10: Translation of an event-triggered wait statement......Page 87
. The method does not know which pid to put in mkimmready (actually the pid depends on which process has called the method)......Page 88
Figure 5.11: Invocation of a method containing a wait statement......Page 89
Figure 5.12: The interface of a signal......Page 90
Figure 5.13: Translation of a signal......Page 91
6.1.1 Overview of our Model Checking Environment......Page 93
Figure 6.1: Model checking environment overview......Page 94
Figure 6.2: A example PRES+ model to be translated into timed automata......Page 95
Figure 6.3: A system of timed automata corresponding to the PRES+ model in Figure 6.2......Page 96
6.1.2 Experimental results......Page 97
Packet switch......Page 98
15375.0......Page 99
4. Messages sent by a master will always eventually be read and acknowledged by a slave.......Page 100
6.1.3 Discussion......Page 101
6.2.1 Related Work......Page 102
6.2.2 Verification Strategy Overview......Page 104
Figure 6.4: Verification Strategy Overview......Page 105
(6.1)......Page 106
Definition 6.3: Total coverage. The total coverage (cov) (coverage for short) is computed by dividing the sum of activated assertions and fired transitions with the sum of the total number of assertions and transitions, as shown in Equation 6.4.......Page 107
6.2.4 Assertion Activation......Page 108
(6.8)......Page 109
Definition 6.5: . The function returning a set of activation sequences given an ACTL formula is recursively defined as:......Page 110
6.2.5 Stimulus Generation......Page 112
(6.10)......Page 113
Figure 6.7: The transition selection process......Page 114
6.2.6 Assertion Checking......Page 115
Figure 6.8: Part of an example monitor......Page 116
Figure 6.9: Assertion checking overview......Page 117
Figure 6.10: The assertion checking algorithm in the context of Figure 6.4......Page 118
Figure 6.11: Algorithm to check the timing aspect of an assertion......Page 120
Figure 6.12: Algorithm for finding monitor transitions fulfilling the expected output......Page 121
(6.13)......Page 122
(6.15)......Page 123
(6.19)......Page 124
(6.23)......Page 125
6.2.7 Coverage Enhancement......Page 126
Enhancing Transition Coverage......Page 127
Definition 6.6: Distance. Let be a marking, a set of values, U a universe containing all possible values which can occur in the .........Page 128
Figure 6.13: Example of computing distance......Page 130
Static Stop Criterion......Page 132
Figure 6.14: Relation between simulation length and validation time......Page 133
Dynamic Stop Criterion......Page 134
(6.26)......Page 135
Figure 6.15: Relation between simulation length and coverage......Page 137
(6.29)......Page 138
6.2.9 Experimental Results......Page 139
0.00......Page 140
PART III Integration Verification......Page 143
7.1 Explanatory Example......Page 145
Figure 7.1: A high level model of the GAP example......Page 146
Figure 7.2: Refined GAP model......Page 147
Figure 7.3: The glue logic between Radar and its Protocol......Page 148
. The components themselves are already verified.......Page 149
(7.2)......Page 150
Figure 7.4: A simple stub of the Protocol adapter......Page 151
Figure 7.5: Example for stub demonstration......Page 152
Figure 7.6: Stubs used in the example in Figure 7.5......Page 153
(7.6)......Page 154
7.4 Verification Methodology Roadmap......Page 156
Figure 7.7: The start of the roadmap......Page 157
8.1 Definitions......Page 159
Figure 8.1: Illustration of interface compatibility......Page 160
Definition 8.3: Observation. An observation is a set of events . Given observation and an interface , the restricted observation.........Page 161
Figure 8.2: Illustration of observations......Page 162
2. For any input observation of component , satisfying all requirements on ports not in , .......Page 163
Definition 8.6: Top-level interface. The top-level interface of a component , with respect to a glue logic , is the set of all p.........Page 164
Figure 8.3: A partial order of interfaces......Page 165
Figure 8.4: The models of the empty stubs......Page 166
8.3 Verification Environment......Page 167
Theorem 8.1: The partition precedence relation is a partial order.......Page 168
Definition 8.9: Environment. The environment corresponding to a partition with respect to a set of ports where , is defined as where each is the stub for interface , and is the empty stub attached to port .......Page 169
Figure 8.5: A few environments for the example in Figure 7.5......Page 170
Figure 8.6: Components and corresponding interfaces......Page 171
Definition 8.10: Surrounding. The surrounding of a glue logic , , is the part of the design not including or any component connected to , .......Page 172
Definition 8.11: Generalised operation. The generalised operation for component is the union of all operations for every possible input observation, .......Page 173
Definition 8.12: State sequence generator. A state, in this context, is a marking of ports. A state sequence generator is a func.........Page 174
(8.4)......Page 175
Theorem 8.4: Assume the partitions and , , a set of ports where , an initial marking on the ports in and a (T)ACTL formula, e.g. , also expressed only on the ports in . If for component , then it is also true that for component .......Page 176
1. The verification is unmanageable in the context defined above. This is the case when formula is expressed in terms of ports w.........Page 177
8.5.1 General Avionics Platform......Page 178
Table 8.1: Experimental results for GAP example......Page 179
Figure 8.10: Schematic view of the STB example......Page 180
Table 8.2: Experimental results for STB example......Page 182
Figure 8.11: Partition lattice in the STB example......Page 183
Figure 8.12: Continuation of the roadmap from Figure 7.7......Page 185
Figure 8.13: Roadmap when using top-level stubs, continuation from Figure 8.12......Page 186
Figure 8.14: Roadmap when using lower-level stubs on ACTL formulas, continuation from Figure 8.12......Page 187
Figure 8.15: Roadmap when using lower-level stubs on non-ACTL formulas, continuation from Figure 8.12......Page 188
C......Page 189
Theorem 9.1: Assume two environments and of the same set of components and , an initial marking and a (T)ACTL formula, e.g. expressed only on the ports of the stubs in and . If for component , then it is also true that for component .......Page 190
9.2 The Naïve Approach......Page 191
(9.2)......Page 192
9.3 Stub Generation Algorithm......Page 193
3. Compensation for the excluded parts of the component......Page 194
Figure 9.4: Algorithms for searching the dataflow......Page 195
Figure 9.5: The dataflow marking of the component in Figure 9.1......Page 196
1. Divergence node (e.g. , , and in Figure 9.5).......Page 197
Figure 9.6: Algorithms for identifying which parts of a component to include in the stub......Page 198
3. The node being visited is neither of the above.......Page 199
Figure 9.7: Algorithm for adding places and transitions to the resulting stub given a separation point......Page 200
Figure 9.8: The places and transitions in the automatically generated stub......Page 201
Definition 9.7: Join node. Assume a component and a stub . A node is a join node if and only if the corresponding node in the component has a node in its preset which is not in the stub .......Page 202
Figure 9.9: Example component and stub explaining the compensation of excluded parts......Page 203
(9.3)......Page 204
(9.8)......Page 205
Figure 9.10: An automatically generated stub......Page 206
9.3.4 Complexity Analysis......Page 207
9.4 Reducing Pessimism in Stubs......Page 208
Figure 9.11: An example system......Page 209
Figure 9.12: The pessimism reduction algorithm......Page 210
Figure 9.13: Auxiliary function for the pessimism reduction algorithm......Page 211
(9.9)......Page 212
9.4.1 Complexity Analysis......Page 213
Figure 9.15: The verified glue logic in the GAP example......Page 214
Table 9.1: Verification results and times for the GAP example......Page 215
9.5.2 Cruise controller......Page 216
Table 9.2: Verification results and times for the CCM example......Page 217
9.6 Verification Methodology Roadmap......Page 218
Figure 9.17: Continuation from Figure 7.7 when no stubs are provided by the designer......Page 219
Figure 9.18: Continuation of the roadmap from Figure 9.17......Page 220
Figure 9.19: Continuation of the roadmap from Figure 9.17 and Figure 9.18......Page 221
T......Page 223
Figure 10.1: Overview of the methodology presented in this chapter......Page 224
Figure 10.2: Petri-nets constructed ad hoc for the formula......Page 225
Table 10.1: Examples of (T)ACTL formulas and their normalisation......Page 226
4. Insertion of initial tokens......Page 227
(10.2)......Page 228
Table 10.2: Listing of all subsets of......Page 230
Definition 10.3: Atomic propositions. The set of atomic propositions in a formula is defined as . This function can also be lift.........Page 229
Definition 10.4: Port values. The set of in-port values of the set of elementary formulas is defined as . The set of out-port values is defined with respect to a particular out-port as , where .......Page 231
(10.4)......Page 232
1. , . If , then . If , then .......Page 233
Definition 10.7: Progress formulas. A progress formula is any elementary formula except atomic propositions. Assuming a set of elementary formulas , . This function can also be lifted to sets of sets of formulas, .......Page 234
Figure 10.3: The algorithm for creating the places in the resulting PRES+ model......Page 236
Definition 10.8: Set of U formulas. The set of U formulas in place is expressed as .......Page 237
Figure 10.5: Adding timers to a place......Page 238
Figure 10.6: Adding timers to the example model......Page 239
(10.5)......Page 240
Definition 10.12: Redundant elementary set. A set of elementary formulas is redundant with respect to a set of sets of elementary formulas , if and only if there exists a set , , with , , and and .......Page 241
No timer was added to the place......Page 242
Figure 10.7: The standard algorithm for adding the transitions belonging to place .......Page 243
Figure 10.9: Algorithm for finding the correct time delay interval of a transition......Page 245
Figure 10.10: The result of adding the transitions of place to the example formula......Page 247
Definition 10.14: Timer triggered formulas. The set of timer triggered formulas of a set of U formulas, , is defined as .......Page 248
Figure 10.11: The algorithm for adding transitions to a place with timers......Page 250
Figure 10.12: The result of adding the transitions of place to the example formula......Page 251
Figure 10.13: The algorithm for adding an initial token......Page 252
Figure 10.14: The resulting PRES+ model of the example formula......Page 253
Figure 10.15: The algorithm for generating a PRES+ model given an ACTL formula......Page 254
.......Page 255
Figure 10.16: The resulting PRES+ model of the formula......Page 256
.......Page 257
Figure 10.17: The resulting PRES+ model corresponding to progress formulas of the formula......Page 258
(10.8)......Page 259
.......Page 260
Figure 10.18: The resulting PRES+ model of the formula......Page 261
10.4 Verification Methodology Roadmap......Page 262
Figure 10.19: Continuation of the roadmap in Figure 9.19, useFormulas......Page 263
3. Speaker. The speaker receives voice signals from the receiver and converts them to sound.......Page 265
Figure 11.1: Overview model of the case study system, a mobile telephone design......Page 266
Figure 11.2: Models of components Buttons and Display......Page 267
11.1.2 Controller......Page 268
Figure 11.3: Model of the Controller component......Page 269
11.1.3 AMBA Bus......Page 270
Figure 11.4: Model of the Arbiter component......Page 271
Figure 11.5: Model of the Bus component......Page 272
Master functionality......Page 273
Figure 11.6: A model of the glue logic for the master functionality of the controller......Page 274
Slave functionality......Page 275
Figure 11.7: A model of the glue logic for the slave functionality of the controller......Page 276
Figure 11.8: The part of the system used to verify property 1 and property 2......Page 277
(11.1)......Page 278
Table 11.2: Verification results of property 2......Page 279
11.2.3 Property 3......Page 280
Table 11.3: Verification results of property 3......Page 281
11.3 Discussion......Page 282
PART IV Conclusions and Future Work......Page 283
12.1 Conclusions......Page 285
. The translation approach from SystemC to PRES+ (Chapter 5) would be strengthened if the result from the proposed translation p.........Page 288
[Bai03]......Page 291
[Cor00]......Page 292
[Gra97]......Page 293
[Kar02]......Page 294
[Loc91]......Page 295
[Swa97]......Page 296
[Wan93]......Page 297
Abbreviations......Page 299
Notation Description......Page 301
Notation Description......Page 302
Notation Description......Page 303
Notation Description......Page 304
Notation Description......Page 305