軟件開發(fā)的形式化方法

前言

軟件是計(jì)算機(jī)應(yīng)用系統(tǒng)中不可分割的一個(gè)重要組成部分。在商務(wù)數(shù)據(jù)庫(kù)管理、宇宙飛船、機(jī)器人、飛機(jī)控制、通信系統(tǒng)、核電站控制、制造自動(dòng)化等系統(tǒng)中，軟件發(fā)揮著不可替代的作用。但在軟件設(shè)計(jì)和開發(fā)中會(huì)遇到不少困難和問(wèn)題。嚴(yán)謹(jǐn)?shù)能浖_發(fā)和設(shè)計(jì)方法——形式化方法，為解決或部分解決這些困難提供了可行途徑。形式化方法是基于嚴(yán)密的、數(shù)學(xué)上的形式機(jī)制的系統(tǒng)研究方法?？陀^地講，有了數(shù)學(xué)的應(yīng)用，就有了形式化方法。但是，一般認(rèn)為形式化方法是始于20世紀(jì)60年代末的Floyd、Hoare和Manna等在程序正確性證明方面的研究，當(dāng)時(shí)由于“軟件危機(jī)”，人們?cè)噲D用數(shù)學(xué)方法證明程序的正確性而發(fā)展成為了各種程序驗(yàn)證方法，但是受程序規(guī)模的限制，這些方法并未達(dá)到預(yù)期的應(yīng)用效果。從20世紀(jì)80年代末開始，由于在硬件設(shè)計(jì)領(lǐng)域形式形式化方法的工業(yè)應(yīng)用的結(jié)果，掀起了形式化方法和技術(shù)的學(xué)術(shù)研究和工業(yè)應(yīng)用的熱潮。在建立軟件設(shè)計(jì)和開發(fā)的形式基礎(chǔ)方面，研究人員已開展了大量的工作，建立了一些較為成熟并初步進(jìn)入應(yīng)用的方法和語(yǔ)言，例如：Statecharts、Petri 網(wǎng)、通信系統(tǒng)演算、程序正確性證明、時(shí)態(tài)邏輯、模型檢驗(yàn)、Z、VDM、Larch等。從廣義角度，形式化方法是軟件開發(fā)過(guò)程中規(guī)格、設(shè)計(jì)及實(shí)現(xiàn)的系統(tǒng)工程方法。狹義地，形式化方法是軟件規(guī)格和驗(yàn)證的方法，因此，形式化方法又分為形式化規(guī)格方法和形式化驗(yàn)證方法。形式化規(guī)格就是通過(guò)數(shù)學(xué)符號(hào)對(duì)系統(tǒng)及行為進(jìn)行精確、簡(jiǎn)潔的描述。任何大型系統(tǒng)開發(fā)的前提都是需求規(guī)格。沒(méi)有這樣的規(guī)格，系統(tǒng)開發(fā)人員就沒(méi)有一個(gè)系統(tǒng)用戶的確切描述，這些用戶就不得不從多個(gè)方面承擔(dān)不明確規(guī)格帶來(lái)的誤錯(cuò)后果。精確的需求規(guī)格已被大多數(shù)工程學(xué)科所接受，計(jì)算機(jī)系統(tǒng)在精確性方面并不比任何其他工程任務(wù)差。然而，不幸的是，當(dāng)今的軟件工業(yè)實(shí)踐在很大程度上還依賴于非形式文本和圖形。形式化的另一個(gè)方面是設(shè)計(jì)的驗(yàn)證。程序是數(shù)學(xué)化的文本，這樣就有可能解釋程序和它們規(guī)格之間的形式關(guān)系?；谛问交椒?，可以建立軟件或程序在各種情形下性質(zhì)及行為的描述。系統(tǒng)開發(fā)的步驟可以基于形式化規(guī)格，也可以針對(duì)形式化規(guī)格來(lái)驗(yàn)證。這樣，在開發(fā)過(guò)程中就可以采用形式化驗(yàn)證以及時(shí)檢查出誤錯(cuò)。開發(fā)過(guò)程中盡早地消除誤錯(cuò)是改善軟件開發(fā)過(guò)程質(zhì)量的關(guān)鍵之一，也是工業(yè)應(yīng)用中采用形式化方法的一個(gè)重要理由。

內(nèi)容概要

