形式化方法研究學術會

❶ 形式化方法的發展過程

軟體形式化方法最早可追溯到20世紀50年代後期對於程序設計語言編譯技術的研究，即J.Backus提出BNF描述Algol60語言的語法，出現了各 種語法分析程序自動生成器以及語法制導的編譯方法，使得編譯系統的開發從「手工藝製作方式」發展成具有牢固理論基礎的系統方法。形式化方法的研究高潮始於 20世紀60年代後期，針對當時所謂「軟體危機」,人們提出種種解決方法,歸納起來有兩類：一是採用工程方法來組織、管理軟體的開發過程；二是深入探討程 序和程序開發過程的規律，建立嚴密的理論，以其用來指導軟體開發實踐。前者導致「軟體工程」的出現和發展，後者則推動了形式化方法的深入研究。經過30多 年的研究和應用，如今人們在形式化方法這一領域取得了大量、重要的成果，從早期最簡單的形式化方法——一階謂詞演算方法到現在的應用於不同領域、不同階段 的基於邏輯、狀態機、網路、進程代數、代數等眾多形式化方法。形式化方法的發展趨勢逐漸融入軟體開發過程的各個階段,從需求分析、功能描述(規約)、(體 系結構/演算法)設計、編程、測試直至維護。

❷ 孫吉貴的學術論文

[1]輸入調解法和單元調解法在Horn集上的完備性 ，《軟體學報》1993年2月，4（1）。歐陽丹彤，孫吉貴，劉敘華。
[2]Horn集上的有向調解法，《吉林大學自然科學學報》 1992年11月，（4）。歐陽丹彤，孫吉貴，劉敘華。
[3]Completeness of Input Symmetric Paramolation and Unit Symmetric Paramolation on Horn Set,《Chinese Journal of Advanced Software Research》 1994年5月，1（2）。歐陽丹彤，孫吉貴，劉敘華。
[4]廣義因果理論上基於模型診斷過程的形式化，《吉林大學自然科學學報》 2000年10月，（4）。歐陽丹彤，孫吉貴。
[5]基於模型診斷的形式化方法，《人工智慧進展（第六屆中國人工智慧聯合學術會議論文集）》 2001年2月1日。歐陽丹彤，孫吉貴，姜雲飛。
[6]對基於模型診斷過程的形式化，《模式識別與人工智慧》 2002年9月，15（3）。歐陽丹彤，孫吉貴。
[7]「離散數學學習指導與習題解答」，高等教育出版社，2003年8月。
[8]約束邏輯的一個新語義研究，廣西師范大學學報（自然科學版），Vol.21, No.1, 2003,1-5。第七屆中國人工智慧聯合學術會議論文集CJCAI2002，張永剛，孫吉貴。
[9]一種模型不完備條件下的診斷方法，廣西師范大學學報（自然科學版），Vol.21, No.1, 2003, 79-82。第七屆中國人工智慧聯合學術會議論文集， CJCAI2002，林海，孫吉貴。
[10]基於模型診斷的替換測試與問題分解的研究，廣西師范大學學報（自然科學版），第七屆中國人工智慧聯合學術會議論文特刊Vol.21, No.1, 2003, 23-26。李佔山，王濤，孫吉貴。
[11]受限的proflog語言及其表推演過程語義，廣西師范大學學報（自然科學版），第七屆中國人工智慧聯合學術會議論文特刊，Vol.21, No.1, 2003, 27-33。陳榮，孫吉貴，姜雲飛。
[12]一種多值規則量詞公式的tableau的方法，廣西師范大學學報（自然科學版），第七屆中國人工智慧聯合學術會議論文特刊，Vol.21, No.1, 2003,，101-105。劉全，孫吉貴。
[13]Theorem Proving Based on the Extension Rule, Journal of Automated Reasoning 31, 2003, pp11-21.LIN Hai, SUN Jigui, ZHANG Yimin.
[14]非二元約束滿足問題求解，計算機學報，Vol.26, No.12, 2003, pp1746-1752.孫吉貴，景沈艷。
[15]The Concept of Approximation Based on Fuzzy Dominance Relation in Decision-Making, Proceedings 9th International Conference, RSFDGrC2003, Chongqing, China, May 2003. In Guoyin Wang, Qing Liu, Yiyu Yao and Andrzej Skowron eds: Rough Sets, Fuzzy Sets, Data Mining, and Granular Computing, Lecture Notes in Artificial Intelligence 2639, Edited by J.G.Carbonell and J.Siekmann, Subseries of Lecture Notes in Computer Science. Springer, pp382-385.。Yunxiang Liu, Jigui Sun, Shengsheng Wang.
[16]量子搜索演算法，軟體學報，Vol.14, No.3, 2003, pp334-344.。孫吉貴，何雨果。
[17]提高一階多值邏輯Tableau推理效率的布爾剪枝方法，計算機學報，Vol.26, No.9, 2003, 1165-1170.。劉全，孫吉貴。
[18]一種含等詞的分階段Tableau演算法，計算機工程，Vol.29, No.8, 2003, pp44-46.。劉全，孫吉貴，張永剛。
[19]一種多值規則量詞公式的Tableau的方法，計算機工程，Vol.29, No.8, 2003, pp128-130.。劉全，孫吉貴，竇全勝。
[20]組合優化調度問題求解方法，計算機科學，Vol.30, No.2, 2003, pp9-16.張居陽，孫吉貴。
[21]基於約束的調度研究與實現，2003中國計算機大會論文集1，北京，2003年12月，清華大學出版社，pp80-85.。張居陽，禮欣，孫吉貴。
[22]適用於決策表的快速屬性約簡演算法，2003中國計算機大會論文集1，北京，2003年12月，清華大學出版社，pp41-46.。何雨果，孫吉貴。
[23]模糊集合的語義，中國人工智慧學會全國第10屆全國學術年會論文集（下），廣州，2003年12月，2003，pp1072-1077。劉雲翔，孫吉貴。
[24]基於t-norm運算元的模糊邏輯和模糊推理。吉林大學學報（理學版），Vol.41, No.1, 2003.pp64-69。劉雲翔，孫吉貴。
[25]模型生成與約束求解，知識科學與計算科學研討會，烏魯木齊，2002年9月，見陸汝鈐主編「知識科學與計算科學」，清華大學出版社，2003年1月，197-232。孫吉貴，張永剛。
[26]量子並行計算，知識科學與計算科學研討會，烏魯木齊，2002年9月，見陸汝鈐主編「知識科學與計算科學」，清華大學出版社，2003年1月，236-242。孫吉貴，何雨果。
[27]基於模型的診斷問題分解及其演算法，計算機學報，Vol.26, No.9, 2003, 1171-1176.李佔山，姜雲飛，王濤。
[28]基於模型診斷方法的系統替換修復與重新配置，吉林大學學報（理學版），Vol.41, No.1, 2003, pp45-48.李佔山，王濤，孫吉貴。
[29]商業智能技術及行業應用分析，吉林大學學報（信息科學版），第21卷 第1期 2003.2.李澤海，孫吉貴，趙君。
[30]離散數學教學改革中的幾點做法和體會，中國教育理論雜志，第42期， 2003.11。張永剛，孫吉貴。
[31]21世紀《離散數學》教材與教學模式的改革現代教學與管理，2003.第8期。李佔山 孫吉貴。

