|
马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。
您需要 登录 才可以下载或查看,没有账号?注册
×
1 Introduction 1
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.4 Thesis Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.5 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2 Preliminaries 13
2.1 Uni¯ed Modeling Language (UML) . . . . . . . . . . . . . . . . . . . 13
2.1.1 Class Diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.1.2 Sequence Diagrams . . . . . . . . . . . . . . . . . . . . . . . . 16
2.2 Abstract State Machines (ASM) . . . . . . . . . . . . . . . . . . . . . 16
2.2.1 ASM Language . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.2.2 States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2.3 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.2.4 Locations and Updates . . . . . . . . . . . . . . . . . . . . . . 18
vii
2.2.5 Transition Rules . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.3 Abstract State Machine Language (AsmL) . . . . . . . . . . . . . . . 21
2.4 Property Speci¯cation Language (PSL) . . . . . . . . . . . . . . . . . 22
2.5 SystemC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3 PCI-X Bus Modeling 27
3.1 PCI-X Bus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.2 UML Modeling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.3 AsmL Modeling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.4 Translation to SystemC . . . . . . . . . . . . . . . . . . . . . . . . . 39
4 Model Checking 42
4.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.2 Model Checking Approach . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3 Model Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.4 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5 Generating FSM from SystemC 51
5.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
5.2 SystemC Syntactical Domain . . . . . . . . . . . . . . . . . . . . . . 52
5.3 Collecting Inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5.4 FSM Generation Algorithm . . . . . . . . . . . . . . . . . . . . . . . 56
5.4.1 Helper Functions . . . . . . . . . . . . . . . . . . . . . . . . . 58
viii
5.4.2 Direct FSM Generation . . . . . . . . . . . . . . . . . . . . . . 59
5.4.3 Grouping FSM Generation . . . . . . . . . . . . . . . . . . . . 61
5.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
6 Model-Based Testing 66
6.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
6.2 Direct Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.3 Grouping Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.4 Test Generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.4.1 Chinese Postman Tour (CPT) . . . . . . . . . . . . . . . . . . 78
6.4.2 RandomWalk . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.4.3 Test Sequences . . . . . . . . . . . . . . . . . . . . . . . . . . 80
6.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
7 Conclusion 85
7.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
7.2 Discussion and Future Work . . . . . . . . . . . . . . . . . . . . . . . 86 |
|