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