❸ 形式化方法的研究內容

形式化方法的一個重要研究內容是形式規約(Formal Specification,也稱形式規范或形式化描述),它是對程序「做什麼」(what to do)的數學描述,是用具有精確語義的形式語言書寫的程序功能描述,它是設計和編製程序的出發點,也是驗證程序是否正確的依據。對形式規約通常要討論其一 致性(自身無矛盾)和完備性(是否完全、無遺漏地刻畫所要描述的對象)等性質。形式規約的方法主要可分為兩類:一類是面向模型的方法也稱為系統建模,該方 法通過構造系統的計算模型來刻畫系統的不同行為特徵；另一類是面向性質的方法也稱為性質描述,該方法通過定義系統必須滿足的一些性質來描述一個系統。不同 的形式規約方法要求不同的形式規約語言,即用於書寫形式規約的語言(也稱形式化描述語言),如代數語言OBJ、Clear、ASL、ACT One/Two等;進程代數語言CSP、CCS、π演算等；時序邏輯語言PLTL、CTL、XYZ/E、UNITY、TLA等；這些規約語言由於基於不同 的數學理論及規約方法，因而也千差萬別，但它們有一個共同的特點,即每種規約語言均由基本成分和構造成分兩部分構成。前者用來描述基本(原子)規約,後者 把基本部分組合成大規約。構造成分是形式規約研究和設計的重點，也是衡量規約語言優劣的主要依據。
形式驗證形式化方法的另一重要研究內容是形式驗證(Formal Verification)。形式驗證與形式規約之間具有緊密的聯系，形式驗證就是驗證已有的程序(系統)P，是否滿足其規約(φ,ψ)的要求(即P (φ,ψ)),它也是形式化方法所要解決的核心問題。傳統的驗證方法包括模擬(simulation)和測試(testing)，它們都是通過實驗的方法 對系統進行查錯。模擬和測試分別在系統抽象模型和實際系統上進行,一般的方法是在系統的某點給予輸入，觀察在另一點的輸出,這些方法花費很大，而且由於實 驗所能涵蓋的系統行為有限，很難找出所有潛在的錯誤。基於此，早期的形式驗證主要研究如何使用數學方法，嚴格證明一個程序的正確性(即程序驗證)。

