成功大學博碩士論文系統

簡易檢索 / 詳目顯示

回結果列表

研究生：	林振凱 Lin, Chen-Kai
論文名稱：	採用模型檢查驗證即時作業系統的排程行為：以Piko/RT為例 Implementation of Spin-based checking for preemptive RTOS scheduling behavior: the case study of Piko/RT
指導教授：	鄭憲宗 Cheng, Sheng-Tzong
學位類別：	碩士 Master
系所名稱：	電機資訊學院 - 資訊工程學系 Department of Computer Science and Information Engineering
論文出版年：	2018
畢業學年度：	106
語文別：	英文
論文頁數：	52
中文關鍵詞：	模型檢查、形式化驗證、先佔式排班
外文關鍵詞：	model checking, formal verification, preemptive scheduling
相關次數：	點閱：97 下載：10
分享至:	分享至facebook 分享至twitter

查詢本校圖書館目錄查詢臺灣博碩士論文知識加值系統勘誤回報

形式化驗證是用來針對目標系統所做的保證，保證在其軟體或硬體的規範下，系統不會出現非預期的行為。隨著資通訊產品日趨複雜及多元，這類非預期行為會隨著嚴重性的不同而造成不同程度的損失。形式化驗證就是其中一種方法，用來保證某些行為一定不會發生，或一定會發生。
Piko/RT 是一個針對物聯網開發的小型即時作業系統核心，而隨著不斷增加的物聯網規模與複雜度，如何保持安全與穩定將會是物聯網的一大問題。在這篇研究裡，我們使用形式化驗證的方法，更精確地說是模型檢查方法，來驗證一個全新作業系統的排程行為，並在不影響開發過程的前提下，透過形式化驗證的手法更深入去檢查單元測試或是Code review 無法檢查到的狀態，增加找出作業系統非預期行為的機會。
我們從硬體及軟體層面設計了一套抽象化的排程模型，包含了ARMv7-M 架構下的中斷行為、先佔式排班等，並驗證了在特定條件下互斥鎖及條件變數不會有競爭共享資源及死結的情形發生。

Formal verification is used to guarantee that under the hardware and software specification the target system must not behave unexpectedly. With the various applications of the ICT product, those unexpected behaviors might cause different degrees of losses. Formal verification is one way to claim that good properties will happen eventually and bad properties will never happen in the target system.

Piko/RT is a tiny real-time operating system kernel ptimized for the Internet of Things. With the massive growth of IOT network, “safety” and “stable” are the most significant issue. In this study, we apply model checking method on a new RTOS kernel to verify its scheduling behavior without affecting the development of the kernel. With this method, we can increase the chance to find unexpected behaviors which are less obvious by unit tests and code review.

We design an abstract scheduling model from the hardware and software aspects, including the preemptive scheduling and exception behavior of the ARMv7-M Architecture. And claims that mutex and condition variable have no mutual exclusion and deadlock under the specific situation.

摘要 i
Abstract ii
Acknowledgment iii
Table of Contents iv
List of Figures vi
List of Tables vi
Chapter 1 Introduction 1
Chapter 2 Background and Related Work 2
    2.1 Model checking 2
        2.1.1 Spin model checker 3
        2.1.2 Linear temporal logic 5
    2.2 Real-time scheduling 8
        2.2.1 Exception of ARMv7-M architecture 8
        2.2.2 Preemptive scheduling 11
    2.3 Related work 14
Chapter 3 Motivation 15
Chapter 4 Promela Model 17
    4.1 Overview of the Promela model 17
        4.1.1 Description of Variables 18
        4.1.2 AWAITS command 20
        4.1.3 Helper function 20
        4.1.4 PendSV request bit 22
        4.1.5 Push and pop AT commands 22
        4.1.6 ITake and PendSVTake commands 23
        4.1.7 IRet command 25
        4.1.8 Mechanism of softirq 26
        4.1.9 Thread information 27
    4.2 Interrupt handler model 28
    4.3 Scheduler model 29
        4.3.1 Bitmap scheduling model 29
        4.3.2 Proctype of SVC exception 34
        4.3.3 Proctype of PendSV exception 39
    4.4 User task model 39
        4.4.1 General user task 39
        4.4.2 Softirq 40
    4.5 Summary of Promela model 41
