计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2012年
16期
52-56
,共5页
形式验证%Z规格说明%数据库交互%逆向工程%定理证明
形式驗證%Z規格說明%數據庫交互%逆嚮工程%定理證明
형식험증%Z규격설명%수거고교호%역향공정%정리증명
采用定理证明和逆向工程的方法,对Web应用中的数据库交互行为进行验证.使用Z规格说明描述需求模型,根据数据库交互的源代码和转换规则得到实现模型.从实现模型中获取Web应用的相关性质,通过Z/EVES定理证明器验证这些性质是否在需求模型的Z规格说明中得到满足.在此基础上,设计该方法的验证框架,并开发相应的原型系统.通过图书馆数据库管理系统实例证明该方法的有效性.
採用定理證明和逆嚮工程的方法,對Web應用中的數據庫交互行為進行驗證.使用Z規格說明描述需求模型,根據數據庫交互的源代碼和轉換規則得到實現模型.從實現模型中穫取Web應用的相關性質,通過Z/EVES定理證明器驗證這些性質是否在需求模型的Z規格說明中得到滿足.在此基礎上,設計該方法的驗證框架,併開髮相應的原型繫統.通過圖書館數據庫管理繫統實例證明該方法的有效性.
채용정리증명화역향공정적방법,대Web응용중적수거고교호행위진행험증.사용Z규격설명묘술수구모형,근거수거고교호적원대마화전환규칙득도실현모형.종실현모형중획취Web응용적상관성질,통과Z/EVES정리증명기험증저사성질시부재수구모형적Z규격설명중득도만족.재차기출상,설계해방법적험증광가,병개발상응적원형계통.통과도서관수거고관리계통실예증명해방법적유효성.
