UML状态机的形式语义 被引量：26

1

作者 蒋慧 谢希仁 林东 《软件学报》 EI CSCD 北大核心 2002年第12期2244-2250,共7页

许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制——状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形... 许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制——状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明,为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotkin风格的结构操作语义SOS(structural operational semantics)规则归纳地给出满足组合性的UML状态机语义.此方法既是对一些经典Statechart形式化方法的综合,又针对UML状态机的特点作了创新,使状态项能够动态地描述任意时刻UML状态机的配置树,简化LTS的标记,同时,结构化的语义规则更为形式化验证奠定了基础. 展开更多

关键词 UML 状态机 形式语义 面向对象 建模语言

下载PDF 职称材料

基于标记变迁系统的可信计算平台信任链测试 被引量：19

2

作者 徐明迪 张焕国 严飞 《计算机学报》 EI CSCD 北大核心 2009年第4期635-645,共11页

可信计算是当今世界信息安全领域的重要潮流之一.根据国家有关规定,信息安全产品需要经过测评认证,但目前国内外对可信计算测试的理论与技术研究还非常不完善,也无相应测试工具或系统,这必然影响可信计算的发展.该文着眼于规范定义的信... 可信计算是当今世界信息安全领域的重要潮流之一.根据国家有关规定,信息安全产品需要经过测评认证,但目前国内外对可信计算测试的理论与技术研究还非常不完善,也无相应测试工具或系统,这必然影响可信计算的发展.该文着眼于规范定义的信任链行为特征,以进程代数作为指称语义描述工具,以标记变迁系统作为操作语义,对规范定义的信任链行为特征进行了形式化描述,提出了一种基于标记变迁系统的信任链测试模型框架.针对信任链规范与实现之间的问题,从易测性出发对测试集进行了有效约简;并论证了信任链的规范实现与规范说明之间的关系,为测试用例构造方法提供了理论依据,从而解决了信任链测试这一难题. 展开更多

关键词 可信计算平台 信任链 进程代数 标记变迁系统 一致性测试

下载PDF 职称材料

互模拟的一些基本性质 被引量：8

3

作者 李娜 姚从军 《云南师范大学学报（哲学社会科学版）》 CSSCI 2010年第5期68-73,共6页

由于互模拟的概念几乎同时在计算机科学、模态逻辑和集合论中产生,本文试图给出一种能够刻画计算机科学、模态逻辑和集合论中互模拟概念的统一定义。因此,本文首先简单介绍互模拟产生的原因及作用;其次,给出两个加标转换系统之间的互模... 由于互模拟的概念几乎同时在计算机科学、模态逻辑和集合论中产生,本文试图给出一种能够刻画计算机科学、模态逻辑和集合论中互模拟概念的统一定义。因此,本文首先简单介绍互模拟产生的原因及作用;其次,给出两个加标转换系统之间的互模拟定义,并说明由此定义如何得到计算机科学中、模态逻辑中以及集合论中互模拟的定义;最后证明在这种定义下,互模拟的一些基本性质。 展开更多

关键词 关系结构 加标转换系统 互模拟

下载PDF 职称材料

一种形式化的协议互操作性测试方法 被引量：6

4

作者 郝瑞兵 吴建平 《计算机学报》 EI CSCD 北大核心 1997年第4期350-359,共10页

对协议实现的互操作性测试是保证网络产品之间互通的一种重要手段．在本文中我们提出了一种基于并发ＴＴＣＮ操作语义的互操作性测试系统的构造方法．并发ＴＴＣＮ是一种能够处理并发测试行为描述的语言，我们通过使用标号变迁系统形式... 对协议实现的互操作性测试是保证网络产品之间互通的一种重要手段．在本文中我们提出了一种基于并发ＴＴＣＮ操作语义的互操作性测试系统的构造方法．并发ＴＴＣＮ是一种能够处理并发测试行为描述的语言，我们通过使用标号变迁系统形式化地定义了它的操作语义，并描述了基于这种语言的操作语义的互操作性测试系统的测试执行和测试判决过程．我们认为这种方法对研究形式化的协议互操作性测试理论是很有帮助的． 展开更多

