(18.204.227.34) 您好!臺灣時間:2021/05/14 08:09
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:林靖婕
研究生(外文):Jing-Jie Lin
論文名稱:安全攸關軟體驗證方法與工具之研究
論文名稱(外文):A Study of Methods and Tools for Verifying Safety-Critical Software
指導教授:蔡益坤
口試委員:王柏堯陳郁方
口試日期:2012-07-24
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:資訊管理學研究所
學門:電算機學門
學類:電算機一般學類
論文種類:學術論文
論文出版年:2013
畢業學年度:101
語文別:中文
論文頁數:62
中文關鍵詞:正規方法模型檢查多執行緒程式即時系統靜態分析時間量測分析最差情況執行時間
外文關鍵詞:Formal MethodsModel CheckingMultithreadingReal-Time SystemsStatic AnalysisTiming AnalysisWCET
相關次數:
  • 被引用被引用:0
  • 點閱點閱:273
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
安全攸關軟體的錯誤將導致人類傷亡,因此其正確性極為重要。安全攸關軟體典型為即時的多執行緒程式。多執行緒以執行多個並行活動,即時程式設計以確保滿足嚴格的時間限制。即時的多執行續程式設計易於犯錯,部分錯誤詭祕而難以用測試或模擬來發現。因此此類安全攸關軟體需要使用正規驗證方法加以檢查。
現今有許多方法及工具來支援即時多執行緒程式在功能及時間正確性上的正規驗證,每種方法或工具提供程式所涵蓋問題的部分解決方案。然而這些方法及工具由不同機構進行開發,因此選擇適合的工具或方法組合變得不易。為了實際驗證一程式,需要花費許多時間努力熟悉在不同領域的工具,並選擇適當的工具組合來完成驗證。在此論文中,我們對此類方法及工具做一精選,並介紹如何實行驗證。為使說明更易理解,我們以一具代表性的控制器程式為範例,此程式用以控制化學反應爐之溫度。論文中詳細說明功能正確性及時間正確性的驗證細節,並指出用以驗證的模型和實際程式間是否存在差異,以及是否存在現今工具無法支援的任務。我們以此論文建立一基準案例,透過此案例可迅速而容易地對現今即時多執行緒程式的正規驗證科技有一定的了解與評估。

Safety-critical software is software whose failure harm people or even cause deaths, so the correctness of such software is very important. Safety-critical software is typically a real-time and multithreaded program. Multithreading is required because of multiple concurrent activities. Real-time programming is required to guarantee strict timing constraints. Real-time multithreaded programs are prone to mistakes, and some bugs in such programs are subtle and difficult to find using testing or simulation. Thus it is desirable to apply formal verification on such safety-critical programs.
Nowadays, there are many methods and tools that support formal verification of the functional and timing correctness of real-time multithreaded programs. Each method or tool provides parts of solutions to the issue involved. Unfortunately, the methods and tools have traditionally been developed separately by different communities, and it is nontrivial to assemble a suitable collection of them. To practically verify a program, one needs to spend much effort and time on getting familiar with the tools located in different domains, and to select an adequate tool collection to complete the verification tasks. In this thesis, we review a selection of methods and tools and show how they may be used to carry out the verification tasks. To provide a more comprehensive illustration, we consider a representative controller program as our target program, which is a temperature controller for chemical reactor protection. We delineate the details for verification of the functional correctness and timing correctness of the program. We also point out whether there exist differences between the model for verification and the real program, and whether there exist tasks that are not supported by current tools. In doing so, we establish a benchmark case and with it obtain a partial yet informative assessment of the readiness of current technology for formal verification of real-time multithreaded programs.

