臺灣博碩士論文加值系統

隨著科技快速的進步，我們的生活中常接觸到各種不同和生命安全息息相關的系統(safety-critical system)，例如交通運輸系統、某些電子系統，以及醫療系統等。在這類的系統，潛在的設計錯誤可能會導致生命或財產的嚴重損害。為了避免發生這樣的憾事，我們可以利用正規驗證(formal verification)，例如模型驗證(model checking)的方法 — 一個非常可靠的技術 — 來徹底地驗證一個講究安全性的系統，究竟是否〝真正〞安全。目前在正規驗證的技術中，仍然沒有一種自動化的方法，能輔助系統設計者正規地模型化出系統發生錯誤以及修復的狀態。我們的貢獻就在於提出一個擴充的安全圖模型，使得模型化系統錯誤和修復錯誤的工作變得容易，並且將安全圖的模型，以相同的語意，轉化成為廣泛的真時自動機 (extended timed automaton, ETA)，當成模型驗證器的輸入，達到正規驗證的目的。正規驗證是驗證系統是否符合所描述的特性，而驗證的結果，能提供一個具體資訊，並且比較使用傳統使用錯誤樹分析(fault-tree analysis, FTA)所得到的結果，這些具體的資訊更為詳細。我們所提出的自動化錯誤分析的技術，整合在SGM這個模型驗證的工具中，並且舉出數個實際應用的例子來說明我們提出的模型和方法應用在驗證一個對安全甚為講究的系統上，是相當合適並且能有效達到錯誤分析的目的。

With rapid development in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design faults might result in injury or even death to human beings. To avoid such mishaps, we need to verify safety-critical systems thoroughly and formal verification techniques such as model checking are a very promising approach. Currently, there is practically no automatic
technique in formal verification that can aid system designers in formally modeling system faults and repairs. This work contributes by proposing an extension to the Safecharts model so that faults and repairs are easily modeled and then the Safecharts are transformed into semantically equivalent Extended Timed Automata models that can be directly model checked. The model checking results, such as witnesses of property specifications representing hazards, provide more concrete and useful information than the results from traditional failure analysis methods such as FTA. The proposed automatic
failure analysis techniques are integrated into the SGM model checker, which can thus be used to verify safety-critical systems. Application examples show the feasibility and benefits of the proposed model-driven verification of safety-critical systems.

Contents
1 Introduction 7
2 RelatedWork 11
3 Work Flow of Automatic Failure Analysis 16
4 Automatic Failure Analysis by Extending Safecharts 19
4.1 Automatic Failure Analysis . . . . . . . . . . . . . . . . . . . .19
4.2 Safecharts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
4.3 Extending Safecharts . . . . . . . . . . . . . . . . . . . . . . . . . 23
4.4 Failure Modes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
4.5 Safety Repair Actions . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4.6 Representation of Failures and Repairs in Safecharts . . . . . . . . . . 28
5 Transformating from Safecharts to Extended Timed Automata 35
5.1 Modeling in Safecharts . . . . . . . . . . . . . . . . . . . . . . . 36
5.2 Transformation from Safecharts to ETA . . . . . . . . . . . . . . . . . 37
5.3 Semantics of the Transformation from Safecharts to ETA . . . . . . . . 45
6 Application Examples 49
6.1 Automatic Water Sprinkler System . . . . . . . . . . . . . . . . . . . . 49
6.2 Automatic Electric Lamp System . . . . . . . . . . . . . . . . . . . . . 54
6.3 Nuclear Reactor System . . . . . . . . . . . . . . . . . . . . . . . . . 55
7 Conclusions 68

