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