本文關(guān)鍵詞：軟件形式化方法與應(yīng)用專題前言

  更多相關(guān)文章： 形式化方法 高階邏輯 應(yīng)用專題 定理證明器 程序理論 數(shù)學(xué)方法 研究成果 代數(shù)的 計(jì)算機(jī)科學(xué) 保障系統(tǒng)

【摘要】：正形式化方法起步于程序理論和語(yǔ)義的研究,歷經(jīng)50余年的發(fā)展,成為了計(jì)算機(jī)科學(xué)的重要領(lǐng)域.它使用嚴(yán)格的數(shù)學(xué)方法,研究并發(fā)展軟件和硬件系統(tǒng)的建模、設(shè)計(jì)、開發(fā)、驗(yàn)證與演化等技術(shù),為保障系統(tǒng)的正確性、可靠性和安全性提供了重要途徑.本專題收錄的13篇論文反映了近年來(lái)我國(guó)學(xué)者在軟件形式化方法與應(yīng)用領(lǐng)域的部分研究成果.《幾何代數(shù)的高階邏輯形式化》提出了一種基于高階邏輯定理證明器HOL-Light的幾何代數(shù)建模和驗(yàn)證方
【作者單位】： 計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室(中國(guó)科學(xué)院軟件研究所);國(guó)防科學(xué)技術(shù)大學(xué)計(jì)算機(jī)學(xué)院;計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室(南京大學(xué));
【關(guān)鍵詞】： 形式化方法;高階邏輯;應(yīng)用專題;定理證明器;程序理論;數(shù)學(xué)方法;研究成果;代數(shù)的;計(jì)算機(jī)科學(xué);保障系統(tǒng);
【分類號(hào)】：TP311.5
【正文快照】： 形式化方法起步于程序理論和語(yǔ)義的研究,歷經(jīng)50余年的發(fā)展,成為了計(jì)算機(jī)科學(xué)的重要領(lǐng)域.它使用嚴(yán)格的數(shù)學(xué)方法,研究并發(fā)展軟件和硬件系統(tǒng)的建模、設(shè)計(jì)、開發(fā)、驗(yàn)證與演化等技術(shù),為保障系統(tǒng)的正確性、可靠性和安全性提供了重要途徑.本專題收錄的13篇論文反映了近年來(lái)我國(guó)學(xué)者在

【相似文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 古天龍;董榮勝;;歐洲高校計(jì)算機(jī)專業(yè)的形式化方法課程教學(xué)[J];計(jì)算機(jī)教育;2008年10期

2 柴振榮;《編程中的形式化方法及其應(yīng)用》會(huì)議[J];管理科學(xué)文摘;1995年06期

3 鄭士貴;智能服務(wù)網(wǎng)絡(luò)形式化方法的模擬和實(shí)質(zhì)[J];管理科學(xué)文摘;1997年01期

4 姜利;孫永強(qiáng);;形式化方法的發(fā)展及展望[J];計(jì)算機(jī)科學(xué);1998年02期

5 張廣泉;關(guān)于軟件形式化方法[J];重慶師范學(xué)院學(xué)報(bào)(自然科學(xué)版);2002年02期

6 崔霞,苗長(zhǎng)芬;硬件設(shè)計(jì)中的形式化方法[J];新鄉(xiāng)教育學(xué)院學(xué)報(bào);2005年02期

7 鹿蕾;;形式化方法B的證明技術(shù)[J];現(xiàn)代電子技術(shù);2005年23期

8 陳澎;設(shè)計(jì)模式形式化方法分析和初步比較[J];計(jì)算機(jī)工程;2005年02期

9 李建華;李紅革;;形式化及其歷史發(fā)展[J];自然辯證法研究;2008年08期

10 曹源;唐濤;徐田華;穆建成;;形式化方法在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J];交通運(yùn)輸工程學(xué)報(bào);2010年01期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前7條

1 李文健;;形式化的涵義及其認(rèn)識(shí)論本質(zhì)[A];1993年邏輯研究專輯[C];1993年

