信息服務的需求獲取與建模研究一般性科技報告

段振華　田聰　王小兵　張南

摘 要：研究目前在以下方面取得了研究進展。首先，在信息服務的需求獲取及協同優化方面：（1）完善了面向特征領域分析的需求獲取方法；（2）完善了基于目標場景的用例驅動需求獲取方法；（3）研究了協同分析與優化方法，同時開發了相應的支撐工具。其次，在信息服務的建模與模型演化方面：（1）研究了基于Petri網的建模和模型演化理論與方法，同時開發了相應的支撐工具；（2）研究了基于進程代數的建模與模型演化理論與方法。最后，在信息服務模型的形式化驗證與確認方面：（1）研究了基于模型的測試理論與方法，并開發了相應的模型測試工具；（2）研究了基于PPTL的符號和限界模型檢測理論與方法，并開發了相應的模型檢測器；（3）完善了基于MSVL的仿真理論與方法，并開發了相應的支撐工具MSV；（4）研究了基于抽象精化的模型檢測理論與方法，并開發了相應的支撐工具。

關鍵詞：需求獲取 信息服務 模型演化 形式驗證 模型檢測 定理證明

Abstract：Recently， the project team made progress in the following aspects. First， in requirement elicitation and collaborative optimization of information services， we （1） improved feature-oriented domain analysis requirement elicitation approach；（2） investigated use case driven requirement elicitation approach based on target scenario；（3） studied collaborative analysis and optimization method and developed the supporting tool. Second， we studied modeling and model evolution methods of information services including：（1） modeling and model evolution theory and approach base on Petri nets；（2） process algebraic based modeling and model evolution theory and method. Supporting tools are also developed. Finally， we investigated the following formal verification and confirmation approaches of information service models. （1） We studied model based testing theory and approach， and developed model based testing tool；（2） we presented symbolic and bounded model checking approaches of PPTL， and developed the corresponding model checkers；（3） we improved simulation theory and approach based on MSVL， and developed toolkit MSV；（4） we studied CEGAR based abstract model checking approach， and developed the supporting tool.

Key Words：Requirement Elicitation；Information Services；Model Evolution；Formal Verification；Model Checking；Theory Proving

閱讀全文鏈接（需實名注冊）：http：//www.nstrs.cn/xiangxiBG.aspx？id=49528&flag=1