課程簡(jiǎn)介
Course Introduction
形式化方法的意義在于它能幫助發(fā)現(xiàn)其它方法不容易發(fā)現(xiàn)的系統(tǒng)描述的不一致、不明確或不完整,，有助于增加軟件開(kāi)發(fā)人員對(duì)系統(tǒng)的理解,，因此形式化方法是提高軟件系統(tǒng)，特別是Safety-Critical系統(tǒng)的安全性與可靠性的重要手段,。最早的形式化方法是邏輯與邏輯推理,，它的目標(biāo)是使推理機(jī)械化。從廣義上講,，這一目標(biāo)受到許多挫折,，比如說(shuō)邏輯系統(tǒng)的不完備性(incompleteness)、邏輯系統(tǒng)的不可判定性(undecidability),、自動(dòng)推理的難處理性(intractability),。但是在一些實(shí)際應(yīng)用上，邏輯方法和自動(dòng)推理還是起著非常大的作用,。
教學(xué)大綱
Teaching Syllabus
從廣義上講,，形式化方法是借助數(shù)學(xué)的方法來(lái)解決軟件工程領(lǐng)域的問(wèn)題，主要包括建立精確的數(shù)學(xué)模型以及對(duì)模型的分析活動(dòng),。狹義的講,，形式化方法是運(yùn)用形式化語(yǔ)言，進(jìn)行形式化的規(guī)格描述,、模型推理和驗(yàn)證的方法,。就形式化建模而言,，形式化表示必須包含一組定義其語(yǔ)法語(yǔ)義的形式化規(guī)則。這些規(guī)則可用于分析給定的表達(dá)式是否符合語(yǔ)法規(guī)定,，或證明該表達(dá)式具有某種性質(zhì),。
教學(xué)隊(duì)伍Teaching Members
友情鏈接Links
相關(guān)課程Correlative
Courses
