《計算機(jī)科學(xué)與技術(shù)方法論》

專題講座

追嶺煎掐襲躇濘昆制碼懼累懇篡憂櫥遮廟豎艘榴完鋼這軸憊欠使秧離鰓茨計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論軟件開發(fā)中的形式化方法1形式化技術(shù)的產(chǎn)生和發(fā)展2軟件開發(fā)中為什么使用形式化方法3形式化規(guī)格技術(shù)4形式化驗證技術(shù)5小結(jié)卑昨咆竣跳狙擺理僑沙匡姐值竹鵬暈土亭洽賭肌胚耶憾控賦薦壯鴉志梢妙計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論1形式化技術(shù)的產(chǎn)生和發(fā)展自20世紀(jì)60年代末以來，許多學(xué)者開展了形式化技術(shù)的相關(guān)研究。形式化技術(shù)最早是從戴克斯特拉和霍爾（C.Hoare）在程序驗證方面的工作和斯科特（D.S.Scott）以及其他學(xué)者在程序語義方面的工作發(fā)展起來的。現(xiàn)在，形式化技術(shù)已經(jīng)成為計算機(jī)科學(xué)的一個重要分支和研究領(lǐng)域，其作用相當(dāng)于傳統(tǒng)工程設(shè)計（如計算流體動力學(xué)，CFD）在航空設(shè)計中的作用。陋姆贓漱蒸害勞亞凡僻賠從濾歌雪賤拖熏底擱履妹相池硝父培借坐咸邁雕計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論1形式化技術(shù)的產(chǎn)生和發(fā)展近些年來，形式化技術(shù)的學(xué)術(shù)研究及其工業(yè)應(yīng)用得到了長足的發(fā)展。研究人員建立了系統(tǒng)設(shè)計人員易于理解的規(guī)格概念和術(shù)語，以及有效應(yīng)用這些術(shù)語和概念的形式化規(guī)格技術(shù)及語言，建立了功能更加強大和完善的模型驗證和定理證明技術(shù)，并開發(fā)出了與之相應(yīng)的從研究原型到商品化產(chǎn)品的支撐工具和環(huán)境。憎倚沖晌橡靜蹲媒捂希肚滬奉勃苑壩涌淌臉瀉黨鄭虧啦犬英繩聰身脊室普計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論1形式化技術(shù)的產(chǎn)生和發(fā)展盡管當(dāng)前對大型復(fù)雜的系統(tǒng)進(jìn)行完整的形式化驗證還不現(xiàn)實，但把形式化技術(shù)應(yīng)用于大型復(fù)雜系統(tǒng)的關(guān)鍵部分確實是一個有效的實用策略。目前，有效的模型檢驗和定理證明技術(shù)已成為硬件驗證中傳統(tǒng)仿真技術(shù)的補充，而軟件開發(fā)工程師們開始使用更為嚴(yán)格的形式化規(guī)格及驗證技術(shù)，成功地完成了過程控制領(lǐng)域工業(yè)規(guī)模系統(tǒng)的設(shè)計，通信系統(tǒng)中大量的安全可靠通信協(xié)議得到了測試和檢驗。秧火窯抑招欲賂屎荔瞄浸怎傅熊佑融汕紛燒賈嚎超串迸頂央彪革耘蛇狗似計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論1形式化技術(shù)的產(chǎn)生和發(fā)展形式化技術(shù)成功的工業(yè)應(yīng)用引起了人們的普遍關(guān)注，可以預(yù)計，在未來的工業(yè)應(yīng)用系統(tǒng)開發(fā)中，形式化技術(shù)將會發(fā)揮越來越重要的作用。院漸波神器蘑躁熄非蔑遂秋仿朔轍餞舌割玄建俐公徊袁竊廟務(wù)酞訟毅殼睜計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論軟件開發(fā)中的形式化方法1形式化技術(shù)的產(chǎn)生和發(fā)展2軟件開發(fā)中為什么使用形式化方法3形式化規(guī)格技術(shù)4形式化驗證技術(shù)5總結(jié)絢負(fù)皋犧取體從崗猴踏壹什抨覆劃嫌風(fēng)稈捅紉襄決蚜興眨吵四吩勁腿磷掏計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論2軟件開發(fā)中為什么使用形式化方法（1）保證質(zhì)量的需要（2）節(jié)約成本的需要（3）形式方法和復(fù)用（4）英國國防部的標(biāo)準(zhǔn)（5）經(jīng)典案例翹糠泣翰稱菱鋪啤琳贍兌魂撰到帝恕簿蓬朽欺患吐痢哦震伙臥挺焚菏邀碧計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）保證質(zhì)量的需要為了得到高質(zhì)量的軟件，我們強烈地希望使用軟件工程中最好的實踐。軟件中存在的缺陷至少會引起客戶的憤怒，而在更壞的情況下可能會給客戶的業(yè)務(wù)造成較大的破壞或者造成生命損失。因此，企業(yè)要采用最好的實踐，使他們的軟件過程變得成熟起來。形式方法是一種前沿技術(shù)，研究表明，這種技術(shù)非常有助于那些希望把軟件產(chǎn)品的缺陷出現(xiàn)率減到最小的公司。憑減殊黑祖犬告侮聚柞纓困鼎彈湘頰觀咸靜炸韶鴻渤鷗哈籌源中苑嗚篇懈計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）節(jié)約成本的需要有證據(jù)顯示，形式方法的使用減少了項目成本。例如，IBM的大型CICS事務(wù)處理項目的獨立審核表明，9％的成本節(jié)約要歸功于形式方法的使用。對T800型變換計算機(jī)的Inmos浮點單元的獨立審核也證明，形式方法的使用估計可以減少12個月的測試時間。菌鴛磁奉撣策銜旗裔冉搓佛忍呻像懂屑李訪予主榮窘挑伴綏溢醋唯賃吻盎計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）形式方法和復(fù)用有效的軟件復(fù)用有助于提高軟件開發(fā)的生產(chǎn)率，這在應(yīng)用軟件的快速開發(fā)中具有特殊的意義。軟件復(fù)用的思想是開發(fā)出可在未來項目中使用的基本部件，這就要求部件具有高質(zhì)量和高可用性，而且部件的實際行為和使用環(huán)境也要具備一個文檔化的描述。倘篩斟風(fēng)埃打削軍酋炯金寡仆紗闊暇夠傘競壞梢焰餾漢辜淫如打帆頌楚錦計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）形式方法和復(fù)用形式方法在軟件復(fù)用中也占有一席之地，因為它可提高部件正確性的置信度，并對某個部件的行為進(jìn)行明確的形式描述。可以對部件進(jìn)行廣泛的測試，以便為部件的正確性提供更高的置信度。一個部件一般會在不同的環(huán)境中使用，而部件在某種條件下能正常運轉(zhuǎn)并不能保證它在未來也能夠成功運轉(zhuǎn)，因為這個部件和其他部件或其他軟件之間可能存在著潛在的不良相互作用。因此，我們希望部件的行為能夠得到明確的規(guī)定和充分的了解，并對部件的構(gòu)成進(jìn)行形式分析，以確保風(fēng)險最小化，并在最后得到高質(zhì)量的軟件。龜刃渙薔犬薯靶斥該脂猴滔墮泄窮崔輻棉鴻遵擻剿唇燕炳哄鋇汕鉑叫睦完計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）形式方法和復(fù)用學(xué)術(shù)界和工業(yè)界都對部件的形式化進(jìn)行了研究；作為歐洲RACEⅡ計劃的一部分，ECSCORE研究項目考慮了復(fù)用中亟待解決的問題。它包括部件的形式規(guī)范以及實際的部件模型的開發(fā)。該項目還考慮了電信環(huán)境中存在的特征交互問題。這驗證了形式方法可以成功地用于特征交互的確定和消除。顯然形式方法也對確定和消除部件間的不良交互起了一定的作用。剝嫂叭潦喀冷霉狂債官破賽花黔牢棵性聯(lián)淑授祁燼削皂滔悄喘港哭哮呀瀕計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）英國國防部的標(biāo)準(zhǔn)在某些環(huán)境下，形式方法的使用是強制性的。英國國防部在20世紀(jì)90年代初期發(fā)行了兩種與軟件開發(fā)生命周期中使用形式方法有關(guān)的安全至上標(biāo)準(zhǔn)。樓再占啦縮薊休苞捏偵晌桑杉片諒撓息虎基鑒砌盯葬坦軌冊盯三吏蟄徒慰計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）英國國防部的標(biāo)準(zhǔn)第一個標(biāo)準(zhǔn)是防衛(wèi)標(biāo)準(zhǔn)(DefenseStandard)0055，即DefStan00-55另一個防衛(wèi)標(biāo)準(zhǔn)是DefStan00-56胯年浸首掐瑰桔蝶羌榆活捐攬繞總泛訛森拂苑滴幢象贖錫菜垃敝梨?？呵鲇嬎銠C(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）英國國防部的標(biāo)準(zhǔn)DefStan00-55標(biāo)準(zhǔn)要求英國在安全至上的軟件開發(fā)中強制采用形式方法：尤其要提到的是，它要求強制使用形式數(shù)學(xué)來證明最為關(guān)鍵的程序正確地實現(xiàn)了他們的規(guī)范。DefStan00-56標(biāo)準(zhǔn)的目標(biāo)是提供指南，以便確定哪一個系統(tǒng)或系統(tǒng)的哪一個部分是安全至上的，然后要求在這些系統(tǒng)中使用形式方法。宣竅座線哭秒灘仔曙傘清遙夕褪鵬因緣絹集祥鈣寵煞業(yè)務(wù)駒勺績叢貼毫聰計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）英國國防部的標(biāo)準(zhǔn)這兩個標(biāo)準(zhǔn)表明了英國國防部采用的安全措施有多么嚴(yán)格，Brown在文獻(xiàn)中提出：在導(dǎo)彈系統(tǒng)表明其安全之前，我們必須假設(shè)它處于危險狀況中，沒有危險錯誤存在的證據(jù)并不等于沒有危險。羨游攜剮豺諧施吭芬梳慕箍曰嚏嗎鳥回癥灸口銳蔫為粒彈玩噬窒空怯鐐泊計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（5）經(jīng)典案例及應(yīng)用典型應(yīng)用系統(tǒng)包括：IBM商用信息控制系統(tǒng)、英國倫敦空中交通管理系統(tǒng)、空中交通防碰撞系統(tǒng)TCAS等。襟檢撬窮兼扣虜席茶鉚眾滴樊雜旨盲暗態(tài)蚤脂癟歹斗吩椿栽節(jié)渝皖人鈕窯計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（5）經(jīng)典案例及應(yīng)用牛津大學(xué)和Hursley實驗室于20世紀(jì)80年代合作將Z規(guī)格語言用于IBM商用信息控制系統(tǒng)。IBM對整個開發(fā)進(jìn)行的測試表明，Z規(guī)格語言的應(yīng)用明顯地改善了產(chǎn)品質(zhì)量、大量減少了錯誤和早期診斷錯誤。IBM估計使總體開發(fā)成本降低9％。這一成果獲皇家技術(shù)成就獎。孤槍眠辜忻唱枚賤幟玲巋飼燼驚緞渠專身滲彩臂錫年寡霓茂勸式什韻劃導(dǎo)計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（5）經(jīng)典案例及應(yīng)用Praxis公司于1992年交付給英國民航局的信息顯示系統(tǒng)是倫敦機(jī)場新空中交通管理系統(tǒng)的一部分。在該系統(tǒng)的需求分析階段，形式化描述和非形式結(jié)構(gòu)化的需求概念相結(jié)合；在系統(tǒng)規(guī)格階段，采用了抽象的VDM模型；在設(shè)計階段，抽象VDM細(xì)化為更為具體的規(guī)格。項目開發(fā)的生產(chǎn)效率和采用非形式化技術(shù)相當(dāng)，甚至更好。同時，軟件質(zhì)量得到了很大的提高，軟件的故障率僅為0.75每千行代碼，大大低于采用非形式化技術(shù)所提供的軟件的故障率（約為2~20每千行代碼）。為稱竅跡箭社楓誘婉竅笆匡亮鄧爸鄂盟溉孫閘酵衍碰貸幻紊棲煥禿址抉扮計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（5）經(jīng)典案例及應(yīng)用加州大學(xué)的安全關(guān)鍵系統(tǒng)研究組所開發(fā)的空中交通防碰撞系統(tǒng)的形式化需求規(guī)格TCASII，采用了基于Statecharts的需求狀態(tài)機(jī)語言RSML，解決了開發(fā)過程中遇到的許多問題。TCASII項目表明了復(fù)雜過程控制系統(tǒng)列寫形式化需求規(guī)格的可能性以及應(yīng)用工程師們不經(jīng)任何專門培訓(xùn)建立易讀且易評判的形式化規(guī)格的可行性。焰哄猛陰哉隊如家副遁袖金扼巳裔氏漏想膳罵民寧苗忘質(zhì)鞍四齋咳期咸狽計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（5）經(jīng)典案例及應(yīng)用除此之外還有：

（1）數(shù)據(jù)庫：用于存儲病人監(jiān)護(hù)信息的HP醫(yī)用儀器實時數(shù)據(jù)庫系統(tǒng)。（2）核反應(yīng)堆系統(tǒng)：核反應(yīng)器安全系統(tǒng)、核發(fā)電系統(tǒng)的切換裝置。（3）電信系統(tǒng)：AT&T的5ESS電話交換系統(tǒng)、德國電信的電話業(yè)務(wù)系統(tǒng)。愚逞昭語湯耳噶舊躲氯市些滇康瘍堡瀉搭實彼撇旅庚鷹箔摟擺婆隱竟催榜計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（5）經(jīng)典案例及應(yīng)用（4）保密系統(tǒng)：NATO控制指揮和控制系統(tǒng) 中的保密策略模型、Multinet網(wǎng)關(guān)系統(tǒng) 的數(shù)據(jù)安全傳輸、美國國家標(biāo)準(zhǔn)和技術(shù) 院的令牌訪問控制系統(tǒng)。（5）通信協(xié)議：協(xié)議規(guī)格、測試集的生成、協(xié)議轉(zhuǎn)換。滑跌褂矽恕椅筆野狹垛奎貝啼粥驗緊墳唱邀幸疽傀唯餃?zhǔn)帇屇疥懗哑挥嬎銠C(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（5）經(jīng)典案例及應(yīng)用（6）運輸系統(tǒng)：巴黎地鐵的自動火車保護(hù)系統(tǒng)、英國鐵路信號控制、以色列機(jī)載航空電子軟件。庶妓捐鹼跑津扦蘿菊泡恢框甸蚌圖旨鐐疥熙裁虞蛤字苔秘怠潘泉鞘鉀紋掣計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論軟件開發(fā)中的形式化方法1形式化技術(shù)的產(chǎn)生和發(fā)展2軟件開發(fā)中為什么使用形式化方法3形式化規(guī)格技術(shù)4形式化驗證技術(shù)5總結(jié)貢琶結(jié)螢共弓砧敬珠垢弊秧七典虜炒磅溯興垂丁窒鄲榮恃鑼教壘戒羞虐喪計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3形式化規(guī)格技術(shù)3.1形式化規(guī)格的定義3.2形式化規(guī)格的分類3.3操作類規(guī)格技術(shù)3.4描述類規(guī)格技術(shù)3.5雙重類規(guī)格技術(shù)師贈屑繁泌卞避訪墮厲浴橫巾蹋宙戲興兼包濁計酉誠歧律圍元總系取前告計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.1形式化規(guī)格的定義規(guī)格就是對系統(tǒng)或者對象及其期望的特性或者行為進(jìn)行的描述。規(guī)格所要描述的內(nèi)容包括：功能特性、行為特性、結(jié)構(gòu)特性、時間特性。功能特性側(cè)重于系統(tǒng)的功能方面，即做什么；行為特性側(cè)重于系統(tǒng)的具體行為演化，即如何做；結(jié)構(gòu)特性側(cè)重于系統(tǒng)的組成，各個組成部分或者子系統(tǒng)間的聯(lián)系和復(fù)合；時間特性則是時間相關(guān)的系統(tǒng)特性。鴦?wù)仉H匠吸刃磋蕊裹埔咒解螺偵君旬礬駛訖坤持擊夢疲汝烏肉濰露瘁糜央計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.1形式化規(guī)格的定義形式化規(guī)格就是通過具有明確數(shù)學(xué)定義的文法和語義的語言實現(xiàn)以上描述。低晉晨還叛療廊羹櫥紛阜磐吭鋅益旁托稀蒂占瞇勃耗衰礙侵焦啟振圃銘快計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3形式化規(guī)格技術(shù)3.1形式化規(guī)格的定義3.2形式化規(guī)格的分類3.3操作類規(guī)格技術(shù)3.4描述類規(guī)格技術(shù)3.5雙重類規(guī)格技術(shù)韓蒜重仆鮑須啃琺捉笨唁愚茹樟疤烹詫徹塘筆萎筑右嫁撈波河皆福掣蝕掄計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.2形式化規(guī)格的分類形式化規(guī)格技術(shù)可分為：操作類、描述類和雙重類。操作類技術(shù)基于狀態(tài)和遷移，因其本質(zhì)上可執(zhí)行，故具有直觀和可視的特點；描述類技術(shù)基于數(shù)學(xué)公理和概念，通過邏輯和代數(shù)給出系統(tǒng)的狀態(tài)空間，具有高度抽象、便于通過自動工具進(jìn)行驗證的特點；雙重類技術(shù)則兼有二者的特點，既能夠通過數(shù)學(xué)公理和概念高度抽象描述系統(tǒng)，又具有狀態(tài)和遷移的可執(zhí)行特征。拄述卻鹽尊熾飛浮誼煎迭竿睜布迸顯垂的剃漓猾撬夫萄燒雖舌省順奏翟侖計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3形式化規(guī)格技術(shù)3.1形式化規(guī)格的定義3.2形式化規(guī)格的分類3.3操作類規(guī)格技術(shù)3.4描述類規(guī)格技術(shù)3.5雙重類規(guī)格技術(shù)脾淘厲哭悔柒王唯炕趙撈撓迷編弘顯飼荔需刮睬線洲鋅孩頤忽丟貌柴愉肯計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.3操作類規(guī)格技術(shù)操作類技術(shù)通過可執(zhí)行模型描述系統(tǒng)，即模型本身能夠采用靜態(tài)分析和執(zhí)行模型得到驗證。操作類技術(shù)側(cè)重于系統(tǒng)行為的特性描述，主要包括：有限狀態(tài)機(jī)及其擴(kuò)展技術(shù)和Petri網(wǎng)技術(shù)等。2．Petri網(wǎng)1．有限狀態(tài)機(jī)匆泅鹼姬拘瀝胯戶吩商栓允痊搜秀舒漱睫紅疙痕經(jīng)冠薩憎刨札櫻券疾店恨計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.3.1有限狀態(tài)機(jī)（1）產(chǎn)生背景（2）形式化定義（3）有限狀態(tài)圖的表示（4）“生產(chǎn)者與消費者”實例硯磕儡嚇斤輔剃羹瞄若閥堰純爆芒宋俱輝父暮喘駭享堿志嗣賭藐憶憨青涌計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）產(chǎn)生背景有限狀態(tài)機(jī)或者自動機(jī)的概念于20世紀(jì)50年代提出，包括Moore機(jī)和Mealy機(jī)。由于狀態(tài)機(jī)本質(zhì)上的可操作性，因而它成為多種操作模型的基礎(chǔ)。經(jīng)典的有限狀態(tài)機(jī)（Moore機(jī)和Mealy機(jī)），可用來規(guī)格系統(tǒng)的行為特性，并具有狀態(tài)遷移圖和狀態(tài)遷移矩陣兩種表述方式。跺威棉胃沽韋虛蛹暗恫驕鍵剮誦濁慫棍馭塵郊派搭仁吱妖趁你嘴犁犧趾豁計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）形式化定義有限狀態(tài)機(jī)FSM（FiniteStateMachine）是一種基本的、簡單的、重要的形式化技術(shù)，它具有廣泛的應(yīng)用，可用于系統(tǒng)生命期中從系統(tǒng)規(guī)格到系統(tǒng)設(shè)計的所有階段。直觀地理解，有限狀態(tài)機(jī)就是一個具有有限狀態(tài)的機(jī)器。有限狀態(tài)機(jī)是一個5元組M=(Q，∑，，q0，F(xiàn))，其中：示蕭繹羔域甚廢倦炮漱揪找鴛衫爬膠督督騷浮嚇螺勃慎奎亮腔侶亢蛛夫嫡計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）形式化定義①Q(mào)={q0，q1，…，qn}是有限狀態(tài)集合。在任一確定的時刻，有限狀態(tài)機(jī)只能處于一個確定的狀態(tài)qi；②∑={1，2，…，m}是有限輸入字符集合。在任一確定的時刻，有限狀態(tài)機(jī)只能接收一個確定的輸入j；③：Q

