2012-02-082024-05-17https://scholars.lib.ntu.edu.tw/handle/123456789/671253摘要：正規方法於電腦化系統的安全功能認證有根本且策略的重要性，台灣如欲自主開發高安全性之電腦化系統甚至提升整體的電腦軟硬體技術水準，持續努力投入正規方法相關技術的研發與應用實有其必要與價值。在上一年度的研究計畫中，我們以「核能儀控系統電腦化發展之安全功能認證」為目標，整理了國內外以正規方法發展安全軟體之應用實績與發展工具，以及更基礎的正規方法應用於安全軟體驗證之理論與技術，進而探討了正規方法應用於國內自主核能儀控系統軟體模組驗證之可行性。我們以一簡化但與核能儀控系統功能相近之化學反應爐溫度控制器程式的驗證為例，檢視運用現有正規方法與工具的可行性。該控制器程式範例具備即時與多執行緒等挑戰驗證技術的基本要素，具相當之代表性。就我們所考慮的代表範例而言，現有的正規驗證方法與工具已能將包括基本程式分析、功能正確性驗證、以及執行時間與排程分析等驗證工作的大部分過程自動化，可顯著節省通過認證所需的人力與時間。本年度，我們將以「核能儀控系統軟體模組安全功能驗證」為中心議題，更深入探討正規驗證方法的應用，除了持續觀察整理相關正規驗證方法與工具的發展外，將針對兩方面的課題做進一步的研究：一、我們希望能深入掌握模型檢測與演繹式兩大類正規驗證工具互補的必要性，理出更有系統的整合運用方式；二、我們也希望在排程分析模型與即時多執行緒程式語意之關聯的確立尋求更嚴謹且精準的方法。基於時間與人力的考量，本研究將較著重在既有方法與工具之整合。<br> Abstract: Formal methods have started to play an essential and strategic role in the certification of safety functions of computerized systems. To enhance her capability in developing safety-critical systems and even to elevate the overall level of computer hardware and software technology, Taiwan should continue investing in the research and application of formal methods. In the previous project “On Certification of Safety Functions in Computerized Nuclear Instrumentation and Control Systems Development,” we reviewed the applications of formal methods and related development tools in safety-critical software as well as the underlying theory and technology. The main purpose was to assess the feasibility of applying formal methods in verifying Taiwan’s probable own computerized nuclear instrumentation and control systems. To that end, we considered the verification of a program for controlling the temperature of a chemical reactor which resembles the targeted application domain. The controller, with real-time and multithread language features that are challenging for formal verification techniques, served well as a representative case. We found that most tasks in the basic program analysis, functional correctness, and timing analysis may be carried out automatically by existing methods and tools, which would considerably save labor and time in the process of certification.For this year, we shall center around a follow-up issue of “Verifying the Safety Functions of Software Modules in Computerized Nuclear Instrumentation and Control Systems” and strive to gain a deeper understanding of the application of formal methods. Aside from watching the research literature on the development of relevant formal methods and tools, we will investigate two particular issues: one is the necessity for model checking and deductive verification tools to complement each other. We hope to obtain a more systematic way of integrating the two kinds of tools. The other issue concerns the link between the task model in scheduling and the semantic model of a real-time multithreaded program. We hope to find a more rigorous and precise way of establishing their correct correspondence. Considering the time and manpower we have for this project, we shall focus more on the integration of existing methods and tools.正規方法安全功能高安全系統軟體驗證Formal MethodsSafety FunctionsSafety-Critical SystemsSoftware Verification