[1] R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science,
126(2):183–235, 1994.
[2] P. Bieber, C. Castel, and C. Seguin. Combination of fault tree analysis and model
checking for safety assessment of complex system. In Proceedings of the 4th
European Dependable Computing Conference, volume 2485 of LNCS, pages 19–
31. Springer Verlag, October 2002.
[3] L. Bodsberg and P. Hokstad. A system approach to reliability and life-cycle-cost of
process safety systems. IEEE Transactions on Reliability, 44(2):179–186, 1995.
[4] M. Bozzano, A. Cavallo, M. Cifaldi, L. Valacca, and A. Villafiorita. Improving
safety assessment of complex systems: an industrial case study. In Proceedings
of the International Formal Methods Europe Symposium, volume 2805 of LNCS,
pages 208–222. Springer Verlag, September 2003.
[5] M. Bozzano and A. Villafiorita. Improving system reliability via model checking:
the FSAP/NuSMV-SA safety analysis platform. In Proceedings of the International
Conferece on Computer Safety, Reliability and Security, volume 2788 of
LNCS, pages 49–62. Springer Verlag, 2003.
[6] E.M. Clarke and E.A. Emerson. Design and sythesis of synchronization skeletons
using branching time temporal logic. In Proceedings of the Logics of Programs
Workshop, volume 131 of LNCS, pages 52–71. Springer Verlag, 1981.
[7] E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 1999.
[8] International Electrotechnical Commission. Functional safety and IEC 61508.
http://www.iec.ch/functionalsafety, 2002.
[9] H. Dammag and N. Nissanke. Safecharts for specifying and designing safety critical
systems. In Proceedings of the 18th IEEE Symposium on Reliable Distributed
Systems, pages 78–87. IEEE CS Press, October 1999.
[10] J. Deneux and O. Akerlund. A common framework for design and safety analyses
using formal methods. In Proceedings of the International Conference on
Probabilistic Safety Assurance and Management (PSAM) and European Safety
and Reliability Conference. Springer, 2004.
[11] P. Fenelon, J.A. McDermid, M. Nicholson, and D.J. Pumfrey. Towards integrated
safety analysis and design. Applied Computing Review, 2:21–32, 1994.
[12] The SGM Group. SGM-State Graph Manipulators Project.
http://embedded.cs.ccu.edu.tw/∼esl web/Project/Ch/SGM/, 2006.
[13] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking
for Real-Time Systems. In Proceedings of the IEEE International Conference on
Logics in Computer Science (LICS’92), pages 394–406, June 1992.
[14] P.-A. Hsiung, Y.-H. Lin, and Y.-R. Chen. Safecharts Model Checking for the Verification
of Safety-Critical Systems. IDEA Group, Inc., 2006. (to appear).
[15] P.-A. Hsiung and F. Wang. A state-graph manipulator tool for real-time system
specification and verification. In Proceedings of the 5th International Conference
on Real-Time Computing Systems and Applications (RTCSA), pages 181–
188, 1998.
[16] J. Jacky. Formal safety analysis of the control program for a radiation therapy
machine. In Proceedings of the 13th International Conference on the Use of Computers
in Radiation Therapy, pages 68–70. Springer, 2000.
[17] M.E. Johnson. Model checking safety properties of servo-loop control systems.
In Proceedings of the International Conference on Dependable Systems and Networks,
pages 45–50. IEEE CS Press, 2002.
[18] G. Gossler K. Altisen and J. Sifakis. Scheduler modeling based on the controller
synthesis paradigm. Real-Time Systems, 23:55–84, 2002.
[19] L. Lavazza, editor. A methodology for formalizing concepts underlying the DESS
notation. ITEA, 2001.
[20] N.G. Leveson. Safeware: System Safety and Computers. Addison Wesley, 1995.
[21] N.G. Leveson and J. L. Stolzy. Safety analysis using Petri nets. IEEE Transactions
on Software Engineering, SE-13(3):386–397, 1987.
[22] S.-W. Lin, P.-A. Hsiung, C.-H. Huang, and Y.-R. Chen. Model checking prioritized
timed automata. In Proceedings of the 3rd International Symposium on Automated
Technology for Verification and Analysis (ATVA), volume 3707 of LNCS, pages
370–384. Springer Verlag, October 2005.
[23] K. Marta, N. Gethin, and P. David. Prism: Probabilistic symbolic model checker.
In Proceedings of the 12th International Conference on Modelling Techniques and
Tools for Computer Performance Evaluation, volume 2324 of LNCS, pages 200–
206. Springer Verlag, April 2002.
[24] N. Nissanke and H. Dammag. Risk bands - a novel feature of Safecharts. In Proceedings
of the 11th International Symposium on Software Reliability Engineering
(ISSRE), pages 293–301. IEEE CS Press, October 2000.
[25] N. Nissanke and H. Dammag. Risk ordering of states in Safecharts. In Proceedings
of the 19th International Conference on Computer Safety, Reliability, and Security,
volume 1943 of LNCS, pages 395–405. Springer Verlag, October 2000.
[26] N. Nissanke and H. Dammag. Design for safety in safecharts with risk ordering of
states. Safety Science, 40(9):753–763, December 2002.
[27] J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in
CESAR. In Proceedings of the International Symposium on Programming, volume
137 of LNCS, pages 337–351. Springer Verlag, 1982.
[28] Frank te Beest, Ad Peeters, Marc Verra, Kees van Berkel, and Hans Kerkhoff. Automatic
scan insertion and test generation for asynchronous circuits. In Proceedings
of the International Test Conference (ITC), pages 804–813. IEEE CS Press,
2002.
[29] European Union. Enhanced safety assessment for complex systems (ESACS)
project, 2003. http://www.esacs.org.
[30] F. Wang and P.-A. Hsiung. Efficient and user-friendly verification. IEEE Transactions
on Computers, 51(1):61–83, January 2002.
[31] S.H. Yang, P.W. Chung, S. Kowalewski, and O. Stursberg. Automatic safety analysis
of computer controlled plants using model checking. In Proceedings of the
10th Symposium on Computer-Aided Process Engineering (ESCAPE 10), 2000.
[32] K. YoungMin and A. Gul. Linear inequality LTL (iLTL): A model checker for
discrete time Markov Chains. In Proceedings of the 6th International Conference
on Formal Engineering Methods, volume 3308 of LNCS, pages 194–207. Springer
Verlag, November 2004.