2013-02-082024-05-17https://scholars.lib.ntu.edu.tw/handle/123456789/671412摘要：應用正規方法於電腦化系統的開發與驗證，由於其根本且策略的重要性，已成為軟體工程基礎研究的主要方向之一。台灣如欲自主開發可靠的高安全系統，持續投入正規方法相關技術的研究實有其必要與價值。在過去兩個年度的相關研究計畫中，我們整理了正規方法應用於安全軟體驗證的理論與技術，進而探討了正規方法應用於國內自主核能儀控系統軟體模組驗證之可行性。我們針對模型檢測與演繹式兩大類正規驗證工具互補的必要性，以及排程分析模型與即時多執行緒程式語意之關聯的確立等兩方面的課題，做深入的研究。我們應用外顯時間的描述法，提出了一套排程相關精準語意模型建構與工作負載模型萃取的框架。這些研究著重於即時多執行緒程式的分析與驗證，絕大部分的努力在於獲致精準之時間分析以及從程式碼中萃取時間分析所需的工作負載模型。然而，這樣的分析與驗證必須依賴即時作業系統排程等行為之精確語意模型；就實務現況而言，相關資料取得之困難極容易影響正規方法導入與落實之成效。相對而言，無作業系統的應用軟體，如感應器監控程式，並沒有這樣的限制，較有利於正規方法之先期導入。 在本年度的計畫中，我們希望能專注於無作業系統的控制程式，提出針對這類程式較完整的正規分析與驗證的方法。雖然少了複雜作業系統行為的障礙，執行程式的處理器硬體仍須以適當語意模型表述其行為，特別是中斷與計時機制；但由於相關技術規格資料取得較容易，比為作業系統塑模要單純許多。時間分析的工作減輕後，我們可投入較多心力於程式碼邏輯正確性的驗證，希望達到可能最完整的程度。這些經驗對於未來再面對即時多執行緒程式時，應有很高的參考價值。 <br> Abstract: Applying formal methods in the development and verification of computerized systems, for its fundamental and strategic importance, has become one of the main directions in the basic research of software engineering. To enhance her capability in developing reliable safety-critical systems, Taiwan should continue investing in the research and application of formal methods. In the previous two years of research on this subject, 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. We investigated two particular issues: the necessity for model checking and deductive verification tools to complement each other, hoping to obtain a more systematic way of integrating the two kinds of tools, and the link between the task model in scheduling and the semantic model of a real-time multithreaded program, hoping to find a more rigorous and precise way of establishing their correct correspondence. We proposed a framework based on the explicit-time approach for the latter semantic modeling, enabling the extraction of an abstract workload model from a real-time multithreaded program. These researches focused on the analysis and verification of real-time multithreaded programs, with most efforts devoted to obtaining a more precise timing analysis and the extraction of a workload model from a program that is needed for the timing analysis. However, such analysis and verification rely on precise modeling of the behaviors, in particular thread scheduling, of the underlying real-time operating system kernel. In practice, the difficulty in obtaining relevant technical documentation would easily hamper the effectiveness of introduction and application of formal methods. On the other hand, software applications that do not rely on an operating system, e.g., control programs for sensors, would not have this limitation and are more amenable to a complete treatment with formal methods. In this project, we hope to focus on control programs that operate without an operating system kernel, in order to obtain a more complete method for the formal analysis and verification of such programs. Although the obstacle of modeling complicated operating system behaviors is temporarily removed, there is still a need to model the behaviors, in particular interrupt and timer mechanisms, of the hardware on which the control program runs. However, as the relevant technical documentation is relatively easier to obtain, this modeling task should be much easier than that for an operating system. With the task of timing analysis lightened, we can devote more efforts in verifying the logical correctness of a program, aiming to obtain a practically applicable set of techniques that is as complete as possible. This experience should be valuable as we again encounter real-time multithreaded programs in the future.控制程式正規方法中斷模型檢測Modex程式證明高安全系統排程分析SPIN時間分析工作負載模型Controller ProgramsFormal MethodsInterruptsModel CheckingModexProgram VerificationSafety-Critical SystemsSchedulability AnalysisSPINTiming AnalysisWorkload Models