課程簡介
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ù)學的方法來解決軟件工程領域的問題，主要包括建立精確的數(shù)學模型以及對模型的分析活動,。狹義的講,，形式化方法是運用形式化語言，進行形式化的規(guī)格描述,、模型推理和驗證的方法,。就形式化建模而言，形式化表示必須包含一組定義其語法語義的形式化規(guī)則,。這些規(guī)則可用于分析給定的表達式是否符合語法規(guī)定,，或證明該表達式具有某種性質。
教學隊伍Teaching Members
友情鏈接Links
相關課程Correlative
Courses
