局部行为模型的合并的分析.pdf

局部行为模型的合并研究 摘要 软件工程中的需求分析是指通过对要解决的问题的分析与理解，为问题涉及 的信息、功能及系统行为建立模型，将用户需求精确化、完全化，最终形成需求 规约说明。而用于需求分析的形式化方法是以严格的数学理论为基础，用数学的 方法来帮助需求分析人员解决目标系统系统“做什么”的问题。 模态迁移系统是一种基于状态机的形式化建模方法，普遍应用于对系统行为 的形式规约。该方法通常假定在某种层次上，已经完整描述目标系统的行为。尽 管这一假设对已经完全探知其属性的命题来说是有效的，但在系统行为建模的初 期是不能满足需求的，系统需求的捕获过程中需求信息是逐步完善的。为获取目 标系统更正确完整的需求规约，本文通过扩展模态迁移系统，定义了局部模态迁 移系统来更精确的描述目标系统的局部行为。局部模态迁移系统对用户需求描述 中的必然行为、不确定行为和禁止行为，都给出了相应的形式规约说明。在局部 模态迁移系统中未描述的行为被认为超出了特定用户关注的范围，是与之无关的 未定义行为。 为消除局部行为模型中存在的不确定行为，获取目标系统的全局行为模型， 文中提出了一种基于事件和状态的局部行为模型合并方法。该方法首先定义了模 型之间的精化关系，利用精化关系比较谁是目标系统更“确定的”的模型，这也 就为确定什么样的模型是我们期望的合并模型提供了依据。由于我们通常希望合 并模型不增加额外的需求信息，因此其合并过程就是构建初始模型的最小共同精 化(或极小共同精化)的过程。通过文中定义的+u操作符和+1操作符可以分别 确定合并模型的上界与最大下界。建模者可以选择性的对最大下界进一步精化获 得预期的极小共同精化。通过对目标系统所有局部行为模型的合并，以及在合并 过程中不断的与相关用户交互，可以精化模型中存在的不确定行为，逐步捕获目 标系统的所有必然行为。最终的全局行为模型应该只包含有必然迁移和禁止迁 移，这样也就得到了我们所期望的初始模型的实现：局部标号迁移系统模型。 关键字：场景；模态迁移系统；禁止行为；精化；合并 Ⅱ ResearchonPaItialBehaVioralModels Me玛i119 ABSTRACT f10rso行ware tlle Requirementanalysis engiIleeringis也eproce§st0，e吮blish modelsof aIld behaviorS iIlfonIlatio玛劬ctionssystem syne唱izing byunderStanding and met0-besolVed alld伍ere】evant thellmal(e a11出yzillg problems enV的nment，and needs aSt0 也ecuStomer so fo彻me precise趾1d complete eVentually requiremem meFoml甜Me廿lodsfor are baSeon spec谲catio珥砒lile appliedrequirememaIlalysis 也e t0s01Vet11e of‘‘whattodo”ofthe rig