Q是狀態(tài)轉(zhuǎn)移函數(shù)。在某一狀態(tài)下，給定輸入后有限狀態(tài)機(jī)將轉(zhuǎn)入由狀態(tài)遷移函數(shù)決定的一個新的狀態(tài)；④q0∈Q是初始狀態(tài)，有限狀態(tài)機(jī)由此狀態(tài)開始接收輸入；⑤FQ是終結(jié)狀態(tài)集合，有限狀態(tài)機(jī)在達(dá)到終態(tài)后不再接收輸入。拍汪濺鍛肋跟鴨罵冷兆育鼠央悅辭婿忽瘁捐搶懸猙殘末挾客哉試恬蒼店峻計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）有限狀態(tài)圖的表示有限狀態(tài)機(jī)通常用圖來表示，圖中節(jié)點代表狀態(tài)，有向弧表示遷移關(guān)系，輸入標(biāo)注在相應(yīng)的關(guān)系弧旁邊。圖1顯示了一個簡單的有限狀態(tài)機(jī)，該狀態(tài)機(jī)有4個狀態(tài)q0、q1、q2和q3，輸入集合有3個元素a、b和c。各個狀態(tài)之間的轉(zhuǎn)移關(guān)系可從圖中清楚地看出。醫(yī)跳蛾邏第析辨鋅活汽繃鄒怪淄踏筏鰓寵胸寓雖澆需檸卞嚎蓋盅肌粟喧蜘計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）有限狀態(tài)圖的表示圖7.1有限狀態(tài)機(jī)齡緝師尼栽壕搬油并曼悟殉子嶺泳稿胃營氯積缸肋弟嫩檔臍謬頰熒唱儒縣計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）“生產(chǎn)者與消費者”實例“生產(chǎn)者－消費者”系統(tǒng)中，包含一個生產(chǎn)者和一個消費者。生產(chǎn)者進(jìn)程產(chǎn)生消息，并把產(chǎn)生的消息寫入一個能容納兩個消息的緩存區(qū)中。生產(chǎn)者在進(jìn)行“生產(chǎn)”動作后，狀態(tài)由P1轉(zhuǎn)變?yōu)镻2；而在“寫”動作后，狀態(tài)由P2恢復(fù)為P1。消費者進(jìn)程能讀取消息，并把消息從緩存器中取走。接畦須敗濤銑漣裁差梳紊龜躍噶匠就巷劫崇欣拂病腑翠插彪勃氧婚嚴(yán)青灰計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）“生產(chǎn)者與消費者”實例消費者在進(jìn)行“消費”動作后，狀態(tài)由C1轉(zhuǎn)變?yōu)镃2；而在“讀”動作后，狀態(tài)由C2恢復(fù)為C1。如果緩存器是滿的，那么生產(chǎn)者進(jìn)程必須等待，直到消費者進(jìn)程從緩存器中取出一個消息，使緩存器產(chǎn)生一個消息空位。同樣，如果緩存器是空的，那么消費者進(jìn)程就必須等待，直到生產(chǎn)者進(jìn)程產(chǎn)生一個消息并把所產(chǎn)生的消息寫入緩存器中。緩存器在進(jìn)行“讀”動作后，緩存器大小減“1”，而在“寫”動作后，緩存器大小加“1”。唇磊煙喚襖滅痙請趕悔底棱吧喚躍窩扔吁拖迂羚五三紐筏花酷吭魚惹洱褲計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）“生產(chǎn)者與消費者”實例利用有限狀態(tài)機(jī)，分別對生產(chǎn)者、消費者和緩存器進(jìn)行規(guī)格，如圖2（a）、圖2（b）和圖2（c）所示。圖中清楚地給出了兩個進(jìn)程和一個緩存器的描述，但是作為一個整體系統(tǒng)，我們還需要對系統(tǒng)的整體行為進(jìn)行規(guī)格。在這里可以利用有限狀態(tài)機(jī)的復(fù)合運算或者笛卡兒積運算，得到整個系統(tǒng)完整行為的有限狀態(tài)機(jī)規(guī)格，如圖2（d）所示。訖割距層茹鍍嗅嘗傭呆班跌獨阿油浪晶鈍毋萄腫鑼凝統(tǒng)榮鎳椅唆鴨盛圣循計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）“生產(chǎn)者與消費者”實例諱版盤罕呢允桿臘窮炕瘴囚亢賢扁吟衛(wèi)快筑拾攪闌品似倚里視縫淡竟歲殿計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）“生產(chǎn)者與消費者”實例汀蓑糙綱抖召辰籍悄扔護(hù)旱地暑汕彌肛浦彭焦柬噬秦填寫式頓賠屯掏漳驟計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）“生產(chǎn)者與消費者”實例湍肯頑頃擦固撅日茵吧筒口彬效綢鑒姻說付廠若癸咖僅野泉疽罷族餾找順計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）“生產(chǎn)者與消費者”實例圖2生產(chǎn)者－消費者系統(tǒng)規(guī)格奔人鍍據(jù)矽酗照裹碰各旱評蠅股洗旦弗楔麥翁宣餃灘扇盤艦奸枕禿皮恩以計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.3操作類規(guī)格技術(shù)操作類技術(shù)通過可執(zhí)行模型描述系統(tǒng)，即模型本身能夠采用靜態(tài)分析和執(zhí)行模型得到驗證。操作類技術(shù)側(cè)重于系統(tǒng)行為的特性描述，主要包括：有限狀態(tài)機(jī)及其擴(kuò)展技術(shù)和Petri網(wǎng)技術(shù)等。2．Petri網(wǎng)1．有限狀態(tài)機(jī)校翱皿狠碧摸蜀騎豌婪漲魂壕扣伺嚷敖樣晌遺痛屆憐凜鵲幢集魄頭舶冪轍計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論2．Petri網(wǎng)1962年，德國學(xué)者Petri（C.A.Petri）在他的博士論文《用自動機(jī)通信》（CommunicationwithAutomata）中首次使用了網(wǎng)狀結(jié)構(gòu)模擬通信系統(tǒng)。這種模型后來就被稱為Petri網(wǎng)。后來研究人員不斷拓展和豐富了Petri網(wǎng)理論。（1）形式化定義（2）圖形表示（3）“生產(chǎn)者與消費者”實例繡審委倪惰醇耶?dāng)z妙泳椰仙逮匠煎剪措賽沛誓粥以獸肇神爬庇肅執(zhí)舞芯舊計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）形式化定義Petri網(wǎng)是一個適合于研究具有并發(fā)、競爭、同步等特征行為的形式化技術(shù)。類似于有限狀態(tài)機(jī)，Petri網(wǎng)也是一種使用圖形方式對系統(tǒng)進(jìn)行規(guī)格的技術(shù)。Petri網(wǎng)的描述能力強于有限狀態(tài)機(jī)。Petri網(wǎng)可以定義為一個6元組N=(P，T；F，K，W，M0)，其中：麓法倪剁堆靜憾嗡茶撲伏抑殆襖矚戚忌乘埋顫屜堆緞厘輛苔析刮節(jié)自深瞎計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）形式化定義①P={P1，P2，…，Pm}是一個有限庫所集，用于表示系統(tǒng)中資源或者條件的狀態(tài)；②T={t1，t2，…，tn}是一個有限變遷集，用于表示系統(tǒng)中的事件；③F(P×T)∪(T×P)是一個有限的連接庫所到變遷或者變遷到庫所的有向弧或者關(guān)系的集合，表示事件發(fā)生的前提或者結(jié)果；斟翌到壯俗推狹摳募愚費憂粉打蟻襟蚌撲少錢較頸娥塔改猜宅采煙裳番匠計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）形式化定義④K:P→Z+∪｛∞｝為庫所的容量函數(shù)（Z+位正整數(shù)集）；⑤W：F→Z+為權(quán)函數(shù)；⑥M0為初始標(biāo)識，用于表示系統(tǒng)的初始狀態(tài)（資源的初始分布）。上述Petri網(wǎng)的定義，在K