关键词 协议互操作性测试 协议一致性测试 标号变迁系统

下载PDF 职称材料

一种可信虚拟机迁移模型构建方法 被引量：6

5

作者 石源 张焕国 吴福生 《计算机研究与发展》 EI CSCD 北大核心 2017年第10期2284-2295,共12页

虚拟机的安全迁移是保障云环境安全可信的重要需求之一.对于包含虚拟可信平台模块(virtual TPM,vTPM)的可信虚拟机,还需要考虑vTPM的安全迁移问题.目前,已有一些针对可信虚拟机的安全迁移的研究,但是由于研究可信虚拟机的模型不统一,导... 虚拟机的安全迁移是保障云环境安全可信的重要需求之一.对于包含虚拟可信平台模块(virtual TPM,vTPM)的可信虚拟机,还需要考虑vTPM的安全迁移问题.目前,已有一些针对可信虚拟机的安全迁移的研究,但是由于研究可信虚拟机的模型不统一,导致迁移模型解决问题的方案不能适用所有的迁移方案,存在一定的局限性.针对可信虚拟机的迁移缺乏统一的安全模型及测试方法的问题,参考虚拟机迁移中普遍存在的安全问题以及可信计算和云的相关规范,从整体系统层面对可信虚拟机的迁移进行安全需求分析;提出一种可信虚拟机迁移框架,将可信迁移的参与组件进行了抽象并描述了迁移协议中的关键步骤和状态;以标号迁移系统LTS为操作语义描述工具对可信迁移系统进行进一步的描述,以系统中迁移进程组件的建模为基础构建出动态的迁移系统状态迁移树;分析了LTS模型可以用于可信迁移协议的一致性测试,并通过与其他相关工作的比较说明了模型在考虑安全属性方面的完备性. 展开更多

关键词 可信虚拟机 虚拟机迁移 安全协议 标号迁移系统 安全模型

下载PDF 职称材料

一种计算有限标号转移系统模拟关系的算法 被引量：2

6

作者 蔡烜 郑一源 《上海交通大学学报》 EI CAS CSCD 北大核心 2009年第11期1784-1787,共4页

基于一般的有限标号转移系统,研究了进程演算中的模拟关系,提出了一个计算进程演算中模拟关系的算法,其时间复杂度为O(mn).

关键词 进程演算 并发系统 模拟关系 标号转移系统 算法

下载PDF 职称材料

基于动作序列的行为需求模式验证的研究 被引量：2

7

作者 杜军威 徐中伟 江峰 《通信学报》 EI CSCD 北大核心 2011年第1期94-105,共12页

提出了基于动作序列刻画安全关键系统的功能行为需求和安全性行为需求,较传统的类逻辑规范和类图式规范更准确表达交互行为间的时序关系。基于动作序列构造功能需求和安全需求两类行为模式,并给出每个模式的操作语义。为实现基于行为模... 提出了基于动作序列刻画安全关键系统的功能行为需求和安全性行为需求,较传统的类逻辑规范和类图式规范更准确表达交互行为间的时序关系。基于动作序列构造功能需求和安全需求两类行为模式,并给出每个模式的操作语义。为实现基于行为模式的需求验证,重新定义LTS安全性和活性的属性表达、组合操作,给出并证明功能需求模式和安全性需求模式满足的充要条件。该框架在高速铁路CTCS2/3的形式验证与确认得到了广泛应用,对指导构件化安全关键系统的组合形式验证具有较高的理论与实践价值。 展开更多

关键词 安全关键系统 动作序列 行为需求模式 标签变迁系统 模式验证

下载PDF 职称材料

体系结构层状态型方面的建模和编织——基于LTS的方法 被引量：1

8

