在信息化时代,软件产品已经成为我们工作学习中不可缺少的重要组成部分。软件作为信息交流传播和自动化生产控制的载体,逐渐成为人类社会发展的重要支柱。软件产品涉猎的领域也越来越广泛,从我们日常的聊天交流娱乐购物到国家军事航空航天领域,都离不开软件产品。一方面我们在享受着软件产品为我们带来各种便利服务,另一方面我们也可能遭受软件产品缺陷或者失效给我们带来生活财产损失甚至人身安全事故等威胁。同时,一些大型密集型软件项目的延期交付或者失败,给企业、国家、组织带来巨大的人力物力财力损失等等问题。这些问题产生的原因有很多,例如硬件的失效或故障、人的不当操作等,但软件需求可以说是出现这些问题的最重要的一个原因。软件需求不仅仅作为整个软件开发早期阶段的起点和基础,也贯穿了整个软件开发生命周期,也是软件开发后期测试阶段的重要参考依据。因此,对软件需求工程的研究,已经成为软件开发和维护不可或缺的部分,具有重要的理论意义和现实意义。在需求工程中,面向问题的软件需求分析方法即问题框架(ProblemFrames)方法,为我们提供了一种解决软件开发问题的一种更广阔的视角和参考模式。问题框架方法强调对存在于真实世界中问题的获取和正确的理解,而不是过早地去关注问题的解决方案。面向问题的软件开发思想也正是这样得来的,即在软件需求分析阶段,我们要关注于问题,而不是问题的解决方案。问题图模型是问题框架中一种基本的建模模型,由机器领域、存在于现实世界的问题域,以及需求组成。软件规格(Softwarespecifications)是用于描述计算机周围应用领域交界处计算机的行为规约。需求(Requirements)是客户想要得到的机器行为作用于现实世界领域的系统环境行为的描述。在问题框架方法中,用户需求通过机器与问题域之间的交互来满足。本文主要围绕问题框架方法中形式化语义解集合的求解问题展开,即验证我们通过问题框架方法建立的问题图需求模型是否存在满足需求的解,然后找出一个可行的解,并验证该解是否满足需求。本文基于UML对问题框架建模方法进行扩展,并提出了对扩展建模方法形式化验证的六步验证方法。在问题图模型的静态结构方面,本文依据问题框架需求建模方法中问题图的自身特性,将其映射为UML类图。然后,本文利用基于对象约束语言OCL(Object Constraint Language)制定的规则校验插件——UML4PF(该插件运行在Eclipse平台上),来检测我们由问题图转化而来的UML类图模型结构的完整性和正确性。在建立了一个完整的、正确的问题图模型之后,本文设计了一个创建问题图因果关系链的算法,然后依据该算法创建出问题图中的一条因果关系链。若能创建出这样一条因果关系链,就说明问题存在一个可能的解。在问题图模型的动态行为方面,为了验证问题图需求模型的解(软件规约S)是否满足需求,本文进一步将问题图映射为UML状态图,用来描述系统软件规约的动态行为特性,然后通过建立状态图与通信顺序进程CSP(CommunicatingSequential Process)之间一对一的映射关系,最终用CSP形式化描述语言来表述原问题图模型中的规约S和需求R。最后,本文借助模型检验工具FDR(Failure/Divergence Refinement)和 PAT(Process Analysis Toolkit)来验证用 CSP 形式化语言描述的软件规约模型是否精化和满足了需求模型。本文通过从问题图模型静态结构和动态行为两方面的验证工作,使我们能够改正软件需求分析模型的错误,从而得到一个高质量的需求模型。这样可以避免错误向软件开发后续阶段传播,同时节省不必要返工代价和成本。