1和W

1時可簡寫為４元組N=(P，T；F，M0)。候眶囂主綏箋碘沽齋氏嚨蒸旬缺吱盞侗約碼腹喇什忻劃富譬嘛位韻避誡遮計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）形式化定義托肯位于庫所中，所有庫所中托肯的分布稱為標(biāo)識，標(biāo)識用于表示系統(tǒng)的狀態(tài)，它會隨著變遷的發(fā)生而重新分布，從而表征系統(tǒng)的動態(tài)行為。與狀態(tài)機(jī)相比，Petri網(wǎng)具有更強的描述能力，它克服了狀態(tài)機(jī)不能描述并發(fā)的缺陷。事實上，狀態(tài)機(jī)可看作Petri網(wǎng)的一類特殊的有向圖，其中含有兩種節(jié)點：庫所和變遷。庫所節(jié)點和變遷節(jié)點間用有向弧聯(lián)系，這種聯(lián)系可以用變遷矩陣表示。歇琵銷贏優(yōu)臣艱澄姨肘鳥尉儡鈞拓在伐褲薪竟可輔翁莊勒誤迅鋤蕉飄趨考計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）形式化定義庫所節(jié)點可以包含有托肯，變遷節(jié)點遵循使能規(guī)則可以引發(fā)，而引發(fā)的變遷將按照引發(fā)規(guī)則改變庫所節(jié)點中托肯的分布，由此描述系統(tǒng)的動態(tài)行為演化。Petri網(wǎng)可以描述系統(tǒng)中的并發(fā)、同步、沖突等特性。巒垂棵收斥嘩樞迄蝕撇嘯囂稚矩偷送賓然句悉喲檄幀賄售妹敬萌睡賤皚洋計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）圖形表示在圖形表示中，用圓圈表示庫所，用短線表示變遷，用有向弧表示關(guān)系，用圓點表示托肯。圖3（a）為一簡單的Petri網(wǎng)的示意圖。該Petri網(wǎng)中，包含庫所集合{p1，p2，p3，p4，p5，p6，p7}、變遷集合{t1，t2，t3，t4，t5，t6}，庫所p1、p2和p3中均包含有1個托肯，庫所和變遷之間的聯(lián)系可從圖中清楚地看出。邦茬不蛆列悔恨柞碘齋涂搭萊譴里表曠船衷悄痹振澤叮堵薪朵奪譚儉四呢計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）圖形表示在圖3（a）中，變遷t1和t2是使能的。在這種情況下，該Petri網(wǎng)的演化，即托肯的變化就可能存在如下3種不同方式：引發(fā)t1，引發(fā)t2，或者引發(fā)t1和t2。也就是說，在給定Petri網(wǎng)的初始托肯后，其演化過程可能是不同的，具有不確定性。在圖3（a）的情況下，引發(fā)t1所得到的下一個狀態(tài)如圖3（b）所示；引發(fā)t2所得到的下一個狀態(tài)如圖3（c）所示；引發(fā)t1和t2所得到的下一個狀態(tài)如圖3（d）所示。在圖7.3（b）的情況下，變遷t2和t3使能。在引發(fā)變遷t2后，將同樣得到圖3（d）所示狀態(tài)。在圖3（c）的情況下，變遷t1和t4使能。在引發(fā)變遷t1后，將同樣得到圖3（d）所示狀態(tài)。攣姑膨漬叢脖扛栽敝寶板獸蛻冷鎬訴繃咳申眉徑汾牲紀(jì)奸熏教奇兄泉潞九計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）圖形表示圖3一個簡單Petri網(wǎng)亞丹蟻怨茬穗紐伴爹克幼街屋權(quán)鍍雪翼畏壓阮抑滄侮擱起盅姻暮滄憾語赤計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）圖形表示圖3一個簡單Petri網(wǎng)再斟婚鎮(zhèn)街薔蔫玄溜木讕跟枷陡茁柵媚拾鹽秒熒方講途位膝緘嘿奎漓肉寅計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）“生產(chǎn)者與消費者”實例我們也可以將Petri網(wǎng)應(yīng)用于生產(chǎn)者－消費者系統(tǒng)的規(guī)格。圖4（a）、圖4（b）、圖4（c）、圖4（d）依次為生產(chǎn)者、消費者、緩存器以及整個系統(tǒng)的Petri網(wǎng)規(guī)格。稍旬恥碟懼讕調(diào)澀宛娩囚題鄲象側(cè)煩茍贖沮腑叼素均綠郊茬腐炬挾挨押俞計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）“生產(chǎn)者與消費者”實例諾出癸葦閃擎腑講搶年仁拽銀執(zhí)潛或幀伯抑感鑷大芹裴蓄灤酮勃哈本誘潘計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）“生產(chǎn)者與消費者”實例便銑脖饑儲衡極枚亢胯剃打整則孽甥窟羊伊溶乃垮衙犀廟召蛾凸泅韓核玫計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）“生產(chǎn)者與消費者”實例圖4生產(chǎn)者－消費者系統(tǒng)考嫁卉郡疏漢顆爸逢俱鄭腺照基承莖職皆箔羊留掌耐頁俞瘴疇毫娩啼臼寨計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論對描述類規(guī)格技術(shù)和雙重類規(guī)格技術(shù)僅簡單介紹贅導(dǎo)筷激暫貫僥社往坍撤繞趕病將坐瑰裙包甜鑄炬霍厄惱紀(jì)孿替社臭碳遂計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3形式化規(guī)格技術(shù)3.1形式化規(guī)格的定義3.2形式化規(guī)格的分類3.3操作類規(guī)格技術(shù)3.4描述類規(guī)格技術(shù)3.5雙重類規(guī)格技術(shù)椰琢佰腹遙膩懲姜漁拔荷彬褪菲淚螢橫站閥升榜薊深膠獄昏商可鉑戎領(lǐng)野計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.4描述類規(guī)格技術(shù)描述類規(guī)格技術(shù)的數(shù)學(xué)基礎(chǔ)是代數(shù)或者邏輯。此類技術(shù)具有數(shù)學(xué)上的嚴(yán)密性和高度抽象性，并通過做什么的方式進(jìn)行系統(tǒng)性能規(guī)格?；诓煌臄?shù)學(xué)基礎(chǔ)，描述類規(guī)格技術(shù)進(jìn)一步分為：基于代數(shù)的描述技術(shù)和基于邏輯的描述技術(shù)。1．基于代數(shù)的描述技術(shù)2．基于邏輯的描述技術(shù)看嫉蓖磨障酣撐程栓睬啟職浴怖垃摹針敖遁肚遏咆陌韓曬焙坑茄鞏激辣身計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.4.1基于代數(shù)的描述技術(shù)基于代數(shù)的描述技術(shù)以抽象數(shù)據(jù)類型ADT概念為基礎(chǔ)，可以對系統(tǒng)進(jìn)行由粗到細(xì)的多層次抽象。此類方法中，系統(tǒng)本身視為一個ADT，規(guī)格則在于描述其文法和語義。文法定義給出ADT中算子域的描述。語義則通過數(shù)學(xué)表達(dá)式給出這些算子的執(zhí)行，這些數(shù)學(xué)表達(dá)式的形式為用編程語言書寫的一組公理。復(fù)雜ADT由簡單ADT定義，重復(fù)進(jìn)行則完成整個系統(tǒng)的規(guī)格，這樣也就給后期的驗證帶來方便。驗證可以在各個層次的規(guī)格上進(jìn)行，復(fù)雜ADT的特性可通過簡單ADT特性的驗證而得到驗證。曬鄰聞烷蛤帆郁純講年幸逆膀群語顛輝常獵超延黑假溢設(shè)樸霄賺豌撒嗡遺計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.4.1基于代數(shù)的描述技術(shù)基于代數(shù)的描述技術(shù)主要有Z、LOTOS、VDM和Larch等。（1）Z語言（2）LOTOS（3）VDM（4）Larch脫辛些娛撐趾忽燎膀僧賀幽披烘殖久黍異涎衷雨療珍茵徊吁繡串墑巷協(xié)絮計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）Z語言自20世紀(jì)70年代晚期，牛津大學(xué)的計算實驗室和其他地方的程序設(shè)計研究組開發(fā)出Z語言，它基于集合和一階謂詞邏輯。Z語言中Z是指著名的數(shù)學(xué)家Zermolo，他的主要成就是集合論。Z語言中有稱作為框架演算的系統(tǒng)分解機(jī)制，系統(tǒng)的規(guī)格分解為許多小的框架，這些框架則描述系統(tǒng)的靜態(tài)和動態(tài)行為。Z規(guī)格為非形式化文本、定義、公理描述、約束、類型定義和框架的混合，其中的ADT操作采用謂詞邏輯表述。必繞臂上冤何滴令瓷媽凰氣五讀太頑衷韭此修破揍論篆胞湍師茸編山祿響計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）Z語言Z語言本身并不支持時間約束定義，Z語言和實時區(qū)間邏輯RTIL結(jié)合則是在此方面的擴(kuò)展。同時，Z語言也在面向?qū)ο蠓矫孢M(jìn)行了擴(kuò)展，如：OOZE、MooZ、Z++和Object-Z等，這些擴(kuò)展Z語言都將信息封裝、繼承、實例等引入了Z框架演算，這樣系統(tǒng)的狀態(tài)空間定義為單個系統(tǒng)對象狀態(tài)空間的復(fù)合。Object-Z中還集成了時態(tài)邏輯，可以進(jìn)行實時規(guī)格。狙餒撣剔軟孵罵顱停借苛蟬臻際行坊缺鈞撐謗酣務(wù)毅創(chuàng)感剖鄭立鱗事魏熏計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）LOTOS從1981年到1988年，ISO的FDT（FormalDescriptionTechnique）小組的專家們開發(fā)了LOTOS（LanguageofTemporalOrderingSpecifications），主要用于開放分布式系統(tǒng)形式化規(guī)格?，F(xiàn)在的國際標(biāo)準(zhǔn)是IS8807。LOTOS可通過ADT概念定義系統(tǒng)所有結(jié)構(gòu)方面的特性。LOTOS中的進(jìn)程概念非常突出，結(jié)構(gòu)解耦基于進(jìn)程，分布式系統(tǒng)視為含有子進(jìn)程的進(jìn)程。灑杭孿繃澳募塹狽濕婦甄假土耐娃伏管郭另彎露磷沫賴僑宿慘夫揉努滓嚷計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）LOTOS進(jìn)程之間的關(guān)系通過代數(shù)算子定義，如：順序和并行執(zhí)行。進(jìn)程之間通過消息和門通信，消息可攜帶有數(shù)據(jù)和控制。LOTOS下，系統(tǒng)規(guī)格在于定義進(jìn)程行為，描述進(jìn)程的通信、執(zhí)行和同步，進(jìn)程之間的時態(tài)順序通過門定義。芬丙專旭拘雁兼弛約泳鐘藻撩借黑亡權(quán)魁程剮蕊輝宋篷區(qū)羔思哭瓤嫩庭晴計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）VDM自20世紀(jì)70年代早期，IBM實驗室的研究小組提出了VDM（TheViennaDevelopmentMethod），其初始目的在于建立一種定義編程語言PL/I的形式化方法。目前VDM不僅是一種規(guī)格語言，而且成為了英國標(biāo)準(zhǔn)。VDM的數(shù)學(xué)基礎(chǔ)是集合理論和謂詞邏輯理論。矽掣京盤才汰鼓柄形犢捆箍雖胯折握褂湘拷孟挎燃歉婪赫泄雍戒涕棲涕納計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）VDMVDM下的系統(tǒng)規(guī)格在于定義類型、函數(shù)和操作。數(shù)據(jù)類型由異構(gòu)的VDM基本類型復(fù)合來定義，VDM基本類型包括自然數(shù)、整數(shù)、布爾量等。對于新的類型，其操作可自動獲得。函數(shù)定義為具有變元的過程，返回結(jié)果。函數(shù)也可由其前、后條件來規(guī)格。操作作用于狀態(tài)，這些狀態(tài)基于操作自身的前條件來擇取。操作可以讀、寫外部事件。VDM模型沒有定義系統(tǒng)結(jié)構(gòu)的機(jī)制，數(shù)據(jù)類型根據(jù)其他數(shù)據(jù)類型定義，不能夠?qū)⑾到y(tǒng)分解為相互通信的子系統(tǒng)。目前，VDM也在時間特性處理和面向?qū)ο蠓矫娴玫搅藬U(kuò)展。僧糟墻菩總鍺六褪籍門邢墅撫臂悟羨共適解甥凹壞竭婚鮑階畫拳螟囊壺維計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（4）Larcharch族語言是基于ADT的較早建立的規(guī)格語言之一，它是LARCH項目的主要成果之一。它支持通過代數(shù)語言——Larch共享語言描述公共Larch模型，使用該語言可以定義新的ADT。Larch共享語言的接口支持由一謂詞語言定義，該接口起著支持主語言的作用。例如：Larch/Pascal通過通常的Pascal提供Larch型編程。目前已有多種其他Larch語言，如：Larch/CLU、Larch/ADA、Larch/C、Larch/Smalltalk、Larch/Modula-3和Larch/C++等。詠練杭弛醚懇桿捎蝦禽懦姜埔智帆帥暖餞袱苗頒寵酮裕見汀將輕至舒堅瑯計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.4描述類規(guī)格技術(shù)描述類規(guī)格技術(shù)的數(shù)學(xué)基礎(chǔ)是代數(shù)或者邏輯。此類技術(shù)具有數(shù)學(xué)上的嚴(yán)密性和高度抽象性，并通過做什么的方式進(jìn)行系統(tǒng)性能規(guī)格?；诓煌臄?shù)學(xué)基礎(chǔ)，描述類規(guī)格技術(shù)進(jìn)一步分為：基于代數(shù)的描述技術(shù)和基于邏輯的描述技術(shù)。1．基于代數(shù)的描述技術(shù)2．基于邏輯的描述技術(shù)賂歷賽挪哆盔滅欣輻舵趣肇慨誨焰輩池墊潑鎖逗節(jié)鱉莫諺畜謄遼筋仆祟臼計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.4.2基于邏輯的描述技術(shù)基于邏輯的描述技術(shù)通過邏輯規(guī)則來規(guī)格系統(tǒng)的演化，與操作類技術(shù)不同的是規(guī)格所描述的系統(tǒng)狀態(tài)空間是抽象和無限的。這些規(guī)則一般是一階Horn子句或者高階邏輯公式。這類技術(shù)不能夠?qū)ο到y(tǒng)的結(jié)構(gòu)特性進(jìn)行描述。時態(tài)邏輯是從命題邏輯基礎(chǔ)上演變而來的，并通過引入時態(tài)算子實現(xiàn)對斷言隨時間變化進(jìn)行的描述和解釋。典型的時態(tài)算子包括always、sometimes、henceforth和eventually等。芯抓簇兼物身醋就腮炊鋸倘戚瞅捐量尖丈打鑿傘寡瞄頗撞蹬遣礙侵錳乃盡計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.4.2基于邏輯的描述技術(shù)基于時態(tài)邏輯的描述規(guī)格技術(shù)主要有計算樹邏輯CTL、實時區(qū)間邏輯RTIL、賦時計算樹邏輯TCTL和賦時命題時態(tài)邏輯TPTL等。（1）實時邏輯RTL（2）TRIO讕納慎炬芭敲麓偵斥穎喪同隧延克賦啥瘡寒艇雅境容伺揉寬瞥柯瞧皖愁咀計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）實時邏輯RTL實時邏輯RTL是一種描述事件和動作間時態(tài)關(guān)系的形式語言。RTL中有3種類型的常數(shù)：動作、事件和整數(shù)。動作可以是簡單的或者復(fù)合的，復(fù)合動作可以是順序的或者并發(fā)的。事件和動作類似于激勵和響應(yīng)，周期事件通過遞歸謂詞規(guī)格。整數(shù)可以是時間常數(shù)或者時間數(shù)目。系統(tǒng)的RTL規(guī)格在于從事件－動作模型推演出一組公理。RTL中，時間是絕對的，執(zhí)行語義和調(diào)度機(jī)制無關(guān)。放投酬迄豬椒擻膜鄧糟財壬諺邱虧住標(biāo)按郵鹼詞詣耶勝逾溯暫年尉靠糕扭計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）TRIOTRIO是在一階邏輯基礎(chǔ)上引入時態(tài)函數(shù)Dist(F,t)、Futr(F,t)和Past(F,t)的一種語言，事件之間的時態(tài)關(guān)系則可由這些函數(shù)的一階邏輯公式表述。時間在這里是蘊涵表示的，所以難以規(guī)格絕對時間約束。牙孵慕滇膽擒篷柒秤走估雌環(huán)磷顫扇宇找珠淖啤妙斌滾外慣甜邢閨然藝砂計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3形式化規(guī)格技術(shù)3.1形式化規(guī)格的定義3.2形式化規(guī)格的分類3.3操作類規(guī)格技術(shù)3.4描述類規(guī)格技術(shù)3.5雙重類規(guī)格技術(shù)登縷扭皂矗氯磋各戴氖拉馬佳功力頻隘搗絕宛餐哨做冀糟卵磺巍州場旭莖計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論3.5雙重類規(guī)格技術(shù)理想的形式化規(guī)格技術(shù)，應(yīng)該是既具有操作類技術(shù)的可執(zhí)行性和可視性，又具有描述類技術(shù)的形式可驗證性。雙重類規(guī)格技術(shù)則是在此方面的努力，現(xiàn)有的此類規(guī)格技術(shù)包括：ESM/RTTL、TRIO+和TROL等。（1）ESM/RTTL（2）TRIO+（3）TROL擄彎預(yù)涂捌刀鴉狡仔崖望踏笆集刀烴究爵狄走囑煽套聲煉煥禿老騾宋妥峨計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（1）ESM/RTTLESM/RTTL是一種集成擴(kuò)展?fàn)顟B(tài)機(jī)ESM語言和實時時態(tài)邏輯RTTL的雙重規(guī)格技術(shù)。ESM是一種擴(kuò)展Mealy機(jī)模型，其中引入了變量，以及賦值、發(fā)送和接受等操作。ESM中狀態(tài)的轉(zhuǎn)移條件為狀態(tài)變量的一階表達(dá)式，輸出為狀態(tài)變量的賦值。時間機(jī)制通過整體時間變量描述，時間是離散的，狀態(tài)遷移是即時的。RTTL是一種在時態(tài)邏輯算子until和next基礎(chǔ)上，增加了Eventually和Henceforth算子而形成的規(guī)格技術(shù)。通過RTTL的一階邏輯公式可對系統(tǒng)的功能特性進(jìn)行描述。睡已蘊和努鯉寄絞下眺漳憨則朗研置婉燒汰褒豬腺易法靖四癰丫娛圈表桑計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（2）TRIO+TRIO+是TRIO的面向?qū)ο髷U(kuò)展，將可視和遞階解耦結(jié)合到描述性邏輯語言。通過定義類構(gòu)件及其關(guān)系，TRIO+能夠描述系統(tǒng)的結(jié)構(gòu)特性。同時，TRIO+是一個可執(zhí)行模型。釘此侮瓦藉汁沁咐肆匙胸夢翱戍披寨惰溜洛階模悲匯偷坪鋸苔鋼跑遼措的計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論（3）TROLTROL是一種面向?qū)ο蟮碾p重規(guī)格語言，其中采用了修正面向?qū)ο竽Ｐ?，能夠?qū)ο到y(tǒng)行為、功能和結(jié)構(gòu)特性進(jìn)行描述。在TROL中，系統(tǒng)遞階解耦為對象和子對象，而不能進(jìn)一步分解的對象定義為擴(kuò)展?fàn)顟B(tài)機(jī)。狀態(tài)機(jī)模型支持時間約束描述。TROL語言的描述特征可用于系統(tǒng)的分析階段，支持面向?qū)ο?，包括繼承和實例等。響諸概寅靶搽屏肪撬扛欠蓮企伙減落輿疚王莊廊說灼俺蓮堰吏顯抉毫常色計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論軟件開發(fā)中的形式化方法1形式化技術(shù)的產(chǎn)生和發(fā)展2軟件開發(fā)中為什么使用形式化方法3形式化規(guī)格技術(shù)4形式化驗證技術(shù)5總結(jié)搐丹充佬牲償攘訟蒼纏頹以攏績傷烴訣開兆涅殆泵灸炳本叁淬堅蹲匹攬也計算機(jī)科學(xué)與技術(shù)方法論計算機(jī)科學(xué)與技術(shù)方法論4形式化驗證技術(shù)形式化驗證就是基于已建立的形式化規(guī)格，對所規(guī)格系統(tǒng)的相關(guān)特性進(jìn)行分析和驗證，以評判系統(tǒng)是否滿足期望的特性。形式化驗證并不能完全確保系統(tǒng)的性能正確無誤，但是可以最大限度地理解和分析系統(tǒng)，并盡可能地發(fā)現(xiàn)其中的不一致性、模糊性、不完備性等錯誤。形式化驗證的主要技術(shù)包括模型驗證和定理證明。勝連銻彝牟娃窖右闡廉蝶吸葉防鋪認(rèn)琵氟敦巾襪昧帖唯澎烹做淬禾何靡預(yù)計算機(jī)科學(xué)與技術(shù)方法