信息服务的需求获取与建模研究一般性科技报告

段振华　田聪　王小兵　张南

摘 要：研究目前在以下方面取得了研究进展。首先，在信息服务的需求获取及协同优化方面：（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