（通信与信息系统专业论文）基于asm的sdl语义形式定义研究.pdf

基于a s m 的s d l 语义形式定义研究 摘要 本文研究的重点是s d l 的形式语义定义方法，在分析s d l 8 8 和s d l 2 0 0 0 语义定义方法的 基础上提一种改进的s d l 2 0 0 0 形式语义的方法。另一方面，考虑到s d l 与u m l 结合使用的发 展趋势，提出用a s m 定义u m 屯形式语义的思想，使s d l 和u m l 可以在语义级统一起来。此 外，本文对形式验证s d l 规范的相关问题作了初步探讨，以期扩展s d l 形式语义定义的应用。 针对s d l 静态语义，本文提出的方法将语法域中元素视为项s d l 规范的所有子项可以表 示为作用于该s d l 规范的函数形式。从这个角度看，良形式条件定义了s d l 规范及其子项之间 的约束关系；转换规则定义了用基本概念子项替换s d l 规范中补充概念子项的模型；映射规则 定义了从a s 0 的语法域到a s l 的语法域的对应关系。其中，转换规则直接采用a s m 的更新规 则定义局部s d l 规范的更新；映射规则应用一系列t 函数实现，从而不必引入重写规则或使用 嵌套模式。 针对s d l 动态语义本文提出的方法采用解释执行的方式通过跟踪具有执行权的船p n f 实 例的当前状态及其关联的动作序列，解释执行动作序列中的动作。这样，s d l 规范与其a s m 语 义模型可以直接关联起来，从而提高了语义定义的连贯性和可理解性。对于复杂的动作，可以透 过引入辅助动作来帮助描述复杂动作的细节。对于面向对象的语法概念，可以通过特定函数计算 或构造完整的展开定义。此外这种方法将系统实例创建为实例结构树的形式，可以简化处理过 程调用和选择异常处理器时保存和恢复控制信息的问题；信号流模型可以从g n 把的角度定义。 这种动态语义定义方法可以采用基本a s m 来描述以便于形式验证( 如m 0 d e ic h e c i c i n g ) 的需要。 u m l 的出现和普及对s d l 语言在面向对象方面的发展产生了深远影响。建议z 1 0 9 专门制 定了从l 玎咀，到s d l 的映射规范。为了放宽对s d l 与u m l 结合使用的约束，采用相同的元语 言定义动态语义可以促进s d l 与u m l 一致地结合使用。考虑到r r u t 已采用a s m 定义s d l 的形式语义，因此采用a s m 定义u m l 的形式语义可以使s d l 和u m l 在语义级一致地表示 为a s m 模型。考虑到眦的复杂性，本文主要给出了定义u 1 札状态机动态语义的方法框架， 与现有的其它方法相比，这种语义定义可以反映u m 状态机的全部语义特征。 由于基本a s m 模型可以视为基于a s m 理论的可执行规范语言a s m l 的伪代码a s m 语义 模型可以方便地转换为相应的a s m l 程序。这样，利用a s m l 集成环境提供的从a s m l 程序生成 状态变迁图的功能，本文给出通过a s m 语义模型采用m o d e lc h e c l ( i 1 1 9 验证s d l 规范的方法框 架。此外，考虑到用于m o d e la l e c h n g 的时序逻辑公式过于数学化，本文给出用直观明了的路 径模式法来表示系统特性以及采用这种表示法构造b n c t i i 自动机的方法。 关键词：规范描述语言( s d l ) ，抽象状态机( a s m ) ，形式语义，一致建模语言( u m l ) ，形式验证。 基于a s m 的s d l 语义形式定义研究 a b s t r a c t t h i sp a p e rm “n l ys t u d i e s0 nt i l e 印p r o a c h e st od e 丘n et h es e m a n t i c so fs d li naf o r m a lw a ya n d p r e s e n t sai m p r o v e dm e t l l o dt od e 丘n em es e m a n 廿c so fs d lb a s e do na n a l y z i n g 血ef o r m a ld e 丘n i 虹o n s o fs d l 一8 8 柚ds d l 广2 0 0 0 o nl l l eo m 甘h 锄d 舔矗l ra ss d lc o m b i n i n g 、i t l lu m li sc o n c e r n e d t i l i s p a p e r 窟i v e sm i d e ao fu s i n ga s mt od e 矗n et l l ef o r m a ls 锄a n 虹c so fu m ls o 吐l a tb d 血s d lm o d e la n d u m lm o d e lc 蛐b ec o m b i n e dt o g e t l l e ra ts e m 锄吐cl e v e l i i la d d i 6 0 n ，h 1o 柑e rt oa p p l yf b r m a id e 丘n i t i o n m i sp 印e ra l s od i s c u s s e st h ep r d b l e m sr e l a i e dt o 吐l ef b r m a lv e r i 丘c a t i o no fs d ls p e c 嫡c a 吐o n s a st om es t a 石cs e m a l l 五c so fs d l t 1 1 em e 吐l o dp r e s e n t e di nm i sp a p 盯r e 叠盯d se l 啪t si ns v n t a c d c d o m a i na ss y n t a c 虹cv a l u e s ，c a l l e d 据m 昭t h e r e f o r e ，a ns d ls p e c i 丘c a t i o nc a nb es e e na sac o m 口o s i t e t e r m ，e v e r ys u b t e r mo fw h i c hc a l lb e 球p r e s e n t 耐a s 如a p p r o p r i a t ec o m p o s i t es f u n c 廿o na 口p i i e dt om e s d ls p e c i 丘c a t i o n f r o mm i sp 目s p t i v e ，w e l i f o r 删：d n 船sc o n d i d o n sd 娟n el 量l ec o n s 廿a i n c s 棚o n 鐾m e s d ls p e c i 6 c a t i o ni t s e l fa i l di t ss u b t e m s ：缸锄s f b r m a 吐o nr u k sd 嘶n eh o wt or e p i a c eas h o m l 蛐dc o 小 c 印ts u b t e r mw i t t lac o f ec o n c 印ts 出e 衄i nm es d ls p e c i 丘c a t i o n ；m p 口i 1 1 9r u l e sd e 丘n eh o wt om a 口a s ”t a c n ct e r mi na s 0 t om ec o 眦s p d i n gs ”t a c ct e r mi na s l h lp a r b c u l 甄m e 订如s f o r m a t i o nr u l e s a r ed e 矗n e db ya s mu p d a t er u l e sd 缸e c t l ya n d 吐1 em a p p i n gr u l e sa r ed f 蛹n e db yas e d e so ft _ f u n c c i o n s a sar e s u l t ，r e m i t i n gr u l e sa i l dn e s t e dp a 址鲫l sa f en ol o g e rn e e d e d a st ot h ed ”a m i cs e m 皿吐c s0 fs d l ，m em e 吐1 0 dp r e s t 酣i n 嘶sp a p e ri n t e r p r e t s 血es e m a l l 吐c s o ft h ea c t i o n sa m 油e dt o 也ec l 盯ts t a l eo fa na g e n ti n s t a 皿c ew i 吐le x e c u n o nr i 曲t sd i r e c t l yi n 血i s w a 弘t h es d ls p e c i f i c a t i o i ia | l di t sa s ms e m 蚰d cm o d e lc 柚b ec l o s e l ya s s o c i a t e dt o g e 吐l e r 如dc o n s e q u e n n y i m p r o v e t i ec o h 盯e n c y 卸d t l l e i n t e i 越百b i i i t yo f m e d e 丘n j d o no f t l l eb e h a v i o rs e m a n t i c s s o m e a u x m a r ya c t i o n s 盯ei n 垃o d u c e dt 0 圮i pd e 丘n et h ed e t a i l s0 f 吐l ec o m p l e x 虻o n s ；s p e c i n c 缸n c d o n sa r e u s o dt 0c o m p u t eo rc o n s 弧】c t 也ec o m p l e t ed e 丘n i d o n so fm ed b j e c t 0 r i e n t e dc o n c e p t s ha d d i t i o n ，m i s m e c h o db u i l d sa ni n s t a n c es 口m c t u r e 扛丘o mas d ls p e c i 丘c 撕o nb a s e do nt l l eo w n e rr e l a t i o n s h i p b e t w e e ne n 吐t yi n s t a l l c e st of 撕h t a t ep r o c 酣u r ei n v 删i o na n de x c e p 廿o nh 赫d l e rs e l e c t i o n ；出es i g n a l n o wm o d e l i sd e 疗n e d 丘o m 也ep e r s p e c 吐v eo f 占d 把a sar e s u l t 。1 i sm e i h o dc a nb ed e 矗n e db ym e a n so f t h es o c a l l e db a s i ca s mt oe a s ef o r m a lv e r i 丘c a d o n ( i e ，m o d e lc h e c l c i n g ) t h eo c c u r r e n c eo fu m lh 豁缸t 1 1 盯i m p a c t0 nt 1 1 ed c v e l o p m e n to fs d li nt 1 1 eo b i e c t o r i e n t e d a s p e c t ，胁o m m e n d a d o nz 1 0 9h 鲢d e 丘n e d 吐l em a p p i l l g 胁nu m lt os d l h d c rt or e i c a s et i l e c o n s t 阻i n t so n 血ec o m b i n a 吐o no fs d la n du m l ，u s i i l g 曲忙翮f n em c t “蚰g u a 霉ct o 枷n ct 艟如f m “ s e m a n t i c so ft h e mc a l lh e l pc o 溉n es d l 州t hu m lc o n s i s t e n t hc s i d e r i n ga s mi sa d o p t e dt o d e 行n et i l ef o r m a ls e m a n d c so fs d lb yr r u - t u s i n ga s mt od 嘶n em ef o r m a ls 锄挑c so fu m lc a n m a k es d l 卸di ，m i ，u l l i 右e dt 9 9 e c h e ra ts 啪柚d cl e v e li nf 砷lo fa s mm o d e l _ d u et on l ec o m p i e x i t y o f u m l ，m i sp a p e r m a i m y g i v 髂a 丘枷e w o r ko f h o w t od e 矗n e 1 e f o r m a ls e m 柚t i c so f u m ls t a t e c h a r 七 d i a 管a mb ym e a n so ft b eb a s i ca s m c o m p a r e dt o0 t l l e r 叩p 吣e s ，吐l i sa s ms e m 蚰吐c sm o d e lc a n c o v e ra 1 1 l h es e m 锄d c sc h a 工宣d 威蚶c s o f u 】ls t a t e c h a r td i a j 酗m s b e c a u s eb a s i ca s mm o d e lc 锄b es e e na sp s e t l d oc o d eo ft 1 1 ea s m _ b a s o de x e c u t a b l es p e c i 丘c a t i o n l a n 窑啦g ea s m lni sc o n v e n i 拍tf b rt 1 1 ea s ms e m 蛆血m o d e lt ob e 仕a t l s f b r m 酣i n t ot i l ee q u i v a l e n t a s m lp f o 掣锄t h e r e f o r e ，b ya p p l y i n gm ef u n c t i o n a l n y ，p r o v i d e db yt h ea s m li n i e 萝a t l 妇e 1 1 v i r o n m e n o fg e n e r a t i n gm es t a t e 垃柚s i 虹o ng r a p h 丘o mn l e 窑i v e l la s m lp r o 】f 锄，m i sp a p e rp r e s e n t sav e r i 矗c a t i o n f r a m e w o r k ，帆d e rw h i c has d ls p e c j 丘c a d o nc a l lb ev e r i 丘e db ym o d e lc h e c l ( i n 窖丘o mi c ss e m a l l t i c s m o d e l c a n s i d e r m 譬t t l et e m 口o c a i1 0 西cf b r m u l aa r em o r em a m e n 值d c s0 r i t e d ，伽sp a p 盯a l s o 叠i v 船锄 i n f u “i v er e 口r e s c n t a 廿o n ，n 椭酣p a 血p 砒啊，t 0s p e c i f y 也es y s t e mp r a p e 嘣髂t ob ev e r i 丘e d 抽w e l la s m em e 血o dt ob u i l db o c h i 蛐t o m a t 曲丘勺m l i sr e d r e s e n t a 毫i o l l k e y w o r d s ：s p e c 曲c 撕o n 锄dd e s 碰p 廿o n 山g u a g e ( s d l ) ，a b s 口扯ts t 8 t em a c h i n e ( a s m ) ，f o r m a l s e m a r i 廿c s ，u h i 丘e dm o d e u n g g u 矩e ( u m l ) ，f o r m a lv e r i f l c a t i 伽， 独创性( 或创新性) 声明 本人声明所呈交的论文是本人在导师指导下进行的研究工作及取得的研究 成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不 包含其他人已经发表或撰写过的研究成果，也不包含为获得北京邮电大学或其他 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示了谢意。 申请学位论文与资料若有不实之处 本人签名：鸯害姐。 本人承担一切相关责任。 臼期：丝堇：， 关于论文使用授权的说明 学位论文作者完全了解北京邮电大学有关保留和使用学位论文的规定，即： 研究生在校攻读学位期间论文工作的知识产权单位属北京邮电大学。学校有权保 留并向国家有关部门或机构送交论文的复印件和磁盘，允许学位论文被查阅和借 阅；学校可以公布学位论文的全部或部分内容，可以允许采用影印、缩印或其它 复制手段保存、汇编学位论文。( 保密的学位论文在解密后遵守此规定) 保密论文注释：本学位论文属于保密在一年解密后适用本授权书。非保密论 文注释： 本人 导师 基于a s m 的s d l 语义形式定义研究 第一章引言 作为国际电信联盟u ( i n t e m 州o n a l l h e c o m m l l n i c a 吐o n s u n i o n ) 推荐使用的形式描述技术，形 式描述语言s d l ( s p e c i n c a n o n “dd e s c r i 砸o nl a n g u a g e ) 广泛应用于电信领域的系统规范和软件 开发中，并且得到其它标准化发展组织如i s o 血t e r n 撕0 n a ls t d a r d i s a t i o no r g a i l i s a t i ) 和e t s i 圆1 1 r o p e t e l e c o m m u n i c a i t o n ss t a i l d a r 出n s t u 哟的认可。二十多年的发展完善，特别是自1 9 8 8 年开始形式语义定义的出现。标志着s d l 已经从一般的规范语言演变为成熟的形式描述语言。 1 1 研究背景 在s d l 语言定义中引入形式语义定义，一方面解决了用自然语言定义语义产生的二义性问 题：另一方面，使验证s d l 语言定义的一致性、s d l 系统规范的正确性以及自动生成s d l 规范 的程序级代码成为可能。然而，s d l 自1 9 7 6 年首次发布以来，虽然每4 年经历一次版本更新， 但是在正式的建议z 1 0 0 中，s d l 的语义定义都是以自然语言的形式给出的。直到1 9 8 8 年发布 s d l 8 8 【1 1 时，一个比较完整的s d l 语言的形式定义才在建议z 1 0 0 的附件酽4 】中首次给出。此 后发布的s d l 9 2 口1 及其修订版【虽然增加了面向对象等新的语言构件，仍然采用s d l 8 8 给出的 形式语义定义方法。 从s d l 的发展历史可知，s d l 是一种不断完善的形式描述语言。随着形式描述技术的进步， s d l 不可避免地需要引入新的语法概念或淘汰过时的语法概念。这意味着为了适应s d l 的发 展变化，定义s d l 形式语义的数学模型应该具有足够的灵活性和丰富的表达能力。另一方面， 由于s d l 以通信扩展有限状态机为模型，通过激励响应序列的方式定义系统的行为，所以，采 用操作语义定义s d l 可以直观地反映s d l 规范的动态行为。此外，尽管s d l 变得越来越复杂， s d l 的语义模型应该尽量保持良好的可理解性t e m 西b i l i t y ) 、可扩展性( s c a l 曲i l n y ) 以及可维护性 ( m a i n t a i n a b i l i t y ) 。鉴于此，1 9 9 9 年发布的s d l 2 0 0 0 采用分布式实时抽象状态机a s m ( a b s t r 虻t s t a t em a c h h l e ) 旧1 9 1 定义s d l 2 0 0 0 的形式语义o o 2 ”。 事实上，国内外的研究者分别提出了其它的s d l 形式语义定义方法。b e r g s 廿a 和m i d d l e b u r g 采用进程代数( p r sa l g 曲r a ) 定义带约束的基本s d “币s d l 0 的形式语义【1 q ，较好地反映了系统 的实时特性，但对s d l 的改动也较大。b r o y 【“】、h o l z 和s 啦e n 【1 2 l 应用f o c u s 的流处理函数( s 骶m p r o c e s s i n g n m c t i o n ) 定义s d l 子集的动态语义，侧重进程行为的函数表示，缺乏对静态结构和时 间特性的描述。m o f k 采用时段演算( d u r a t i o nc a l l l l s ) 刻画s d l 时间相关概念的语义【4 9 】，对时间 特性验证和进程调度簧略提供帮助。g o d s k e s e n 提出了s d l 8 8 子集的操作语义模型o “。f i s c h e r 和d i m i 仃o v 提出扩展p e t r i 网作为验证s d l 协议规范的形式基础【l 习；f 1 e i s d 血a c k 和g r a l l h a n n 使用高级p 瞰i 网定义s d l 的形式语义；m n d e r s p a c h e r 则利用基于项重写系统( t e r m _ r e l r i t i n g s y s t e m ) 的建模概念【1 5 】；r s c h e r 、l a u 和p 血z 使用0 协p 倍z 定义s d l 的语义模型【1 6 】。上述语义 定义方法，或者只考虑s d l 的子集，或者改动s d l 基本概念的语义；或者针对规范的验证。 值得一提的是，北京邮电大学计算机学院通信软件工程中心自1 9 9 7 年开始，在艾波教授的 指导下一直进行s d l 语义形式定义的研究工作。已毕业的倪朝博士提出了基于谓词演算的s d l 良形式条件定义方法和基于变迁系统的结构化操作语义模型【5 i 】。其中，前者被r r u t 第十研究 基于a s m 的s d l 语义形式定义研究 组采纳为定义s d l 广2 0 0 0 静态语义的主要方法之一。现在s d i 广2 0 0 0 的附件f 2 中给出的s d l 良 形式条件定义部分矧( 注意，与s d l 8 8 有所不同，s d 0 2 0 0 0 明确定义静态语义由良形式条件、 转换规则和映射规则三部分构成) 就是我们对倪朝方法进行完善的结果。 1 2 研究内容 在参与定义s d 0 2 0 0 0 静态语义工作的基础上，作者对s d l 完整的形式语义定义方法、s d l 结合u m l 以及s d l 规范形式验证( m o d e lc h e c l 【i n g ) 等问题作了进一步研究。因此，本文的主要 内容包括以下四个部分： 分析现有s d l 形式语义定义方法：首先介绍s d l 形式语义定义的内容和形式语义定义的一 般方法然后从静态语义和动态语义两个方面分析s d l 培8 和s d l 2 0 0 0 的语义定义方法。 改进s d l 2 0 0 0 形式语义定义方法：s d l 2 0 0 0 的语义定义方法改进了s d i ，8 8 方法存在的问 题，但是，这种方法本身也有需要完善的地方。此外，考虑到语义模型的可执行性和通过 语义模型形式验证s d l 规范的可行性，本文采用基本a s m 给出这种改进的形式语义定义 方法。这种方法在保持原有方法优点的前提下，针对原有方法存在的问题在一定程度上作 了改进。由于基本a s m 模型可以视为基于a s m 理论的可执行规范语言a s m l 的伪代码， 本文给出的a s m 语义模型可以方便地转换为相应的a s m l 程序，在a s m l 集成环境中，可 以真正运行这个语义模型，并且使通过该语义模型实现形式验证s 现规范成为可能。 研究s d l 与u m l 结台使用的相关问题：由于眦提供从不同角度描述系统的模型构件， 使s d l 与u m l 结合使用的需求越来越多。如何保证各种u m l 模型以及s d l 模型之间的 一致性，是实现s d l 与u m l 无缝地结台使用的关键。本文提出s d l 与u m l 在语义级相 结合的思想，即采用a s m 定义眦的形式语义，这样s d l 和u m l 可以在语义级统一成 a s m 模型，并在此基础上验证s d l 模型与u m l 模型的一致性。考虑到u m l 的复杂性， 本文主要针对u m l 状态机，给出其基本a s m 语义模型的定义框架。 探讨形式验证s d l 规范的相关问题：m o d e l c h e c k 抽g 是一种适合自动验证有限状态系统的 形式验证方法，但是m o d e lc h e d d n g 工具接受的语言通常只有有限的表达能力和简单的 数据类型。因此，将s 仉规范转换为给定m o d e l c h e c 】d n g 工具的输入会受到相应的限制。 本文给出通过语义模型验证s d l 规范的方法可以避免上述问题。此外，用于m o d e l c h e c k i n g 的时序逻辑公式通常过于数学化，本文给出直观的路径模式表示法，可以直观明了地表示 时序逻辑公式，并且可以构造直接用于m 0 d e io l e c h n g 的b n c h i 自动机。 本文其余部分的组织结构如下：第二章简介s d l 语言的内容；第三章概述用于定义s d l 形 式语义的a s m ；第四章分析s d l 8 8 和s d l _ 2 0 0 0 的形式语义定义方法：第五章给出用基本a s m 定义的改进的s d l 形式语义定义方法；第六章研究s d l 与u m l 结合使用的相关问题：第七章 探讨s d l 规范形式验证的相关问题：第八章总结现有的研究工作并展望今后的研究方向。 2 基于a s m 的s d l 语义形式定义研究 第二章s d l 语言 规范描述语言s d l 是国际电联推荐使用的一致建模语言之一，主要用于无二义性地规范或 描述电信领域中的复杂系统和通信协议。这里，术语“规范”定义系统中要求的行为；而“描述” 定义系统中实际的行为。从使用s d l 角度看，不必区分用s d l 规范”系统还是“描述 系统，因 此，本文中的“规范”泛指对系统要求的行为或实际的行为的描述。 s d l 的发展可以追溯到1 9 7 2 年，人们认识到有必要开发一种标准语言来规范复杂系统的行 为h “。最早的s d l 语言于1 9 7 6 年以建议的形式首次发布。此后，s d l 语言每隔四年进行一次 版本升级：7 6 年版只能规范简单系统的行为；8 0 年版引入结构化机制；8 4 年版引入基于抽象数 据类型的数据定义：8 8 年版首次给出s d l 语言语义的形式定义；9 2 年版引入面向对象概念，远 程过程调用和非确定性机制；9 6 年版对9 2 版s d l 语言做了微小的扩充并对存在的问题作了修 正；2 0 0 0 年版完全基于面向对象技术并且采用新的形式方法定义语义。从1 9 8 8 年开始，s d i 。语 言形式语义的出现标志着s d l 从标准规范语言发展成为成熟的形式描述技术。为了区分不同版 本的s d l ，8 8 年版建议简称s d l 8 8 ；9 2 年版简称s d l 9 2 ；2 0 0 0 年版简称s d l 2 0 0 0 。 本章首先介绍s d l 的文法表示；然后从语义角度将s d l 的语法概念分成面向对象的概念、 结构、行为、时间以及数据五个方面介绍；最后给出s d l 规范的实例并得出结论。 2 1 文法表示 s d l 建议z 1 0 0 提供两种规范系统的方法：图形表示法s d u g r ( g r a p l l i cr 印r e s e n 忸t i 如) 和正 文表示法s d m p r f r e x t u a ln l r 勰er e 班e s e n 协血o n ) 。这两种表示法包含描述各种系统的丰富概念。 然而，如果直接在两种表示法上定义s d l 语义势必增加语义定义的复杂性，并且难以保证两种 表示法的语义定义等价。为此，z 1 0 0 中引入了可以将这两种表示法统一起来的抽象文法( a b s 仕a c t g r a m m 哪。与抽象文法相对，图形表示法和正文表示法属于具体文法，不妨称之为具体图形文法 和具体正文文法。抽象文法是具体文法的语义级抽象。这样，在抽象文法上定义s d l 语义可以 降低语义定义的复杂性，并且容易保证语义定义的统一。也就是说两种具体文法可以通过与抽 象文法的关系获得抽象文法的语义。 在s d l 中，文法( g r a 删m r ) 的定义包括两部分：语法( s ”t a x ) 和良形式( w e l l - f h m e d n e s s ) 条件a 其中，语法定义语言构件之间的组成关系；良形式条件定义语言构件之间的约束关系。这里，语 言构件又可称为语法概念或简称为概念。在具体语法中语法概念分为两类：基本概念和补充概 念。其中，补充概念是基本概念的简化形式。每个补充概念都存在变换为基本概念的模型( m o d e l ) 。 换句话说，补充概念通过模型得到自己的语义。这样，具体语法的语义可以通过基本概念的语义 获得。抽象语法中的概念是对具体语法中基本概念的抽象。具体语法中的基本概念根据这种抽象 映射为抽象语法中的相应概念，即基本概念可以通过映射关系得到相应抽象语法概念的语义。 2 2 面向对象的概念 对象( o b j e c t ) 是数据结构( d a t es 仕u c t u r e ) 和行为( b e h “i o r ) 的结合体。其中，数据结构描述对象 的逻辑信息；行为描述应用于数据的操作( o p e r 撕o n ) 。面向对象( o b j e c t 耐t 鲥o n ) 意味着按照对 3 基于a s m 的s d l 语义形式定义研究 象的观点描述事物。s d l 2 0 0 0 是一种面向对象的规范语言，但是由于历史原因，面向对象的术 语类( c l a s s ) 在s d l 中称为类型( 呻e ) ；而对象则称为实例( i n s t a n c e ) 。 在s d l 中，类型和实例通过定义( d e 6 n i t i ) 来描述定义、类型和实例之间的关系如图2 1 所示。参数化类型( p a r a m e c e r i z e dt 卵e ) 是带有形式上下文参数( t b m a ic o n 把x tp a r a m e c 盯) 的类型。 用实际上下文参数( a c t u a lc o n t e x tp e t e r ) 替换参数化类型中的部分形式上下文参数仍得到参数 化类型；而替换全部形式上下文参数可得l 通常意义上的类型。通过增加或重定义类型( 父类型) 中的特性( p r o p e r t y ) 可得到这个类型的子类型( s p e c i a l 协畸o n ) 。对非抽象类型的实例化( i n s 协n n a t i ) 可得到这个类型的实例定义。当然，实例也可以直接定义。直接定义的实例隐含地定义了这个实 例的类型( i m p u e dt y p e ) 并且这个实例定义就是这个隐含类型实例化的结果。 圈2 1 定义、类型和实例的关系图 有些s d l 构件既存在实例定义也存在类型定义。这时，为叙述方便，“实例”的限定可以省 略，但“类型”的限定必须保留。例如，系统( 5 y s t 锄) 定义意味着系统实倒的定义：丽提到系统 类型定义则不能省略“类型”的限定。其它s d l 构件只能或者作为类型存在或者作为实例存在。 这时“类型”和“实例”的限定都可省略。例如，信号( s i g n a l ) 定义总是指信号类型的定义：而 信道( c h a n n e l ) 定义总是指信道实例的定义。 2 3 结构 从s d l 的角度看，客观世界分为两部分：系统和环境。s d l 规范可以描述系统如何响应从 环境到系统的激励( s d m u u ) ，但对系统所处的环境本身却不能定义。尽管环境的行为是非确定的 ( n o n d e t e r 删n i s d c ) ，s d l 系统规范可以给出环境应该服从的约束。特别地，环境可以视为一种特 殊的系统，其中的实例与s d l 系统中的实例采用不同的实例标识符p i d 来标识。 在s d l 2 0 0 0 中，系统( 日，咖m ) 可以分解成多个功能块( 6 k 砷和进程( p m c ) 。其中，功能块 又可以分解成更简单的功能块和进程；进程又可以分解成更简单的进程。依此类推，直到系统中 所有的功能块和进程都不再进一步分解为止。这样，系统、功能块和进程分别描述不同抽象层次 的系统模块，统称为姐p 小。注意，系统相当于最外层的功能块，不能定义在其它d g 小中，并 且只能有一个实例。因此。口筘n f 实际上只有两种：功能块和进程。 4 基于a s m 的s d l 语义形式定义研究 作为面向对象的规范描述语言，s d l q g m r 主要由三部分构成：属性( 参数和变量) ；行为( 显 式或隐式定义的状态机) ：结构( 昭n f 集和通信路径) 。口g e n f 可以显式或隐式地通过口水n r 类型定 义。哪“r 定义实际上定义了这种船“f 类型的实例集胖眦实例可以通过创建( c f e 缸e ) 动作自4 建， 也可以通过实例化站f 定义得到。创建铅e ，l f 实例意味着递归地创建所有在这个日舻肿定义中 定义的d g p 时实例，这些孵p 眦实例称为初始( i n i n d 凹“略e n f 实例之间通过称为信道( 血a n n e l ) 的通信路径相关联。信道包括延时信道和无延时信道两种。日肚n f 实例的状态机是通信扩展有限 状态机。口g e n r 实例的状态机之间通过信道传递信号。每个咯日n f 实例的状态机都设有一个接收 信号的输入端口( m p u tp o r t ) 。输入端口是一个扩展的先入先出( f i f o ) 队列。所有到达凹m f 实例 的信号按照到达时间的先后顺序在其输入端口中排队等待处理。 昭e n r 定义蕴含着接口定义，这个接口定义隐式地定义了与这个昭e 眦同名的p i d 类别( s o r t ) 。 每个昭p m 实例都存在四个p i d 类别的匿名变量，这四个变量的值分别由p i d 类别的动态表达式 s e l p a n n t ，o 凰p r l 唱和n d e r 确定。其中，s e l f 表示这个a 扩埘实例本身：p a m n t 表示创建这 个口g e 卅实例的昭e 卅实例；o f 唧r i n g 表示这个凹e n f 实例创建的最新的钾f 实例：s e n d e r 表 示这个d 目f 实例最近消耗的信号的发送者。注意，对于系统初始化时创建的卵f 实例，其p e n t 为比对于新创建的a 胛耐实例，其n d e r 和胡印r i g 都为 忆玑 2 4 行为 s d l 甜e 卅在定义系统结构的同时也定义了系统的行为。s d l 规范的行为定义为系统实例中 所有a p e 耐的状态机的行为。其中，功能块的状态机与定义在这个功能块中的钾e ，i f 的状态机并 行地( c o n c u “e n n y ) 工作；进程的状态机与定义在这个进程中的进程的状态机交替地( a l t m l a t i v e l ” 工作。状态机之间可以通过发送信号、远程过程调用、出口( e x p o n e d ) 变量以及共享变量等方式 交换信息。 当系统实例以及直接或间接地定义在系统中的所有初始口占m f 创建完成后，信号开始在状态 机之间和状态机与环境之间传递。同时，系统中所有的状态机进入执行“开始( s t a r t ) ”动作状态a 随着开始动作的结束，状态机进入等待输入信号的状态。如果状态机的输入端口中存在可以接收 的信号，则这个信号从输入端口中被移出并消耗。然后，状态机通过触发相应的变迁( 乱s 城o n ) 进入下一个状态。注意，隐含消耗的信号直接从输入端口中删除即可。如果没有可以接收的信号， 状态机可以尝试消耗连续信号( c o n d n u o u s 蛔锄。在选择可消耗信号的过程中，可能随时发生自 发变迁( s p 。n t a n e s 妇n s i n o n ) 。自发变迁不依赖于输入信号，用于描述系统的非确定行为。重复 上述过程，直到状态机执行“停止( s t o p ) ”动作或发生异常( “c e 州o n ) 信号 对于功能块的状态机，如果功能块在执行停止动作时仍然包含括动的口g f 那么，这个功 能块进入停止状态( s t o p p m gc o n d i n ) 。在这个状态，状态机只处理来自内部昭r 的读写请求， 而不再接收来自外部的任何信号。当所有内部的珏g e n f 停止活动时，处于停止状态的功能块才真 正停止活动。对于进程的状态机，如果进程在执行停止动作时仍然包含活动的进程，那么这个 进程处于停止状态。当所有内部的进程停止活动时，处于停止状态的进程才真正停止活动。钾e m 停止活动意味菅这个卵f 实例不复存在，其p i d 也不再有效。 如果状态机在执行动作时发生异常信号。那么，状态机从异常发生的动作开始，按照作用域 由小到大的顺序，向上逐层查找可以捕获这个异常信号的活动的异常处理器( e x c e p n o nh d l 口) 。 找到，则消耗这个异常信号并触发相应的异常处理变迁；否则，状态机保持在发生异常时的状态， 5 基于a s m 的s d l 语义形式定义研究 但以后的行为无法确定，即系统发生了错误( e r r o r ) 。注意，如果异常发生在被调用的远程过程中， 那么，异常信号仍然会传播到调用者，并把相应的调用动作视为异常的发生地点。 为了规范复杂系统的行为，s d l 中引入复合状态( c o m p o s i t es t a t e ) 的概念。复合状态有复合状 态图( c o m p o s i t es t a t e 掣a p h ) 和状态聚集( s 呲ea 黯r e g a d o n ) 两种形式。前者相当于一个子状态机：后 者相当于一组交替执行的子状态机。 2 5 时间 作为规范语言，为了保持语义的抽象性，s d l 投有关于时间本身行为的任何假设或约束。 在s d l 中，动作没有明确的执行时间；状态机可以在当前状态停留任意长时间：信道分为延时 和非延时两种，但不限定延时信道的延时区间：定时器( d m e r ) 只能定义最少的等待处理时间：信 号在输入端口中可能等待任意长时间。由于上述时间问题应该依赖于实现规范的具体系统，s d l 中只包含简单的与时间相关的概念。s d l 假定系统采用统一的全局时钟，提供动态表达式呐w 获得系统的当前时间并提供定时器以及相关的置位( s e t ) 和复位( r e t ) 操作来规范系统需要满足的 时间特性。注意，s d l 不能规范时间的运动方式和时间的度量单位。 2 6 数据 在s d l 中，数据的定义基于抽象数据类型( a b s 口a c td a t at y p e ) 。抽象数据类型定义为数据元 素( d a t ai t e m ) 集以及作用于数据元素集的操作( o p 州i o n ) 集。由于数据元素集和操作集描述了数据 类型的抽象特性，因此，s d l 可以不依赖于具体实现而定义数据类型。注意，抽象数据类型的 抽象含义与面向对象概念中抽象类型( a b s 廿a c t t y p e ) 的抽象含义不同，为了区别二者，本文将抽象 数据类型简称为数据类型。 s d l 采用面向对象的方法定义数据类型。由于接口定义a n t 刚沁ed 娟n 坩o n ) 可以视为特殊的 对象类型，s d l 中主要有两种数据类型：值类型( v a l u e 帅e ) 和对象类型( o b j e c tt y p e ) a 数据类型中 元索集定义为与这个数据类型同名的类别( s o r t ) 。值类别中的元素是值；对象类别中的元素是对 象。特别地，接口类型的类别称为p i d 类别，p i d 类别中的元素称为标识a 弘眦实例的p i d 。注意， 对象是对值的引用( r c 向) ；而p i d 是对q 弘时实例的引用值类型和对象类型是抽象对象类型 a n y 直接或间接的子类型。类似地，接口类型是接口类型p i d 直接或间接的子类型。值类型和对 象类型只能有一个父类型 而接口类型可以有多个父类型。 为了简化系统规范的定义，s d l 预定义了一些常用的数据类型，如b o o l e ，i n t e g n a t u m l ， r e a l ，0 1 a r