❹ 形式化方法的介紹

形式化方法英文的名稱是formal methods。在邏輯科學中是指分析、研究思維形式結構的方法。它把各種具有不同內容的思維形式(主要是命題和推理)加以比較,找出其中各個部分相互聯結的方式,如命題中包含概念彼此間的聯結,推理中則是各個命題之間的聯結,抽取出它們共同的形式結構;再引入表達形式結構的符號語言,用符號與符號之間的聯系表達命題或推理的形式結構。例如,把全稱肯定命題,用符號形式化為「SAP」;把聯言命題、假言命題分別形式化為:「p∧q、「p→q」。又例如:一個具體的假言聯言推理「如果這種金屬是純鋁,那麼它的物理性質必與純鋁相同;如果這種金屬是純鋁,那麼它的化學性質必與純鋁相同;但這種金屬的物理性質和化學性質與純鋁不相同;所以,它不是純鋁。」這個推理的形式結構是:「如果p,則q;如果p,則r;非q且非r;所以非p。」可進而形式化為下列公式:((p→q)∧(p→r)∧┐q∧┐r→┐p。

❺ 形式化方法的分類

根據說明目標軟體系統的方式，形式化方法可以分為兩類：
1）面向模型的形式化方法。面向模型的方法通過構造一個數學模型來說明系統的行為。
2）面向屬性的形式化方法。面向屬性的方法通過描述目標軟體系統的各種屬性來間接定義系統行為。
根據表達能力，形式化方法可以分為五類：
1）基於模型的方法：通過明確定義狀態和操作來建立一個系統模型（使系統從一個狀態轉換到另一個狀態）。用這種方法雖可以表示非功能性需求（諸如時間需求），但不能很好地表示並發性。如：Z語言，VDM，B方法等。
2）基於邏輯的方法：用邏輯描述系統預期的性能，包括底層規約、時序和可能性行為。採用與所選邏輯相關的公理系統證明系統具有預期的性能。用具體的編程構 造擴充邏輯從而得到一種廣譜形式化方法，通過保持正確性的細化步驟集來開發系統。如：ITL（區間時序邏輯），區段演算（DC），hoare 邏輯，WP演算，模態邏輯，時序邏輯，TAM（時序代理模型），RTTL（實時時序邏輯）等。
3）代數方法：通過將未定義狀態下不同的操作行為相聯系，給出操作的顯式定義。與基於模型的方法相同的是，沒有給出並發的顯式表示。如：OBJ， Larch族代數規約語言等；
4）過程代數方法：通過限制所有容許的可觀察的過程間通信來表示系統行為。此類方法允許並發過程的顯式表示。如：通信順序過程（CSP），通信系統演算 （CCS），通信過程代數（ACP），時序排序規約語言（LOTOS），計時CSP(TCSP），通信系統計時可能性演算（TPCCS）等。
5）基於網路的方法：由於圖形化表示法易於理解，而且非專業人員能夠使用，因此是一種通用的系統確定表示法。該方法採用具有形式語義的圖形語言，為系統開發和再工程帶來特殊的好處。如 Petri圖，計時Petri圖，狀態圖等。

❻ 形式化方法

你用畫的方法是一個過程的解決方式，這個方式是很流行的

❼ 什麼是形式化什麼是形式模型

形式化方法一般是用一種嚴格的，精準的方法（一般是數學語言）描述軟體，對軟體建模。
你可以理解為類似UML建模。只是形式化的方法更難學，你可以理解為離散數學里的各種規約、公式。形式化模型就是你用形式化方法構建出來的模型，可類比UML模型，也可以類比數學建模，甚至可以類比編程代碼（編程同樣是用編程語言對軟體需求的精確描述）

❽ 對軟體形式化方法課程學習的認識

把概念、判斷、推理轉化成特製的形式符號後，對形式符號表達系統進行研究的方法。它可以消除自然語言的歧義性、不通用性，為不同學科提供具有普遍適用性的共同邏輯形式，有利於揭示新聯系，導致新發現。