形式化方法是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上、具有精確數(shù)學(xué)語(yǔ)義的開發(fā)方法。從廣義角度，形式化方法是軟件開發(fā)過(guò)程中分析、設(shè)計(jì)及實(shí)現(xiàn)的系統(tǒng)工程方法。狹義地，形式化方法是軟件規(guī)格和驗(yàn)證的方法。本書對(duì)軟件開發(fā)中的形式化方法進(jìn)行了介紹和討論，內(nèi)容涵蓋了SE2004中關(guān)于“軟件的形式化方法”的知識(shí)點(diǎn)，主要包括：有限狀態(tài)機(jī)、Statecharts、Petri網(wǎng)、通信順序進(jìn)程、通信系統(tǒng)演算、一階邏輯、程序正確性證明、時(shí)態(tài)邏輯、模型檢驗(yàn)、Z、VDM、Larch等。　　本書可作為計(jì)算機(jī)、軟件工程等專業(yè)高年級(jí)本科聲或研究生的教學(xué)用書，也可供相關(guān)領(lǐng)域的研究人員和工程技術(shù)人員參考。

書籍目錄

第1章　軟件及其開發(fā)概述　1.1　軟件開發(fā)的歷史　1.2　軟件危機(jī)　1.3　軟件工程　1.4　形式化方法　習(xí)題第2章　有限狀態(tài)機(jī)及其擴(kuò)展　　2.1　有限狀態(tài)機(jī)　2.2　Statecharts　習(xí)題第3章　Petri網(wǎng)　　3.1　位置/遷移Petri網(wǎng)　3.2　高級(jí)Petri網(wǎng)　習(xí)題第4章　進(jìn)程代數(shù)　　4.1　通信順序進(jìn)程　　　4.2　通信系統(tǒng)演算　習(xí)題第5章　一階邏輯　　5.1　命題邏輯　5.2　謂詞邏輯　　5.3　程序正確性證明　習(xí)題第6章　時(shí)態(tài)邏輯　　6.1　模態(tài)邏輯　　6.2　線性時(shí)態(tài)邏輯　　6.3　計(jì)算樹邏輯　　6.4　模型檢驗(yàn)　習(xí)題第7章　Z　7.1　概述　　7.2　表示抽象　　7.3　操作抽象　　7.4　Z規(guī)格的例　習(xí)題第8章　VDM　8.1　概述　　8.2　表示抽象　　8.3　操作抽象　　8.4　VDM規(guī)格的例　習(xí)題第9章　Larch參考文獻(xiàn)

章節(jié)摘錄

第1章軟件及其開發(fā)概述軟件或者程序是計(jì)算機(jī)及其應(yīng)用系統(tǒng)的一個(gè)重要組成部分。伴隨著計(jì)算機(jī)的誕生和發(fā)展，軟件及其開發(fā)經(jīng)歷了半個(gè)多世紀(jì)的歷程。本章簡(jiǎn)要回顧了軟件及其開發(fā)的歷史；闡述了軟件發(fā)展過(guò)程中的軟件危機(jī)、軟件工程、軟件開發(fā)的形式化方法等。1.1軟件開發(fā)的歷史第一臺(tái)通用電子數(shù)字計(jì)算機(jī)ENIAC于1946年2月15日誕生，與之相伴，出現(xiàn)了計(jì)算機(jī)軟件（早期稱為程序）。軟件是計(jì)算機(jī)系統(tǒng)中與硬件相互依存的另一部分，它與硬件合為一體完成系統(tǒng)功能。在計(jì)算機(jī)發(fā)展的早期階段（1946年到20世紀(jì)60年代中期），計(jì)算機(jī)系統(tǒng)還是以硬件為主，軟件費(fèi)用只占總費(fèi)用的20％左右；到了計(jì)算機(jī)發(fā)展的第二個(gè)階段（20世紀(jì)60年代中期到20世紀(jì)80年代初期），在硬件費(fèi)用成倍下降的同時(shí)，軟件費(fèi)用卻迅速上升，達(dá)到了總費(fèi)用的60％以上；之后軟件費(fèi)用一直持續(xù)上升，其在計(jì)算機(jī)系統(tǒng)總費(fèi)用中的比例一直上升到今天的80％以上。所謂軟件開發(fā)，實(shí)際上就是把現(xiàn)實(shí)世界的需求反映成軟件的模型化并予以實(shí)現(xiàn)的過(guò)程。在計(jì)算機(jī)發(fā)展的不同時(shí)期，人們對(duì)軟件的認(rèn)識(shí)不同，相應(yīng)地，所進(jìn)行的軟件開發(fā)也具有不同的特點(diǎn)。軟件及其開發(fā)大體經(jīng)歷了如下三個(gè)階段：（1）程序設(shè)計(jì)階段（1946年-1956年）自1946年2月15日第一臺(tái)通用電子數(shù)字計(jì)算機(jī)ENIAC宣告研制成功，到1956年高級(jí)語(yǔ)言的誕生，是軟件發(fā)展的第一個(gè)階段。

編輯推薦

《軟件開發(fā)的形式化方法》是由高等教育出版社出版。

圖書封面

圖書標(biāo)簽Tags

無(wú)

評(píng)論、評(píng)分、閱讀與下載

---

    軟件開發(fā)的形式化方法 PDF格式下載

---