誌謝 i
中文摘要 ii
THESIS ABSTRACT iii
1 Introduction 1
1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Motivation and Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2 Preliminaries and Related Work 4
2.1 Controllers and Real-Time Programming . . . . . . . . . . . . . . . . . . 4
2.2 Model Checking and Deductive Verification . . . . . . . . . . . . . . . . . 5
2.2.1 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.2.2 Deductive Verification . . . . . . . . . . . . . . . . . . . . . . . . 8
2.3 WCET and Scheduling Analysis . . . . . . . . . . . . . . . . . . . . . . . 10
2.3.1 WCET . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.3.2 Scheduling Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.4.1 Cases of Tools Application for Functional Correctness . . . . . . . 20
2.4.2 Cases of Tools Application for Timing Correctness . . . . . . . . . 21
2.4.3 Cases of Tools Application for Both Functional and Timing Correctness
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3 Challenge Case: The Controller 22
3.1 Introduction of the Controller . . . . . . . . . . . . . . . . . . . . . . . . 22
3.2 Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3.3 Code of the Controller . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
4 Functional Correctness 33
4.1 Model Checking - Using SPIN . . . . . . . . . . . . . . . . . . . . . . . . 33
4.1.1 De_ne Modex test harness _le . . . . . . . . . . . . . . . . . . . . 33
4.1.2 Run Modex to Extract Model . . . . . . . . . . . . . . . . . . . . 39
4.1.3 Run SPIN to Verify the Model . . . . . . . . . . . . . . . . . . . . 39
4.2 Deductive Approach - Using VeriFast . . . . . . . . . . . . . . . . . . . . 41
4.2.1 Rewrite Program . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.2.2 Model External Functions . . . . . . . . . . . . . . . . . . . . . . 41
4.2.3 Annotate Program . . . . . . . . . . . . . . . . . . . . . . . . . . 43
5 Timing Correctness 47
5.1 Compute WCET . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
5.1.1 Divide and Compile the Program . . . . . . . . . . . . . . . . . . 47
5.1.2 Annotate Program . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5.2 Compute WCRT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.2.1 Set up System Model . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.2.2 Query for WCET and Run . . . . . . . . . . . . . . . . . . . . . . 51
5.3 Compute Overhead . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
5.3.1 Query Task Switch Cost . . . . . . . . . . . . . . . . . . . . . . . 52
5.3.2 Run Scheduling Analysis . . . . . . . . . . . . . . . . . . . . . . . 53
6 Conclusion 54
6.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
6.2 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
6.2.1 SPIN+Modex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
6.2.2 VeriFast . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
6.3 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
Bibliography 58