2 吳允曾;;關(guān)于形式化的幾個(gè)問(wèn)題[A];金岳霖學(xué)術(shù)思想研究——金岳霖學(xué)術(shù)思想研討會(huì)論文集[C];1985年

3 鄭宇軍;石海鶴;薛錦云;;Spec#語(yǔ)言中的形式化特性[A];2005年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2005年

4 雷敏;雷友殉;;一種UML到SDL轉(zhuǎn)換方法的研究與應(yīng)用[A];2006通信理論與技術(shù)新進(jìn)展——第十一屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集[C];2006年

5 苗潔君;王克;;密碼模塊的形式化設(shè)計(jì)和驗(yàn)證研究[A];第二十一次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2006年

6 繆道期;;評(píng)審計(jì)算機(jī)安全等級(jí)[A];第二次計(jì)算機(jī)安全技術(shù)交流會(huì)論文集[C];1987年

7 趙曉峰;;城市軌道交通自主化信號(hào)系統(tǒng)全面創(chuàng)新實(shí)踐[A];中國(guó)系統(tǒng)工程學(xué)會(huì)第十八屆學(xué)術(shù)年會(huì)論文集——A12系統(tǒng)科學(xué)與系統(tǒng)工程理論在各個(gè)領(lǐng)域中的應(yīng)用研究[C];2014年

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前1條

1 殷杰 安軍 山西大學(xué)科學(xué)技術(shù)哲學(xué)研究中心;21世紀(jì)科學(xué)哲學(xué)的關(guān)鍵詞:語(yǔ)境、科學(xué)理性與形式化[N];中國(guó)社會(huì)科學(xué)報(bào);2011年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前8條

1 劉艷;互聯(lián)網(wǎng)內(nèi)容分級(jí)服務(wù)技術(shù)標(biāo)準(zhǔn)體系的形式化設(shè)計(jì)與驗(yàn)證[D];華中師范大學(xué);2015年

2 錢振江;安全操作系統(tǒng)形式化設(shè)計(jì)與驗(yàn)證方法研究[D];南京大學(xué);2013年

3 劉強(qiáng);設(shè)計(jì)模式的形式化研究及其EMF實(shí)現(xiàn)[D];華東師范大學(xué);2011年

4 張鵬;形式化方法在云計(jì)算中的應(yīng)用研究[D];吉林大學(xué);2014年

5 劉洋;網(wǎng)絡(luò)式軟件需求驗(yàn)證的形式化方法研究[D];電子科技大學(xué);2013年

6 王邁;語(yǔ)言形式化原理[D];上海外國(guó)語(yǔ)大學(xué);2011年

7 胡靜;基于Pi-演算的Web服務(wù)形式化描述模型[D];天津大學(xué);2013年

8 周寧;代數(shù)化符號(hào)模擬驗(yàn)證的應(yīng)用研究[D];北京交通大學(xué);2015年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 王春曉;MDF連續(xù)平壓質(zhì)量控制形式化建模及優(yōu)化研究[D];東北林業(yè)大學(xué);2015年

2 王亞麗;面向機(jī)器人規(guī)劃的形式化研究[D];北京化工大學(xué);2015年

3 Hamza I.Bangura;基于Z規(guī)格的軟件缺陷形式化方法[D];天津大學(xué);2010年

4 鐘琪;軟件分析模式的形式化研究[D];西南師范大學(xué);2004年

5 王祥兵;形式化方法的理論及其影響[D];貴州大學(xué);2009年

6 郭忠偉;神經(jīng)內(nèi)分泌復(fù)雜系統(tǒng)的形式化研究[D];揚(yáng)州大學(xué);2009年

7 王曉帆;基于模糊數(shù)學(xué)的形式化開發(fā)方法研究[D];西安理工大學(xué);2003年

8 閔洪軍;軟件工程中形式化方法研究[D];浙江大學(xué);2006年

9 張楊;UML模型形式化轉(zhuǎn)換及驗(yàn)證的研究[D];太原理工大學(xué);2013年

10 匡春臨;并發(fā)系統(tǒng)的形式化技術(shù)研究[D];華僑大學(xué);2008年

，

本文編號(hào)：786854