段振華　田聰　王小兵　張南

摘 要：研究目前在以下方面取得了研究進展。首先，在信息服務(wù)的需求獲取及協(xié)同優(yōu)化方面：（1）完善了面向特征領(lǐng)域分析的需求獲取方法；（2）完善了基于目標(biāo)場景的用例驅(qū)動需求獲取方法；（3）研究了協(xié)同分析與優(yōu)化方法，同時開發(fā)了相應(yīng)的支撐工具。其次，在信息服務(wù)的建模與模型演化方面：（1）研究了基于Petri網(wǎng)的建模和模型演化理論與方法，同時開發(fā)了相應(yīng)的支撐工具；（2）研究了基于進程代數(shù)的建模與模型演化理論與方法。最后，在信息服務(wù)模型的形式化驗證與確認(rèn)方面：（1）研究了基于模型的測試?yán)碚撆c方法，并開發(fā)了相應(yīng)的模型測試工具；（2）研究了基于PPTL的符號和限界模型檢測理論與方法，并開發(fā)了相應(yīng)的模型檢測器；（3）完善了基于MSVL的仿真理論與方法，并開發(fā)了相應(yīng)的支撐工具MSV；（4）研究了基于抽象精化的模型檢測理論與方法，并開發(fā)了相應(yīng)的支撐工具。

關(guān)鍵詞：需求獲取 信息服務(wù) 模型演化 形式驗證 模型檢測 定理證明

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