[1] aiT. http://www.absint.com/ait/.
[2] Bound-T. http://www.bound-t.com/.
[3] DO-178B/ED-12B. Software Considerations in Airborne Sstems and Equipment Certification
[4] Frama-C software analyzers. http://frama-c.com/.
[5] The GNU C library manual.
[6] IEC 61508. http://www.iec.ch/functionalsafety/.
[7] IEEE Std 1003.1-2008 Portable Operating System Interface (POSIX) Base Specifications, Issue 7.
[8] IEEE Std 1003.1-2008 Portable Operating System Interface (POSIX) Commands and Utilities, Issue 7.
[9] IEEE Std 1003.1-2008 Portable Operating System Interface (POSIX) System Interfaces and Headers, Issue 7.
[10] INTERESTED project.
[11] Modex. http://spinroot.com/modex/index.html.
[12] RT-Druid. http://www.evidence.eu.com/content/view/28/51/.
[13] SWEET. http://www.mrtc.mdh.se/projects/wcet/sweet.html.
[14] SymTA/S. http://www.symtavision.com/symtas.html.
[15] MISRA-C: 2004 | guidelines for the use of the C language in critical systems, 2004.
[16] T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with SLAM. Communications of the ACM, 54(7):68-76, 2011.
[17] D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In CAV 2011, volume 6806 of LNCS, pages 84-190, 2011.
[18] S. Byhlin, Ermedahl A., Gustafsson J., and Lisper B. Applying static wcet analysis to automotive communication software. In ECRTS 2005, pages 249-258, 2005.
[19] A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An opensource tool for symbolic model checking. In CAV 2002, volume 2404 of LNCS, pages 359-364, 2002.
[20] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proceedings of the 12th International Conference on Computer Aided Verification, volume 1855 of LNCS, pages 154-169, 2000.
[21] E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. The MIT Press, 1999.
[22] E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: a practical system for verifying concurrent c. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of LNCS, pages 23-42, 2009.
[23] L. Cordeiro and B. Fischer. Verifying multi-threaded software using SMT-based context-bounded model checking. In Proceedings of the 33rd International Conference on Software Engineering, pages 331{340, 2011.
[24] C. Cuypers, B. Jacobs, and F. Piessens. Verification of data-race-freedom of a java chat server with verifast. CW reports CW550, Department of Computer Science, K.U.Leuven, 2009.
[25] E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453{457, 1975.
[26] B. Dutertre and L. d. Moura. The YICES SMT solver.
[27] C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt, H. Theiling, S. Thesing, and R. Wilhelm. Reliable and precise wcet determination for a real-life processor. In Proceedings of the 1st International Workshop on Embedded Software, volume 2211 of LNCS, pages 469{485, 2001.
[28] J.-C. Filli^atre and C. Marche. The Why/Krakatoa/Caduceus platform for deductive program verification. In CAV 2007, volume 4590 of LNCS, pages 173{177, 2007.
[29] P. R. Gluck and G. J. Holzmann. Using spin model checking for ight software verification. In Proceedings of Aerospace Conference, 2002. IEEE, volume 1, pages 105{113, 2002.
[30] J. Gustafsson and A. Ermedahl. Experiences from applyingWCET analysis in industrial settings. In Proceedings of the 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing, ISORC ''07, pages 382{392. IEEE Computer Society, 2007.
[31] R. Heckmann and C. Ferdinand. Worst-case execution time prediction by static program analysis. Technical report, AbsInt Angewandte Informatik GmbH, 2004. http://www.absint.com/wcet.htm.
[32] R. Henia, A. Hamann, M. Jersak, R. Racu, K. Richter, and R. Ernst. System
level performance analysis { the SymTA/S approach. IEE Computers and Digital
Techniques, 152(2):148{166, 2005.
[33] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576{580, 1969.
[34] G. J. Holzmann. An improved protocol reachability analysis technique. SOFTWARE, PRACTICE AND EXPERIENCE, 18:137{161, 1988.
[35] G. J. Holzmann. An analysis of bitstate hashing. Formal Methods in System Design, 13(3):289{307, 1998.
[36] G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. 2003.
[37] Md. I. Hossain and N. S. Chowdhury. A practical approach on model checking with modex and spin. In International Journal of Electrical and Computer Sciences, volume 11, pages 1{7, 2011.
[38] B. Jacobs, J. Smans, and F. Piessens. A quick tour of the VeriFast program verifier.
In APLAS 2010, volume 6461 of LNCS, pages 304{311, 2010.
[39] M. Jersak. Compositional performance analysis for complex embedded applications.
Technical report, PhD thesis, Technical University of Braunschweig, 2004.
[40] D. Kastner, R. Wilhelm, R. Heckmann, M. Schlickling, M. Pister, M. Jersak,
K. Richter, and C. Ferdinand. Timing validation of automotive software. In ISoLA, pages 93{107, 2008.
[41] M. Kim, S. Hong, C. Hong, and T. Kim. Model-based kernel testing for concurrency bugs through counter example replay. Electronic Notes in Theoretical Computer Science, 253(2):21{36, 2009.
[42] J. Kosina. Fighting security bugs in the linux kernel. In WDS''07 Proceedings of Contributed Papers, pages 64{71, 2007.
[43] S. Kunzli, A. Hamann, R. Ernst, and L. Thiele. Combined approach to system level performance analysis of embedded systems. In Proceedings of the 5th IEEE/ACM International Conference on Hardware/Software Codesign and System Synthesis, pages 63{68, 2007.
[44] C.-G. Lee, J. Hahn, Y.-M. Seo, S. L. Min, R. Ha, S. Hong, C. Y. Park, M. Lee, and C. S. Kim. Analysis of cache-related preemption delay in fixed-priority preemptive scheduling. IEEE Transactions on Computers, 47:700{713, 1998.
[45] J. Lehoczky, L. Sha, and Y. Ding. The rate monotonic scheduling algorithm exact characterization and average case behavior. In Proceedings of Real Time Systems Symposium 1989, pages 166{171, Santa Monica, CA, USA, 1989.
[46] J. W. S. Liu. Real-Time Systems. Prentice Hall, 2002.
[47] L. d. Moura and N. Bjorner. Z3: An effcient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 337{340, 2008.
[48] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: a proof assistant for
higher-order logic. 2002.
[49] J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS 2002, pages 55{74. IEEE Computer Society Press, 2002.
[50] J. Souyris, V. Wiels, D. Delmas, and H. Delseny. Formal verification of avionics software products. In Proceedings of the 2nd World Congress on Formal Methods, volume 5850 of LNCS, pages 532{546, 2009.
[51] The Coq Development Team. The Coq Proof Assistant Reference Manual { Version 8.3, October 2010.
[52] W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engineering, 10(2):203{232, 2003.
[53] R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenstrom. The worst-case execution-time problem - overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems, 7(3):36{1, 2008.
[54] J. Yoo, E. Jee, and S. Cha. Formal modeling and verification of safety-critical
software. Software, IEEE, 26(3):42{49, 2009.
[55] A. Zaks and R. Joshi. Verifying multi-threaded C programs with SPIN. In Proceedings of the 15th International SPIN Workshop on Model Checking Software, volume 5156 of LNCS, pages 325{342, 2008.

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
系統版面圖檔 系統版面圖檔