摘要:形式化软件规约与设计间的语义断层问题,是制约形式化方法从规约向设计平滑迁移的重要问题,目标操作化是解决这一问题的重要方法.KAOS是主要的支持目标操作化的规约语言之一,但它给出的主体、目标和操作缺乏统一的语义描述,对目标操作化的支持仅限于模型实例化级别上规约(触发条件)与设计(状态变化)间的语义连接,且只能针对具体实例实施目标操作化,本文引入主体模型,将主体的结构(状态)上的操作与BDI模型中的事件统一起来,并扩充BDI模型的语法、语义,建立了一种新的目标操作化规约模型(GOP模型),实现了主体、目标、操作在GOP模型中的统一描述;通过引入对偶主体和完全世界的概念,把操作描述为主体与对偶主体的状态关系上的一个算子,从而在元模型级别较好地解决了规约与设计间的语义断层问题;本文基于多类型代数建立主体属性域结构模型,使得GOP模型中描述操作的算子可与下层属性域结构模型,使得GOP模型中描述操作的算子可与下层属性域的结构性质联系起来,籍此在一个域原子操作的基础上,根据域结构构造出属性域上的任意原子目标操作,因而可以用一个域原子操作模型解决一个属性域上全部原子目标操作化的问题,具有更广泛的理论指导意义和实践应用价值.