王凡教授的個人資料 - Profile of Farn Wang

王凡 Farn Wang

國立臺灣大學電機工程學系 教授
Professor, Department of Electrical Engineering, National Taiwan University
★副編輯(Associate Editorship)：
　　◆International Journal of Formal Methods in System Design, Springer-Verlag.
　　　(SCI extended)
★客座編輯(Guest Editorships)：
　　◆IJFCS (International Jounral of Foundations on Computer Science)
　　　Verification and Analysis of Infinite-state Systems特刊,
　　　Vol. 14, Nr.4, August, 2003, World Scientific Publishing Co. (SCI extended)
　　◆IJFCS, ATVA 2003/2004 特刊, (SCI extended), to appear.
★指導委員(Steering Committee Memberships in International Conferences)：
　　◆ATVA (International Symposium on Automated Technology for Verification
　　　and Analysis）
★議程委員會主席(Program Committee Chairmanships in International Conferences)：
　　◆IFIP FORTE (International Conference on Formal Techniques for Networked
　　　and Distributed Systems) 2005
　　◆ATVA 2004
★議程委員會共同主席(Program Committee Cochairmanships in International Conferences)：
　　◆ATVA 2003
　　◆RTC (International Workshop on Real-Time Constraints) 1999
　　◆RTCSA (International Conference on Real-Time Computing System and Applications)
　　　1997
★國際會議特邀演講講員(Invited Speeches in International Conferences and Workshops):
　　◆AVIS (Automated Verification of Infinite Systems) 2003, Warsaw, Poland
　　◆1st IWTS (International Workshop on Specification and Verification
　　　of Timed Systems) 1999, Kyoto, Japan.
　　◆IEEE HASE (High-Assurance Software Engineering) 98.
★國際會議短期課程講員(Tutorials in International Conferences and Workshops):
　　◆ICFEM (International Conference on Formal Engineering Methods) 2005
　　◆FORTE 2004
　　◆ATVA 2003

主要研究領域:

驗證自動化、軟體測試

Major Research Areas:

Verification Automation, Software Testing

研究領域摘要:

王教授的研究領域，是在利用人類的經驗與智慧，透過演算法語自動工具，提高系統驗證的效率與成本。現在一般大型計畫的執行成本，有超過50％是花費在驗證方面。台灣高科技產業未來能否存活，不在於能夠將多少尖端的feature放入系統中，而在於能否設計出品質穩定達到顧客期待的尖端產品。而這方面正是台灣高科技產業最欠缺的能力。針對這方面的需求，王教授的研究領域有下列兩項：

1. 嵌入式軟體自動驗證技術：利用演算法，自動分析系統設計的數學模型，找出設計錯誤。這方面著名的應用，有違軟的SLAM計畫。王教授的實驗室在嵌入式系統模型檢驗的自動演算法與工具方面，目前效能已經擊敗瑞典、法國、與美國的類似工具。

2. 軟體測試技術：「測試」是目前用來保證軟體品質的最常見手段。面對商業軟體動輒上百萬行的規模，其挑戰在於如何運用系統化的分析，方法化的研究，去自動產生test plan，達到高涵蓋率，並進而降低系統測試的成本與時間。

王教授目前執行包過廣達電腦、資策會、國科會、教育部、Intel等單位之研究計畫，年度總金額約四百萬元。

Research Summary:

 Prof. Wang's is now interested at helping the industry to reduce the cost of verification (or debugging), which has sky-rocketed up to more than 50% of the total development budget.  His research mainly are focused on two techniques.  

1. Automating human verification experiences to develop verification tools with high abstractness and efficiency.   Such tools have been shown effective in MS SLAM project to reduce the bugs of Windows drivers and the quality control in Intel CPU designs. 

2. Automatic test plan generation for embedded software.  In most companies, testing is still the major technique used to control the quality of software systems.  Our focus is to use automated technology to analyze system spec. and generate quality test plans that can check out bugs systematically and methodically. 

He is now executing the following projects. 

  1. NAS Server Functional Testing and Verification, Quanta Computers Inc. (廣達電腦), 2005/10/1-2006/9/30, NT$1,570,000.00

  2. Research on the Automation and Visualization Technology of Testcases for Software Systems, III (資策會), 2006/1/1-2006/12/31, NT$900,000. 

  3. A New Theory for Program Execution Time Analysis, NSC (國科會), 2005/8/1-2008/7/31, 3*NT$773,000.00. 

  4. An Integrated Framework for the Formal Development of Complex Embedded Systems, NSC (國科會), 2005/8/1-2008/7/31, 3*NT$483,000.00.

  5. Formal Method Course Planning, Software Engineering Consortium, Ministry of Education(教育部), 2004/3/1-2006/12/31, 2*NT$450,000.00. 

  6. Intel Multi-Core Course Planning, Intel, 2006/4/1-2007/3/31, USD$20,000.  (with Prof. S.-Y. Kuo, C.-L. Lei, H.-C. Yen)

Photo of Farn Wang

代表性著作 Selected Publication

  1. Farn Wang, G.-D. Huang, F. Yu., “TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering,” IEEE Transactions on Software Engineering, IEEE Computer Society., Vol. 32, Nr. 7, 510-526, Jul. 2006
  2. F. Wang, “Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-Structures,” IEEE Transactions on Software Engineering, Vol. 31, Nr. 1, 38-51, Jan. 2005
  3. F. Wang, “Inductive Composition of Numbers with Maximum, Minimum, and Addition - A New Theory for Program Execution-Time Analysis,” International Journal of Foundations of Computer Science, World Scientific, Vol. 15, Nr. 6, Dec. 2004
  4. F. Wang, H.-C. Yen., “Reachability Solution Characterization of Parametric Real-Time Systems,” Theoretical Computer Science, Elsevier,, Vol. 328, Nr. 1-2, 187-201, Nov. 2004
  5. F. Wang., “Formal Verification of Timed Systems: A Survey and Perspective,” Proceedings of the IEEE., Vol. 92, Nr. 8, 1283-1307, Aug. 2004
  6. F. Wang., “Efficient Verification of Timed Automata with BDD-like Data-Structures,” journal of Software Tools for Technology Transfer (STTT), Springer-Verlag, Vol. 6, Nr. 1, Jul. 2004
  7. J. Yang, A.K. Mok, F. Wang, “Symbolic Model Checking for Event-Driven Real-Time Systems,” ACM Transactions on Programming Languages and Systems, Vol. 19, Nr. 2, 386-412, Mar. 1997
  8. F. Wang, “Parametric Timing Analysis of Real-Time Systems,” Information and Computation, Academic Press, Vol. 130, Nr. 2,, 131-150, Nov. 1996
  9. F. Wang, A.K. Mok, E.A. Emerson, “Real-Time Distributed System Specification and Verification in APTL,” ACM Transactions on Software Engineering and Methodology, Vol. 2, Nr. 4, 346-378, Oct. 1993