（管理科学与工程专业论文）基于rcos的sysml形式化研究.pdf

内蒙古大学硕士学位论文 基于r c o s 的s y s m l 形式化研究 摘要 s y s m l 系统建模语言s y s t e m sm o d e l i n gl a n g u a g e 是一种通用的图形化 的建模语言 是u m l 2 0 的一个外廓 目前 s y s m l 已经成为系统工程建模领 域的标准 但是s y s m l 的语义仍是半形式化的 这种半形式化的语义降低了 s y s m l 模型的精确性 给模型的自动分析和验证带来了困难 一种解决方法就 是使用某种形式化方法来精确的描述s y s m l 元模型的语义信息 目前 形式化地支持基于u l v i l 开发的大多数工作已经存在 但据我们所知 几乎没有关于s y s m l 的形式化语义研究及其协调性精化方面的工作 因此这 个工作在计算机科学和软件工程领域都有理论意义和实用价值 本文主要研究如何使用面向对象的形式语言r c o s 描述s y s m l 元模型并在 确保其一致性的基础上提出了一个论断性的集成的s y s m l 语义模型 为了使 形式化工作尽可能系统化 我们首先给出s y s m l 元模型 主要为模块定义图 和顺序图 的形式化语义 在此基础上将s y s m l 元模型转化到r c o s 的规范形 式 本文给出了s y s m l 部分元模型的精确描述 解决了协调性问题 即各种观 点下的模型在语法和语义上的相容性问题 为模型的转换和精化奠定了坚实的 基础 关键词 s y s m l 形式化 语义 r c o s 基于r c o s 的s y s m l 形式化研究 r e s e a r c ho nf o r m a l i z 虹i o no fs y s t e m s m o d e l i n gl a n g u a g eb a s e do nr c o s a b s t r a c t t h es y s t e m sm o d e l i n gl a n g u a g e s y s m l i sag e n e r a l p u r p o s eg r a p h i c a l m o d e l i n gl a n g u a g e w h i c hi s as u b s e to fu m l2 0 n o w s y s m lb e c o m e st h e s t a n d a r di ns y s t e m se n g i n e e r i n gd o m a i n b u tt h es e m a n t i c so fs y s m li sa l s o i n f o r m a l t h e s ei n f o r m a ls e m a n t i c so fl a n g u a g em a k ei td i f f i c u l tf o rs y s m l m o d e l sr e a s o n i n g o n ew a yi st ou s es o m ew e l l d e f i n e do b j e c t o r i e n t e df o r m a l s p e c i f i c a t i o nt od e f i n es y s m lm e t a m o d e l se x a c t l y t h e m a jo r i t y o ft h ew o r k so nf o r m a l i z a t i o n s u p p o r t t ou m l b a s e d d e v e l o p m e n th a s a l s oe x i s t e d b u t t oo u rk n o w l e d g e t h e r ei sl i t t l ew o r ko n c o n s i s t e n tr e f i n e m e n to fs y s m lm o d e l s t h e r e f o r et h ew o r ki sv e r yt h e o r e t i c a l l y m e a n i n g f u la n du s e f u li nt h ec o m p u t e rs c i e n c ea n ds o f t w a r ee n g i n e e r i n ga r e a s i nt h i sp a p e rw et r yt ou s er c o st od e f i n es y s m lm e t a m o d e l sa n dp r e s e n ta p r e d i c a t i v es e m a n t i cm o d e lf o ri n t e g r a t i n gm o d e l sf r o ms y s m lb l o c kd e f i n i t i o n d i a g r a m sa n ds e q u e n c ed i a g r a m sb a s e do nc o n s i s t e n c yb e t w e e nt h e m i no r d e rt o m a k et h i sw o r km o r ef o r m a l w ef i r s t g i v et h es e m a n t i cm o d e l so fs y s m l m e t a m o d e l s w h i c hm a i n l yi n c l u d et h eb l o c kd e f i n i t i o nd i a g r a m sa n ds e q u e n c e d i a g r a m s t h e n a n yv e r i f i c a t i o no fs y s m lm o d e l sc a nt a k ep l a c eo nt h e i r c o r r e s p o n d i n gr c o ss p e c i f i c a t i o n su s i n gr e a s o n i n gt e c h n i q u e sp r o v i d e db yr c o s w i t ht h i sa p p r o a c h w ep r o v i d en o to n l yap r e c i s es e m a n t i cb a s i sf o rs y s m l m e t a m o d e l sb u ta l s os o l v et h ep r o b l e mo fc o n s i s t e n c y i e t h e c o m p a t i b i l i t y b e t w e e ns y n t a c t i cm o d e l sa n ds e m a n t i cm o d e l s i tp a v e st h ew a yf o rt h em o d e l t r a n s f o r m a t i o na n dm o d e lr e f i n e m e n t k e y w o r d s s y s m l f o r m a l i z a t i o n s e m a n t i c s r c o s i i 内蒙古大学硕士学位论文 图表目录 表3 1 s y s m l 元模型体系结构 1 4 图3 1 系统建模语言中的图形分类 1 6 图4 r 模块的具体语法 j1 9 图4 2 模块定义图的具体语法 2 0 图4 3 防滑刹车系统的模块定义图 2 0 图4 4 内部模块图的具体语法 2 0 图4 5 反锁控制器的内部模块图 2 1 图4 6 发动汽车的简单的黑盒顺序图 2 2 图4 7 发动汽车的简单的白盒顺序图 2 2 图4 8 自动柜员机系统的需求模型 4 1 图4 9 自动柜员机系统的模块定义图 4 1 图4 1 0 自动柜员机系统的顺序图 4 2 v 原创性声明 本入声明 所呈交的论文是本人在导师指导下进行的研究工作及取得的研究 成果 除了文中特别加以标注和致谢中所罗列的内容以外 论文中不包含其他人 已经发表或撰写过的研究成果 也不包含为获得内蒙吉大学及其他教育桃构的学 位或证书而使用过的材料 与我一同工作的同志对本研究所做的任何贡献均己在 论文中作了明确的说暖并表示了谢意 学位论文俸者签名 日期 弦螽戡指导教师签名 至盛翌 在学期间研究成果使用说明书 本学位论文 乍者完全了解内蒙吉大学有关保留和使用学位论文的飙定 帮 内蒙古大学研究生在校攻读学位期间论文工作的知识产权单位属内蒙古大学 学 校有权保留并向豳家有关部门或机构送交论文的复印侔和磁盘 允许学位论文被 查阅和借阅 学校可以公布学位论文的全部或部分内容 可以允许采用影印 缩 印或其它复制手段保存 汇编学位论文 乍者今后使用涉及在学期间主要研究内 容或研究成果 须征得内蒙古大学就读期间导师的同意 若用于发表论文 版权 单位必须署名为内蒙古大学方可投稿或公开发表 学位论文作者签名 瑟霆酪 指导教师签名 堡 量望 爵 内蒙古大学硕士学位论文 第一章绪论弟一早硒形 1 1 背景介绍 目前 系统工程师使用的建模语言 工具和技术种类很多 如行为图 i d e f 0 n 2 图 等 这些建模方法使用的符号和语义不同 彼此之间不能互操作和重用 系统工程正是由 于缺乏l 种强壮的 标准的 建模语言和建模工具 从而限制了系统工程师和其他学科之间 关于系统需求和设计的有效通信 影响了系统工程过程的质量和效率 为了满足系统工程 的实际需要 国际系统工程学会i n c o s e i n t e m a t i o n a lc o u n c i lo ns y s t e m se n g i n e e r i n g 和对 象管理组织o m g o b j e c tm a n a g e m e n tg r o u p 决定在对u m l 2 0 的子集进行复用和扩展的基 础上 提出一种新的系统建模语言 s y s m l s y s t e m sm o d e l i n gl a n g u a g e 作为系统工程 的标准建模语言 l 和u m l 用来统一软件工程中使用的建模语言一样 s y s m l 的目的是 统一系统工程中使用的建模语言 s y s m l 是u m l 在系统工程应用领域的延续和扩展 是近年提出的系统体系结构设计 的通用的图形化建模语言 用于由软硬件 数据和人综合而成的复杂系统的集成体系结构 说明 分析 设计及校验 s y s m l 已经成为o m g 的标准 其优势主要体现在可以使用单 一的集成的表示法来对系统工程的多个方面进行建模 但是 s y s m l 也存在不少问题 尤 其是它缺乏一个精确的形式化的语义 这使得对一个s y s m l 模型的理解可能会有歧义 另 一方面 在用s y s m l 描绘的系统工程不同方面的各种模型之间也容易存在不一致性 因此 难以实现逐步求精的开发过程 难以对模型进行分析以保证其正确性 随着建模语言的发展 建模语言的语义研究成为一个新兴的领域 在用u m l 建模 模 型转换以及提高模型的精确性和一致性方面 已有一些专家 学者做了大量的工作 g a r l a n 和k o m p a n e k 分析并评价了用u m l 建模软件体系结构的方式与性能 2 1 p a i g e 等人将程序 设计演算与部分u m l 模型结合起来 3 a m a l i o 等人将部分u m l 模型形式化1 4 k i m 和 c a r r i n g t o n 等人将部分u m l 视图映射到形式语言z 并用以描述面向对象的设计模式 5 6 1 他们的工作为在s y s m l 领域中进行相关研究奠定了基础 本文正是在前人研究的基础上 使用一种具有面向对象特征的形式化规格说明语言r c o s ar e f i n e m e n tc a l c u l u sf o ro b j e c t s y s t e m s 来对s y s m l 的部分元模型进行形式化描述 使得分析人员利用s y s m l 建立的系 统模型能够满足形式化规约的要求 基于r c o s 的s y s m l 形式化研究 1 2 研究目标 s y s m l 这套语言规范在面向对象分析 设计上是极其优秀的可视化建模语言 遗憾的 是s y s m l 的语义缺乏精确性 而将其形式化能够提供准确的描述和精确的规格说明 目前 在我国 对s y s m l 的研究还处于起步阶段 对其元模型及其形式化的研究还处 于空白 只是在局部领域内积累了一些经验 并没有形成成熟的形式化描述方法 所以 作者进行了 基于r c o s 的s y s m l 形式化研究 提出了将s y s m l 部分元模型形式化的方法 对s y s m l 元模型的形式化主要是对模块定义图 内部模块图和顺序图的形式化 并在此基 础上给出了s y s m l 的需求模型和设计模型的r c o s 规范形式 提出了一个论断性的s y s m l 的语义模型 本文的工作实际上建立了一种从图形加文字的非形式化模型到具有数学基础 的形式化模型的映射 在此基础上 可以进一步进行s y s m l 完整模型与协调性精化的研究 作者愿意在这方面做出有益的探索 为后续的研究工作做出一些贡献 1 3 研究意义 虽然我国在u m l 形式化方面的研究相对成熟 但据我们所知 几乎没有关于s y s m l 形式化研究方面的工作 所以非常需要有s y s m l 形式化基础方面的研究的出现 本课题对 s y s m l 的元模型进行了分析 结合u m l 形式化方面的相关工作 研究了部分s y s m l 元模 型的形式化描述 这在计算机科学和软件工程领域都有理论意义和实用价值 更重要的是 r c o s 的精化计算将被用来定义s y s m l 模型的协调性精化 这对支持可执行s y s m l 模型的 模型驱动的开发方法也有重要意义 希望通过本文所述的研究 能够在s y s m l 建模 模型转换以及提高模型的精确性和一 致性方面做出一定的贡献 进而推动我国在s y s m l 领域研究的发展 1 4 论文框架 本篇论文的结构如下 第一章绪论 本章主要阐述了论文选题的背景 研究目标和论文的基本框架 第二章形式化方法 重点介绍了r c o s 语言 r c o s 语言的规格说明及其语义 第三章系统建模语言s y s m l 介绍了s y s m l 的发展历史 主要内容及其优缺点 重 点介绍了s y s m l 的元模型 第四章三种s y s m l 图的形式化描述 依次给出了s y s m l 模块定义图 内部模块图 2 内蒙古大学硕士学位论文 和顺序图的形式化描述 并在此基础上提出了一种论断性的s y s m l 语义模型 第五章总结与展望 对本文工作进行总结 对未来工作进行展望 3 基于r c o s 的s y s m l 形式化研究 2 1 形式化方法介绍 第二章形式化方法 形式化方法是一种用于规范 设计和验证计算机系统的基于数学的方法 包括各种语 言 技术和工具等 形式化方法可分为形式规约方法和形式验证方法两大类 形式规约方 法包括了各种基于数学的表示法 语言以及对应的工具 形式验证方法包括各种模型检查 器 定理证明器以及证明和验证的方法等 形式化方法在软件开发中是很有意义的 首先是对软件需求的描述 形式化方法要求 描述的明确性 而描述的不一致性也就相对易于发现 其次是对软件设计的描述 软件设 计的描述和软件需求的描述同样重要 形式化方法的优点在于对软件需求的描述同样适用 于软件设计的描述 由于有了软件需求的形式化说明 我们可以检验软件的设计是否满足 软件的要求 对于编程来讲 甚至可以考虑代码的自动生成 对于一些简单的系统 形式 化的描述有可能直接转换成可执行程序 这就简化了软件开发过程 减少了产生错误的可 能性 极大的节约了软件的开发时间和资源成本 尽管形式化方法在软件工程及其相关的计算机领域己经取得了成功 但是与面向对象 技术和g u i 技术相比 其实用性还存在很大的差距 现有的技术应用更多的是局限于大学 科研机构和对安全性要求极高的工业部门 其主要的问题在于 7 由于形式化方法在本质上是一种严格的 灵活性较差的方法 缺乏必要的实施手段 和支持工具 所以难以在实际工业开发过程中被广泛的接受 现有的形式化方法在解决小规模的问题时较为有效 但却无法或很难应用于一些较 大规模的开发过程中 形式化方法和软件开发过程难以平滑的结合 针对上述情况 国际上有很多关于如何将形式化方法与主流的面向对象软件开发结合 起来的研究和尝试 由此产生了多种面向对象的形式化语言 目前 面向对象的形式化语言主要有o b j e c t z v d m 等 这些语言对诸如集合和关 系之类的数据结构建模来说是有效的 但是它们不能处理更复杂的机制 例如动态绑定和 多态性 m i k h a j l o v aa n ds e k e r i n s k i 用一个典型系统和谓词转换丰富了一种面向对象语割引 n a u m a n n 用谓词转换定义了一种带有子类型和多态的面向对象编程语言 9 1 然而 这些方 4 内蒙古大学硕士学位论文 法中都不允许类与类之间使用参考关系和依赖关系 l e i n o 用面向对象的特征扩展了一种已 经存在的数学语言 1 0 但是它不允许使用继承 并且不能处理类与可见性 本文选用r c o s 语言的一个优点是便于模型精化 在r c o s 1 1 模型中 一个程序被表示 为一个谓词 在u t p 中称作一个设计 d e s i g n 1 2 因此 程序间的精化关系可以用设计 间的蕴含式来表示 选用r c o s 的另一个优点是其在关系计算中给出了一个相当直接且容易 理解的规格说明 虽然r c o s 不能处理并发 但是u t p 能够描述计算的不同特征 包括并 发 通讯 时序和高阶的计算 1 3 1 4 这就为扩展r c o s 使之处理面向对象程序的不同方面 奠定了基础 2 2r c o s 语言 本文定义中用到的元符号及其语义如下 表示 被指派为 用于各种语法单位的定义之中 ii 表示互斥字母表中平行进程的执行 表示 被定义为 p t 表示由t 的所有子集构成的集合 即t 的幂集 sh 丁表示从s 到t 的一个二元关系 2 2 1r c o s 概述 r c o s 的全名是 ar e f i n e m e n tc a l c u l u sf o ro b j e c ts y s t e m s 即对象精化演算系统 它是一种基于r u p r a t i o n a lu n i t e dp r o c e s s 过程的开发面向对象软件的形式化方法 r c o s 可以定义面向对象的概念 如类 对象 继承 引用等 并且可以在此基础上利用求精规 则实现整个开发过程的求精化简 r c o s 是一种特征丰富的面向对象语言 其特征包括子类 引用类型 可见性 继承 动态绑定 多态和局部变量嵌套声明 r c o s 用于推理验证不同抽象层次上的面向对象的软 件 包括规格说明 设计和程序 r c o s 的语法包括面向对象系统 类声明 命令和表达式 其主要语法同j a v a 类似 其语义及转换规则能够为系统工程提供对象精化的转换规则 因 此 本文采用r c o s 来形式化系统建模语言的元模型 2 2 2r c o s 的语法规则的形式 一 面向对象系统 5 基于r c o s 的s y s m l 形式化研究 一个对象系统s 记作c d e c l s p c d e c l s 是有限类的声明 p 被称为主方法 记作 g l b c 由包括全局变量及其类型的有限集g l b 和命令c 组成 在主方法p 中 类的属性不能直接访 问 但g l b 中的变量可以直接访问 在类的声明域中 p 只能作为类的方法 r c o s 的语法包括类声明 类声明域 命令和表达式 我们将类声明处理为命令 并依 据前置条件和后置条件将其语义定义为一个设计 二 表达式 表达式出现在等号的右侧 形式如下 e jn u l lis e l f le af e 其中 n u l l 是所有类的子类 n u l l 是特殊类n u l l 的唯一的一个对象 s e l f 是当前环 境下的活动对象 e a 是e 的属性 f e 表示内嵌表达式 三 类声明 声明的形式为c d e c l s c d e c llc d e c l s c d e c l 是如下形式的类声明 c l a s s ne x t e n d sm p r i v a t e u iu l a l u mu m a f i l p r o t e c t e d v iv l h i v nv n b n p u b l i c w lw i c l w kw k c k m e t h o d m l t l l x l t i 2 y l t 1 3 z i c i m l t l l x l t t 2 y l t 1 3 z 1 c l 其中 n 和m 为类的名称 m 为n 的直接超类 p r i v a t e 描述类的私有属性 p r o t e c t e d 描述类的被保护属性 p u b l i c 描述类的公有属性 m e t h o d 为类的方法 t i l x i 为值参数 t i 2 y i 为结果参数 t i a z i 为值一结果参数 c i 为方法体 我们常用m p a r a s c 来表示方法 p a r a s 为m 中参数列表 c 为i t i 中命令的正文 方法b o d yc i 是一个命令 在后文中定义 四 命令 r c o s 支持面向对象的程序构建 下列命令含义分别如下 c s k i pc h a o sv a rtx e 终止 异常中断 局部变量声明 le n dx ic c lc c局部变量声明终止 顺序 条件 c f l cb c l e n e v u l 非确定性选择 循环 方法调用 l e e ic n e w x 指派 新建一个对象 6 内蒙古大学硕士学位论文 下面 我们将解释几个在面向对象程序中常用的命令 1 指派 指派l e e 是定义良好的当且仅当l e 和e 都是定义良好的 并且e 的类型是l e 中已经声 明的一种类型 例如 x e 表示将e 赋值给x ll e 玳表示将l e 的属性a 的值修改为e 2 方法调用 一个方法调用l e m v r v r 是定义良好的当且仅当l e 非空 m x y z 是l e 类型的方法声明 若方法是定义良好的 则其在执行中将实参v 和 r 赋值给形参x 然后在活动对象的类的 环境下执行方法的主体 在执行终止后 结果的值y 和值一结果参数z 被传回实参r 和v r m 中的z 为l e 引用的活动对象 3 新建对象 如果c 是一个被声明的类 则c n e w x 是定义良好的 2 2 3r c o s 的语义 一个程序表示为一个 设计 r c o s 的语义在 8 中陈述 在r c o s 中 一个程序或一个程序中的命令被定义为一个 设 计 用序偶乜p 来表示 a 表示程序的变量集 被称为设计的字母表 p 为设计的规约 是如下形式的谓词 p x 卜r x x o k 八p x o k 八r x x x 和x 表示a 中程序变量x 的初值和执行完程序后x 的终值 谓词p 为程序的前置条 件 谓词r 为程序的后置条件 用布尔变量o k 和o k 来描述程序的最终行为状态 当程 序正确启动时前者值为真 当程序终止时 后者值为真 因此 一个设计p x 卜r x x 表示 当程序正确启动 而且满足前置条件p x 那么该程序一定终止 终止时满足谓词r x x 细节参见 1 2 下面的精化定义是在 1l jq b 的 定义2 2 1 顺序组合 对于一个给定的字母表a 和两个规约p l p 2 顺序组合p l p 2 被定义为 p t x x p 2 x x 3m p l x m 八p 2 m x 2 1 定义2 2 2 对象系统间的精化 令s l 和s 2 为对象程序 如果s l 的行为比s 2 的行为更可预测更易控制 我们说属于全 局变量的集合g l b s 1 是s 2 的精化 记做s i2 s 2 定义为 s2 一v x o k o k s i s 2 2 2 7 基于r c o s 的s y s m l 形式化研究 其中 整是g l b 中的变量 也就是说s l 的外部行为是s 2 外部行为的一个子集 下面 我们将描述r c o s 的语义 我们以值 变量 状态 表达式 命令 声明和程序 这种编程语言的方式来定义一个基于状态的模型 二 值 对象 变量和状态 一个程序不仅对变量的初始类型进行操作 而且对对象的参数类型进行操作 为了描 2 述一个程序的行为 我们使用下面的局部变量作为自由变量 它们用于观察程序的行为 1 1 1 1 c n a m e c n a m e 的值是已声明的类的集合 在类声明中被修改 2 在c c n a m e 中有 a t t r c 类c 中声明或继承而来的属性的集合 形式为 t i 和d i 是属 性a i 的类型与初值 被分别归入集合d e c l t y p e c a i 和i n i t i a l c a i 中 用符号a t t r n a m e c 来表 示如下定义的集合 a t t r n a m e c 一pf j r d a t t r o p c 类c 中声明或继承而来的方法的集合 我们允许废除方法 但不允许重定义子类中的 方法 m l 卜专 銎 丑b y l 玉2 国 丑3 d i lki x 瓯 t k l 强 k 盈 乳 d k 上述符号表明方法m i 有值参数 结果参数和值一结果参数 分别用v a l c m i r e s c m i 和v a l r e s c m i 来表示 m i 的行为用命令d i 来表示 我们可以简单的定义o p c 的任意一个 元素为m l h 幽岛d i 有时 我们习惯用符号m o p c 来表示如下表达式 j 卫丛箜 d mh 哑 d o p c c 程序运行中存在的类c 的对象集合 在对象创建或销毁时被更新 令 u c 则 c e a 埘研p 变量 e c l c c n a m e 在创建一个新对象时被修改 本文不考虑已经存在的对象的销毁 3 s u p e r c l a s s s u p e r c l a s s 是局部函数 通过扩展自c l 的类c 的闭包将c n a m e 中的每一个类映射到其 直接超类上 在类声明中可以修改变量s u p e r c l a s s 符号5 表示一个超类的自反传递闭包 符号c 1 c 2 表示c l 是c 2 的超类 8 内蒙古大学硕士学位论文 4 g l b 程序中已知的全局变量以及全局变量类型的集合 形式为 x l t 1 x k t k x i 的类型t i 用d e c l t y p e x i 来表示 5 1 0 c v a r 程序当前状态下局部变量的集合 由于r c o s 语言允许嵌套声明 l o c v a r 的形式为变量 与类型序列的关联 记做 己 x n t i 是x i 的最新类型 用 d e c l t y p e x i 来表示 用v a r 来表示l o v a r ug l b 假定l o v a r m g l b 6 v i s i b l e a t t r 当前类的内部可视属性集的集合 属性包括当前类中已经声明的属性和其超类中的被 保护属性和所有的公有属性 三 评估表达式 对表达式的评估要求表达式是定义良好的 用d e 来表示一个良构的表达式e 对表达 式评估的结果如下所示 1 空的对象表达式是良构的 d n u l l t r u e t y p e n u l l n u l l v a l u e n u l l n u l l 2 如果一个变量在v a r 中被声明 我们说变量x 是良构的 其类型或者是初值 或者 是c n a m e 中的一个类 d x 一x v a r 人 d e c l t y p e x f v d e c l l y p e c c n a m e d e c l t y p e x fjh e a d x d e c l t y p e x d e c l t y p e x c n a m e h e a d x r ef x d e c l t y p e x 一 篇筠 燃如一i v a l u e x 1 一h e a d x 3 变量s e l f 是一个特殊的局部变量 它的类型通常为c n a m e 中的一个类 d s e l f 一s e l f l o cv a r ad e c l t y p e s e l f c n a m e h e a d s e l f r ef z d e c l t y p e s e l f t y p e s e l f 一t y p e h e a d s e l f v a l u e s e l f 一h e a d s e l f 4 如果h e a d x 是一个对象的标识 其类型为d e l c t y p e x a 为该对象的可视属性 则我 9 基于r c o s 的s y s m l 形式化研究 们说x a 是良构的 d x 口 d x d e c l t y p e x c n a m eat y p e x a v i s i b l e a t t r a h e a d x n u l l t y p e x a 一t y p e h e a d x 口 v a l u e x a l 一h e a d x a 5 如果1 e 是类的一个类型且该类非空 则我们说属性l e a 是良构的 a 为属性的名称 因此 一个属性的定义被归纳为 d 1 e 口 一d 1 e at y p e 1 e a v i s i b l e a t t r t y p e 1 e 口 一t y p e v a l u e 1 e a v a l u e 1 e a 一v a l u e 1 e a 6 f e 表示一个内嵌表达式 如果有e f 则它的良构条件和它的值如下所示 d e f 一d p ad ad e c l t y p e e r e a l a d e c l t y p e f r ea lav a l u e f 0 v a l u e e f v a l u e e v a l u e f 四 命令的语义 下文将给出面向对象程序设计中几个经常用到的命令的语义 1 指派的语义 给定一个指派 如果l e 和e 都是定义良好的 并且e 的当前类型与l e 中已经声明的类 型相匹配 则我们说l e e 是定义良好的 d 1 e e d r e ad at y p e e d e c l t y p e 1 e 有两种类型的指派 一种类型是将一个值赋给一个变量 这种情况只有在对象的类型 与变量的已声明类型相一致的情况下才可以使用 另一种类型是修改一个表达式对象的属 性值 x e 一 x d x p 卜 f t a i l x l e a e 一 x d e c l t y p e 1 e d 1 e a e 卜 f z d e c l t y p e 1 e t d e c l t y p e 1 e 1 l o v a l u e 1 e o ahv a l u e e j 2 新建对象的语义 1 0 内蒙古大学硕士学位论文 如果表达式列表e 的长度同c 的属性个数相同且表达式的类型与属性中相应的类型相 匹配 则我们说c n e w x 回的执行是定义良好的 其中 c e c n a m e 例 c n e w x e 一c c n a m e k 回 s i z e a t t r c kv i z y p e e f d e c l t y p e c i a 上述命令声明了一个变量x 新建了一个对象 将x 作为对象的名称 并将对象属性的 初值赋给x 具体内容如下所示 叶 c n e w x e 一 v a r x c d c 疗p x 幽 f3 r e f 正r ef x e z c u ia f a t t r c x g l b 人 x r e f v x o cv a r a x j 1 0 cv a r x l o cv a r u z i o cv a r x v x 萑v a r 人 一 八 i o c v a t l o c v a r u x 我们用c n e w x 来表示命令c n e w x i n i t i a a c a 用其属性的缺省值建立c 的一个实例 3 方法调用的语义 f v a rn s e l f l e 互工 1 疋y 疋 1 3 n t y p e 1 e kl 甲 埘 r w y z i i e n ds e l f x j z 其中 x y z 分别是类n 中方法的值参数 结果参数和值一结果参数 l n m 表示类 基于r c o s 的s y s m l 形式化研究 c d e c l 一 c n a m e s u pc l a s s p r i p r o t p u b d c d e c l 卜 c n a m e c n a m eu n s u p c l a s s s u p c l a s s0 hm ap r i p r i 0 n a p r o t p r o t 0 n a p u b p u b 0 o p o p0 nh 聊lh p a r a s l c 1 珑 b p a r a s c 其中 局部变量p r i p r o t 和p u b 用来记录n 的己声明属性 从中可以构建状态a t t r 在类 中依赖关系被指定前不能定义方法的动态行为 局部变量o p n 将方法i t i i 绑定在代码c i 上 六 程序的语义 令c d e c l s 为 个类声明域 g l b c 为p 的主方法 程序c d e c l s p 的含义被定义为类声明 c d e c l s 设计i n i t 和命令c 意义的组合 c d e l s p i n i t c d e c l s c 2 3 设计i n i t 执行下列操作 1 检查声明域的定义良好性 2 由p r i p r o t 和p u b 的值决定a t t r 和v i s i b l e a t t r 的值 3 定义每一个方法体c 4 检查g l b 的良构性 令d i 滓l 2 3 4 为设计i n i t 的条件 则其标准形式为 i n i t 一 v i b l e a t t a t t r d l d 2ad 3ad 4 卜 f v i s i b l e a t t r u n ai 口 p u b n l av n c n a m e a t t r n p r i n uu p r o t m up u b m i 型 i 1人o p n mi p a r a s w n 肌 i 研h p a r a s c o p m an e n e a p su l a t e d b 1 0 c k l x y c 旧舢工 口e v a t o r s 0 p er a t i o n l p 1 t y p e l t y p e 2 m r 临 p t o p er r y l b i oc i c1 甩枷 盥工 pr o p e r r 啦 b i oc k 2p 2 1 or d er e 4 啊瞌圯譬 pr o p e r t j e i n t e g e l 9 9 r e a d o n l y p t o p er r v 4 r ea l 1 0 0 口 q 唧魄噶 pr o pe r r s 5 b i oc k3 图4 1 模块的具体语法 f i g u r e4 1t h ec o n c r e t es y n t a xe x a m p l eo fb l o c k 系统的结构用模块定义图和内部模块图来描述 模块定义图描述了模块间的关系 如 组合 关联 分层等 模块定义图的语义是在u m l 类图的基础上进行了约束和扩展而得 到的 模块定义图的具体语法实例如图4 2 所示 1 9 基于r c o s 的s y s m l 形式化研究 图4 2 模块定义图的具体语法 f i g u r e4 2t h ec o n c r e t es y n t a xe x a m p l eo fb l o c k d e f i n i t o nd i a g r a m 例1 一个防滑煞车系统的防锁控制器的模块定义图如图4 3 所示 4 1 2 内部模块图简介 图4 3 防滑刹车系统的模块定义图 f i g u r e4 3a b s b l o c k d e f i n i t o nd i a g r a m 内部模块图用属性和连接子定义了一个模块的内部结构 它描述了部件间的交互 内 部模块定义图是在u m l 的复合结构图的基础上进行了约束和扩展而得到的 其具体语法实 例如图4 4 所示 图4 4 内部模块图的具体语法 f i g u r e4 4t h ec o n c r e t es y n t a xo fi n t e r n a lb l o c kd i a g r a m 例2 一个防滑煞车系统的防锁控制器的内部模块图如图4 5 所示 2 0 内蒙古大学硕十学位论文 4 1 3 顺序图简介 图4 5 反锁控制器的内部模块图 f i g u r e4 5a n t i l o c kc o n t r o l l e ri n t e r n a lb l o c kd i a g r a m 顺序图描述了参与者与系统 模块之间的控制流或系统 模块部件之间的交互 在 s y s m l 中不包括时间图 交互图和通信图 在s y s m l 中顺序图是最常用的交互图 它复用 了u m l 的顺序图 提供了基于行为的消息的实现 顺序图中的主要元素包括 1 对象及其生命线 控制期 对象用标有模块名称的方框来表示 对象图下方的一条垂直的虚线为该对象的生命线 代表对象的存在时期 在交互的整个过程中都存在的对象 它的生命线从图的顶部画到图 的底部 临时存在的对象的生命线从收到创建对象消息处开始画 直到收到撤销对象消息 时结束 用一个 作为标记 2 消息 消息可以激发某个操作 发送信号或导致某个对象的创建与撤销 用箭头来表示消息 方向为从发送方指向接收方 在顺序图中有三种不同形式的消息 实线黑箭头 表示调用操作或嵌套控制流 实线细箭头 表示异步通讯 发送方发送消息后立即执行后面的操作 不等待接收 方的返回消息 虚线细箭头 表示调用操作的返回 在s y s m l 中 默认消息的传递是即时的 即可以认为任何消息都不占用时间 但有时 2 l 基于r c o s 的s y s m l 形式化研究 还需要对消息的发送时间和接受时间加以约束 可以将约束条件置于顺序图左侧的空白处 用消息的顺序号或名称与消息相对应 例3 发动汽车的简单的黑盒顺序如图4 6 所示 其中 黑盒交互可以分解为白盒交互 图4 6 中的 h y b r i d s u v 是详细描述开始发动汽车时 h y b r i d s u v 内部发生事件的另一个交 互 具体内容参见例4 图4 6 发动汽车的简单的黑盒顺序图 f i g u r e4 6 s t a r t v e h i c l e b l a c k b o xs e q u e n c ed i a g r a m 例4 发动汽车的简单的白盒顺序如图4 7 所示 图4 7 描述了当汽车发动成功时 在 h y b i r d s l w 中发生的交互的顺序 图4 7 发动汽车的简单的白盒顺序图 f i g u r e4 7 s t a r t v e h i c l e w h i t e b o xs e q u e n c ed i a g r a m 2 2 内蒙古大学硕士学位论文 4 2s y s m l 中模块定义图 内部模块图和顺序图的形式化语义 4 2 1 s y s m l 中模块定义图的形式化语义 为了定义模块定义图 内部模块图和顺序图的语法 我们引入了四个集合 b n a m e a n a m e a t t r n a m e 和s i g 煎三个集合分别表示模块 关联以及属性 签名 s i g n a t u r e m x u y v 表示方法m m 带有一个输入参数x u 的列表和一个输出参数y v 的列表 s i g 表示所有签名的集合 缩写m 或m x y 表示符号m x u y v 对象的属性值的类型被称为数据类型 整数型用h l t 表示 布尔型用b o o l 表示 字符 型用c h a r 表示等 用r 来表示数据类型的集合 一 方法的规格说明 调用方法时 不仅要确保该方法的语义是正确的 面且要确保该方法的功能是良好的 下面给出了设计中一些简明符号 使用它们可以详细描述方法及方法的精化 该理论在 1 2 中有详细阐述 在u t p 中 程序或程序的命令用设计来描述 用序偶d 伍p 来表示 a 为设计的字母 表 p 为设计的规约 a 声暖了程序的变量 p 指明了程序的行为 a i n a o o u t a a 包括 程序的变量集合以及变量类型的集合 i n a 描述程序执行的初始状态的值 o u t a 描述程序执 行的终止状态的值 p 被称为设计的规约 是如下形式的谓词 plr o k a p 茗 o k 灭 i 其中 x 和x 表示a 中程序变量x 的初值和终值 谓词p 程序的前黉条件 播述已激活程序的初始状态并使程序执行到终止 谓词r 程序的后置条件 将程序的初始状态同其终止状态相关联 布尔变量酞和o k 用来描述程序的终止行为状态 当程序被正常激活时前者值为真 当程序执行正常终止时 后者值为真 在本节中 我们将用设计的符号来描述程序命令的语义 1 命令s k i p 表示 个程序正常终止 程序中的变量没有改变 s k i p 粼t r u e0 x x y y a a z x y z 是命令的