作者 杨春花 王海洋 《计算机学报》 EI CSCD 北大核心 2011年第2期342-352,共11页

状态型方面是一种封装反应式关注点的方面,它需要专门的切点机制来跟踪系统的执行历史.然而当前在体系结构层还缺乏支持状态型方面建模的有效机制.针对这一问题,提出一种体系结构层状态型方面的建模和编织方法.它以标记转换系统(Labelle... 状态型方面是一种封装反应式关注点的方面,它需要专门的切点机制来跟踪系统的执行历史.然而当前在体系结构层还缺乏支持状态型方面建模的有效机制.针对这一问题,提出一种体系结构层状态型方面的建模和编织方法.它以标记转换系统(Labelled Transition System,LTS)为底层形式化,建立了用于识别系统运行轨迹中特定模式的切点机制,并定义了支持多种通知类型的编织运算.该方法当前已在一个基于FSP规范的原型编织工具上实现,并用一个实例说明了该方法的有效性. 展开更多

关键词 方面 状态型方面 编织 标记转换系统 面向方面的软件开发

下载PDF 职称材料

标记迁移系统的组合可达性分析 被引量：2

9

作者 文艳军 王戟 齐治昌 《计算机科学》 CSCD 北大核心 2005年第12期110-111,145,共3页

标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描... 标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描述和精确表达。本文对其基本原理进行了分析和概括,并作了形式化陈述,证明了相关结论。本文的工作有助于深入理解和澄清组合可达性分析的内部工作机制。 展开更多

关键词 标记迁移系统 计算机辅助设计和验证 组合可达性分析 状态空间爆炸问题 观察等价

下载PDF 职称材料

基于事件结构的并发程序可视化调试方法 被引量：2

10

作者 伍晓泉 魏峻 《软件学报》 EI CSCD 北大核心 2014年第3期457-471,共15页

在多核和并发技术得到广泛应用的今天,如何有效地调试并发程序,成为一个重要且亟待解决的研究课题.并发程序的不确定性及其行为的复杂性,使得传统的调试技术难以得到有效的应用;而软件维护场景中错误发现与错误调试过程的分离使得错误... 在多核和并发技术得到广泛应用的今天,如何有效地调试并发程序,成为一个重要且亟待解决的研究课题.并发程序的不确定性及其行为的复杂性,使得传统的调试技术难以得到有效的应用;而软件维护场景中错误发现与错误调试过程的分离使得错误重现难以实现,面向缺陷报告的调试需求使得自动的错误定位技术难以应用,加剧了调试的困难.针对软件维护阶段由缺陷报告导向的程序调试场景,提出了可视化的并发程序调试方法.该方法能够根据缺陷报告中的信息对程序进行切片,缩小需要分析的代码范围;通过静态分析构造出程序行为的全局视图,帮助程序员发现隐含的程序执行路径;根据事件结构的语义简化程序行为视图,使得行为模型规模可控;根据图形中的分支,引导用户关注路径中的关键操作,从而更快地发现程序中的缺陷.与动态调试方法相比,该方法能够避免错误重现的代价.借助缺陷报告中的信息以及事件结构模型的特点,该方法能够尽量减少状态爆炸的发生.已开发出的交互式并发程序调试工具原型JESVis Debugger,初步实现了所提出的方法. 展开更多

关键词 可视化调试 并发程序 事件结构 配置结构 标记迁移系统

下载PDF 职称材料

微服务的死锁兼容性检测 被引量：2

11

作者 李呓瑾 吴玮 +2 位作者 张雪坚 陈姣 彭剑锋 《电子设计工程》 2021年第4期11-15,共5页

兼容性检测是使用微服务构建软件时将面临的一个关键问题,如果一组微服务的组合满足某些属性,如无死锁,则称这组微服务是兼容的。但是,微服务固有的动态性和复杂性给兼容性检测带来了新的挑战。提出了一种微服务的死锁兼容性检测方法,... 兼容性检测是使用微服务构建软件时将面临的一个关键问题,如果一组微服务的组合满足某些属性,如无死锁,则称这组微服务是兼容的。但是,微服务固有的动态性和复杂性给兼容性检测带来了新的挑战。提出了一种微服务的死锁兼容性检测方法,该方法使用标号迁移系统建模微服务和微服务间的异步组合;提出了死锁兼容性的定义,并给出了死锁兼容性的检测算法。在工具的支持下,实现了死锁兼容性检测方法,并通过实验证明该方法是有效的。 展开更多

关键词 微服务 兼容性 死锁 标号迁移系统

下载PDF 职称材料

基于标签转移系统的二乘二取二系统的形式化验证研究 被引量：1

12

作者 付伟 《铁道标准设计》 北大核心 2018年第7期164-168,共5页

为了提高二乘二取二系统的安全应用特性,系统的安全相关逻辑在投入使用前必须进行验证。模型检验是验证系统安全属性的有效手段之一。提出基于转移标签系统模型验证系统安全属性的新方法。针对系统的安全需求,利用LTS对系统行为进行建... 为了提高二乘二取二系统的安全应用特性,系统的安全相关逻辑在投入使用前必须进行验证。模型检验是验证系统安全属性的有效手段之一。提出基于转移标签系统模型验证系统安全属性的新方法。针对系统的安全需求,利用LTS对系统行为进行建模处理,最后使用LTSA软件对模型的安全属性进行分析和验证,与传统人工验证方法相比,LTS模型产生程序缺陷少64%,同时节省开发工作时间29%。结果表明:该方法有效地实现了对系统属性的安全验证,并对系统的安全设计和开发进行了改进。 展开更多

关键词 CTCS系统 模型校验 标签转移系统 二乘二取二

下载PDF 职称材料

互模拟准局部验证算法的扩展与实现 被引量：1

13

作者 郑晓琳 邓玉欣 +1 位作者 付辰 雷国庆 《软件学报》 EI CSCD 北大核心 2018年第6期1517-1526,共10页

互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验,发... 互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验,发现在大多数情况下,前者的性能比后者更好.同时,修改了算法使其能够验证模拟关系.最后,用Java实现对标记迁移系统进行转换,使算法同时可以验证弱互模拟关系. 展开更多

关键词 互模拟 标记迁移系统 扩展

下载PDF 职称材料

映射ELOTOS到基于FSM的性能估价模型

14

作者 罗铁庚 陈火旺 +1 位作者 龚正虎 齐治昌 《软件学报》 EI CSCD 北大核心 1997年第10期788-792,共5页

ELOTOS是协议描述规范语言LOTOS的扩展．本文用标号转换系统LTS（labeledtransitionsystem）给出了ELOTOS的语义．然后，通过对LTS进行踪迹等价住分析，将ELOTOS映射到基于有穷状态机FSM（finitestatemachine）的性能估价模型．

关键词 ELOTOS FSM 性能模型 网络协议 计算机网络

下载PDF 职称材料

生成诊断公式的有限状态进程等价验证 被引量：1

15

作者 李明 《计算机工程与设计》 CSCD 北大核心 2010年第2期344-347,共4页

分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统。给出生成Hennessy-Milner逻辑描述的诊断公式的算法... 分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统。给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式。算法的时间复杂度为O(mlogn),空间复杂度为O(m+n)。 展开更多

关键词 互模拟 形式验证 带标号的迁移系统 有限状态进程 Hennessy-Milner逻辑

下载PDF 职称材料

并发系统的安全性与活性的验证方法

16

作者 李杨 程建华 +2 位作者 房鼎益 陈晓江 冯健 《计算机工程与应用》 CSCD 北大核心 2008年第4期107-110,共4页

网络环境下的分布式系统是典型的并发系统。安全性和活性是并发系统最为关注和需要保证的两个主要性质。然而在并发系统建模和形式化验证时,面临着描述繁琐、复杂和难以理解的问题,特别是当并发系统的规模(并发进程数目)较大时其性质验... 网络环境下的分布式系统是典型的并发系统。安全性和活性是并发系统最为关注和需要保证的两个主要性质。然而在并发系统建模和形式化验证时,面临着描述繁琐、复杂和难以理解的问题,特别是当并发系统的规模(并发进程数目)较大时其性质验证时的效率问题更是严重阻碍了并发系统模型检测与验证技术的应用。将组合可达性分析和标号迁移系统的模块化思想与模型验证技术相结合,提出了一套有效的性质验证方法。论证、分析了三个并发系统安全性和活性验证定理,据此导出了并发系统的安全性与活性验证的有效算法。并通过一个简单实例,对算法有效性进行了初步验证。 展开更多

关键词 并发系统 安全性 活性 组合可达性 标号迁移系统

下载PDF 职称材料

标号迁移系统的互模拟关系及其性质

17

作者 唐郑熠 林佳音 黄泽斌 《福建工程学院学报》 CAS 2018年第6期547-552,共6页

以标号迁移系统为工具,探讨了系统行为的等价性问题,构建了模拟及互模拟关系的形式化模型,进而将互模拟的概念推广到了系统的层面,进一步探讨了模拟及互模拟关系的性质,揭示了互模拟概念的本质,为其在形式化分析及验证技术中的应用提供... 以标号迁移系统为工具,探讨了系统行为的等价性问题,构建了模拟及互模拟关系的形式化模型,进而将互模拟的概念推广到了系统的层面,进一步探讨了模拟及互模拟关系的性质,揭示了互模拟概念的本质,为其在形式化分析及验证技术中的应用提供了基础。 展开更多

关键词 系统行为 等价 标号迁移系统 模拟 互模拟

下载PDF 职称材料

航空软件模型状态最小化算法的比较

18

作者 杜文杰 雷国庆 《金融管理研究》 2020年第2期133-142,共10页

标号迁移系统是对航空软件操作行为建模的重要手段。当软件规模很大时,对应的标号迁移系统变得非常庞大,需要对其状态空间进行压缩。本文分别实现了由Valmari和Schtzle等人提出的两种互模拟压缩算法,并将其应用于互模拟压缩问题中,比较... 标号迁移系统是对航空软件操作行为建模的重要手段。当软件规模很大时,对应的标号迁移系统变得非常庞大,需要对其状态空间进行压缩。本文分别实现了由Valmari和Schtzle等人提出的两种互模拟压缩算法,并将其应用于互模拟压缩问题中,比较了两种算法的运行效果。根据实验数据可知,在PC平台上处理百万级规模以内的标号迁移系统最好选择基于内存的Valmari算法,在服务器的数据库中处理超大规模迁移系统时应选择基于外存的Schtzle算法。 展开更多

关键词 标号迁移系统 互模拟压缩 算法

原文传递

非确定性系统的动态测试过程

19

作者 刘咏梅 叶新铭 +1 位作者 周建涛 赵玉兰 《内蒙古大学学报（自然科学版）》 CAS CSCD 1999年第2期247-253,共7页

针对非确定性系统，提出一种新的相容性测试方法．即扩展〔１〕中所提出的对确定的有限状态机进行动态测试的方法，使之可应用于非确定的带标记转换系统．与以往方法相比，该方法可获得更符合实际的测试结果．

关键词 相容性测试 测试序列树 非确定性系统 动态测试

下载PDF 职称材料

余代数上的弱不变量

20

作者 曹学磊 何伟 +1 位作者 樊磊 庞智恒 《中央民族大学学报（自然科学版）》 2007年第4期304-309,共6页

余代数上的不变量在理论计算机科学中占有十分重要的地位,本文借助文献[1]的思想建立弱不变量的定义,讨论了弱不变量的性质以及与不变量的关系;其次,定义标记迁移系统的弱不变量并证明这两种定义是等价的.

关键词 余代数 标记迁移系统 不变量 弱不变量

下载PDF 职称材料