Chapter 5 Discussion 41
    5.1 Spin options 42
        5.1.1 Spin runtime options 42
        5.1.2 Verification options 42
        5.1.3 Runtime options 43
        5.1.4 Analyzing unreached statements 43
    5.2 Verifying simple applications 43
        5.2.1 Mutual exclusion with two interrupts 43
        5.2.2 Condition variable with one interrupts 46
        5.2.3 Condition variable with two interrupts 47
    5.3 Discussion 47
Chapter 6 Conclusions and Future Work 48
    6.1 Conclusion 48
    6.2 Future work 49
Reference 49
Appendix: Listing of Promela macros 51
                                    

[1] B. Alpern and F. B. Schneider, “Recognizing safety and liveness,” Distributed Computing, vol. 2, no. 3, pp. 117–126, 1987.
[2] J. Andronick, C. Lewis, D. Matichuk, C. Morgan, and C. Rizkallah, “Proof of OS scheduling behavior in the presence of interrupt-induced concurrency,” in International Conference on Interactive Theorem Proving, Nancy, France, 2016, pp. 52–68.
[3] ARM Limited, ARMv7-M Architecture Reference Manual, 2014.
[4] C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, London, 2008.
[5] M. Ben-Ari, Principles of the Spin Model Checker. Springer-Verlang London, 2008.
[6] B. Blackham, Y. Shi, S. Chattopadhyay, A. Roychoudhury, and G. Heiser, “Timing analysis of a protected operating system kernel,” in 2011 IEEE 32nd Real-Time Systems Symposium, 2011, pp. 339–348.
[7] E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. The MIT Press, 1999.
[8] P. Fonseca, K. Zhang, X. Wang, and A. Krishnamurthy, “An empirical study on the correctness of formally verified distributed systems,” in Proceedings of the Twelfth European Conference on Computer Systems, 2017, pp. 328–343.
[9] G. J. Holzmann. (2017) Spin. [Online]. Available: https://spinroot.com
[10] G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.
[11] J. Huang, Y.-K. Wu, and L. Lu. (2018) Piko/RT. [Online]. Available: https://github.com/PikoRT/pikoRT
[12] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “sel4: Formal verification of an os kernel,” in Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, 2009, pp. 207–220.
[13] L. Lamport, “Proving the correctness of multiprocess programs,” Software Engineering, IEEE Transactions on, vol. SE-3, pp. 125–143, 1977.
[14] X. Leroy, “Formal verification of a realistic compiler,” Commun. ACM, vol. 52, no. 7, pp. 107–115, 2009.
[15] C.-K. Lin. (2018) pikoRT-Spin. [Online]. Available: https://github.com/kaizsv/pikoRT-Spin
[16] R. Love, Linux Kernel Development, 3rd ed. Addison-Wesley Professional, 2010.
[17] NASA Engineering and Safety Center, “National highway traffic safety administration toyota unintended acceleration investigation,” NASA Engineering and Safety Center, Tech. Rep. TI-10-00618, 2011.
[18] S. Owicki and D. Gries, “An axiomatic proof technique for parallel programs i,” Acta Informatica, vol. 6, no. 4, pp. 319–340, 1976.
[19] A. Reid, R. Chen, A. Deligiannis, D. Gilday, D. Hoyes, W. Keen, A. Pathirane, O. Shepherd, P. Vrabel, and A. Zaidi, “End-to-End Verification of ARM Processors with ISA-Formal,” in Proceedings of the 2016 International Conference on Computer Aided Verification (CAV’16), vol. 9780, no. 9780, 2016, pp. 42–58.
[20] J. Yiu, The Definitive Guide to ARM Cortex-M3 and Cortex-M4 Processors. Newnes; 3 edition (November 1, 2013), 2013.
[21] H. Zhang, T. Aoki, and Y. Chiba, “A spin-based approach for checking osek/vdx applications,” in Formal Techniques for Safety-Critical Systems: Third International Workshop, FTSCS 2014, Luxembourg, November 6-7, 2014. Revised Selected Papers, 2015, pp. 239–255.

校內：立即公開
校外：立即公開

簡易檢索 / 詳目顯示

相關論文