软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2013年
4期
715-729
,共15页
形式规格说明%相对正确性%确认%扩展的逻辑系统%辅助证明算法
形式規格說明%相對正確性%確認%擴展的邏輯繫統%輔助證明算法
형식규격설명%상대정학성%학인%확전적라집계통%보조증명산법
formal specification%relative correctness%validation%extended logic system%aided certified algorithm
在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.
在形式規格說明的穫取任務中,一箇重要問題是驗證穫取得到的形式規格說明的正確性.即給定一箇問題需求P,往往可以穫取多種不同形式的規格說明,如何驗證這些不同形式的規格說明均正確?問題需求的非(半)形式化與形式規格說明的形式化兩者之間差異的本性,使得該問題成為軟件需求工程中一箇具有挑戰性的問題.提齣一種基于形式化推導的方法來驗證同一問題不同形式規格說明的相對正確性,通過證明不同形式規格說明與問題需求某箇最為直截明瞭的形式規格說明Si等價來實現,而Si使用PAR方法和PAR平檯轉換為可執行程序,通過測試已經得到確認.為瞭支持該方法,進一步提齣瞭擴展的邏輯繫統和輔助證明算法.使用Radl語言作為形式規格說明語言,通過排序搜索、組閤優化領域的兩箇典型實例對該方法進行瞭詳細的闡述.實際使用效果錶明,該方法不僅能夠有效地驗證Radl形式規格說明的正確性,還具備良好的可擴充性.該方法在規格說明的正確性驗證、算法優化、程序等價性證明等研究領域具有潛在的理論意義與應用價值.
재형식규격설명적획취임무중,일개중요문제시험증획취득도적형식규격설명적정학성.즉급정일개문제수구P,왕왕가이획취다충불동형식적규격설명,여하험증저사불동형식적규격설명균정학?문제수구적비(반)형식화여형식규격설명적형식화량자지간차이적본성,사득해문제성위연건수구공정중일개구유도전성적문제.제출일충기우형식화추도적방법래험증동일문제불동형식규격설명적상대정학성,통과증명불동형식규격설명여문제수구모개최위직절명료적형식규격설명Si등개래실현,이Si사용PAR방법화PAR평태전환위가집행정서,통과측시이경득도학인.위료지지해방법,진일보제출료확전적라집계통화보조증명산법.사용Radl어언작위형식규격설명어언,통과배서수색、조합우화영역적량개전형실례대해방법진행료상세적천술.실제사용효과표명,해방법불부능구유효지험증Radl형식규격설명적정학성,환구비량호적가확충성.해방법재규격설명적정학성험증、산법우화、정서등개성증명등연구영역구유잠재적이론의의여응용개치.
