Formal Verification of Concurrent Software Systems

瀏覽統計 Email 通知 RSS Feed

簡歷

基本資料

Project title

Code/計畫編號

NSC97-2221-E019-013-MY3

Translated Name/計畫中文名

並行性軟體系統的正規驗證

Project Coordinator/計畫主持人

Yee-Jsong Juan

Funding Organization/主管機關

National Science and Technology Council

Department/Unit

Department of Computer Science and Engineering

Website

https://www.grb.gov.tw/search/planDetail?id=1749664

Year

2009

Start date/計畫起

01-08-2019

Expected Completion/計畫迄

31-07-2020

Bugetid/研究經費

544千元

ResearchField/研究領域

資訊工程--硬體工程

隨着網際網路和高速運算能力的快速成長，大型和複雜的軟體系統增加異常迅速。很多的軟體被應用於控制安全性需求高的系統，如果這些系統有錯誤，人類的生命及財產將受其危害，因此這類軟體必須擁有高的保證性(high assurance)。另外多核心的處理器使得個人電腦邁向另一個嶄新的紀元，為了從現今硬體技術發展上獲益，我們將必須設計能夠在非常多核心上同時執行的並行性軟體。並行性軟體必須具有同時執行的多執行緒技術(SMT)寫於程式碼中。沒有多執行緒技術(SMT)，軟體只能執行於單一個核心上，軟體的性能將無法從多核心處理器上得到任何的提升。令人遺憾，支援多核心處理器的軟體發展遠遠落後硬體的發展。自從Intel 介紹第一個雙核心的桌面處理器，只有少數的軟體廠商有開發利用多核心技術提升性能的並行性軟體 [41]。其主要原因包括1)現下軟體工程師缺乏針對多核心處理器足夠的並行性軟體訓練 2)支援多核心處理器的並行性軟體具有很高的複雜性不管在軟體設計，編碼，測試，或除錯上。其結果是不可靠和效率差的應用軟體，延誤幾年以上軟體開發計劃，和費用遠高於預算。因此輔助軟體設計的技術和工具必須加以大改進。正規驗證法在近十年內被快速接受為一個能自動證明並行性軟體正確性的有效方法。儘管已有許多研究成果，可惜的是正規驗證法現在主要的瓶頸在於程序狀態的劇增，當軟體的大小以直線增加，正規驗證法的複雜度是以指數方式而增加，現今正規驗證法的技術並不能應用於實際的並行性軟體開發計劃。為了解決這個問題，此研究計劃將發展新的並行性軟體正規驗證法，我們將專注於新的基礎理論和技術以克服程序狀態劇增的瓶頸。根據我們前幾年的研究成果，我們預計此研究計劃將有深遠的貢獻於正規驗證法。我們新的技術將可驗證很多重要的並行性軟體特性，例如: liveness, livelock, persistence, safety, fairness。除了同時的執行程序外，我們的技術將可驗證非同時的執行程序，非同時的執行程序已被廣泛的使用在現代的大型軟體系統中。此研究計劃也將發展一個整合性的架構,來進一步的減低正規驗證法的複雜度。此研究計劃所發展出的軟體驗證工具對將大型並行性軟體系統的正規驗證有重要的貢獻。 With the rapid growth of networking and high-computing power, the use of larger and more complex concurrent software systems has increased dramatically. Many of the concurrent software systems support or supplant human control of safety-critical systems. Failure of safety-critical systems could result in loss of finance and human life. Therefore, software used for safety-critical systems should preserve high assurance properties. In addition, multi-core processors usher in a brand new era in personal computers. A traditional single-core processor can only process one thread at a time, spending a majority of time waiting for data from memory. In contrast, each core in a multi-core processor processes a software thread simultaneously to improve system efficiency. In order be able to gain from the hardware technology progress we will have to design parallel applications running on many CPU cores at the same time. The software must have simultaneous multi-threading technology (SMT) written into its code. Without SMT the software will only recognize one core and there is no performance gain from multi-core platform. Unfortunately, the supporting concurrent software developed for multi-core processors legs far behind the advance of hardware. Since Intel introduced the first dual-core desktop processor, only a handful of independent software vendors have written applications that exploit multi-core architectures [41]. The main reasons are 1) software engineers nowadays lack sufficient training in concurrent software 2) concurrent software for multi-core processors has tremendously high complexity in design, coding, testing, and debugging. The results are unreliable and poorly performing applications, delayed projects (often for years), and considerable cost overruns. In order to improve the usability and reliability of large-scale concurrent systems, the supporting techniques and development tools need to be greatly enhanced. Formal verification is rapidly becoming accepted as a promising and automated method to verify the correctness of software systems. Despite many works have been done in the area of formal verification, one of main bottleneck so far is the state explosion problem. When the size of a software system increases linearly, the analysis complexity of the system could grow exponentially. The capability and performance of current techniques still cannot efficiently verify typical large-scale software systems in practice. In order to make good use of formal verification for modern large-scale concurrent software systems, this research project will develop new fundamental theories and techniques for formal verification. We will focus on the development of new techniques to attack the state explosion problem. According to the results of our preliminary research, we expect that this research project will have significant contribution to the area of formal verification. Our new technique will be able to verify many important high-assurance properties such as liveness, livelock, persistence, safety, fairness etc. In addition to dealing with synchronous processes, our technique will also be able to efficiently verify asynchronous processes which are widely used in modern large-scale concurrent software systems. This research will provide an integrated framework to further reduce the high analysis complexity by including other technique into our system. Finally, we expect the developed toolset will greatly contribute the practical use of automated tools for the development of large-scale concurrent software systems.

Keyword(s)

正規驗證
並行性系統
程序狀態的劇增
同時的
非同時的
安全的
持續的
公平的
執行程序
formal verification
concurrent systems
real-time systems
state explosion
liveness
livelock
persistence
safety
fairness
synchronous processes
asynchronousprocesses

DSpace CRIS

Formal Verification of Concurrent Software Systems

基本資料

Description