期刊文献+
共找到60篇文章
< 1 2 3 >
每页显示 20 50 100
Approximate Failures Semantics for Polynomial Labelled Transition Systems 被引量:1
1
《Journal of Donghua University(English Edition)》 EI CAS 2013年第6期472-476,共5页
Labelled transition systems(LTSs) are widely used to formally describe system behaviour.The labels of LTS are extended to offer a more satisfactory description of behaviour by refining the abstract labels into multiva... Labelled transition systems(LTSs) are widely used to formally describe system behaviour.The labels of LTS are extended to offer a more satisfactory description of behaviour by refining the abstract labels into multivariate polynomials.These labels can be simplified by numerous numerical approximation methods.Those LTSs that can not apply failures semantics equivalence in description and verification may have a chance after using approximation on labels.The technique that combines approximation and failures semantics equivalence effectively alleviates the computational complexity and minimizes LTS. 展开更多
关键词 多项式系统 语义 标记 多元多项式 描述系统 逼近方法 lts 标签
下载PDF
LTS仿真模型组合验证方法 被引量:1
2
作者 冯晓宁 王卓 王金娜 《哈尔滨工程大学学报》 EI CAS CSCD 北大核心 2014年第5期589-593,618,共6页
为提高复杂仿真系统的开发效率和降低开发成本,提出了基于标签转移系统LTS的仿真模型组合验证方法。该方法在组合仿真模型的行为表示中引入时间因素,并将执行序列表示为LTS,通过将表示组合仿真模型行为的LTS进行比较,得出组合仿真模型... 为提高复杂仿真系统的开发效率和降低开发成本,提出了基于标签转移系统LTS的仿真模型组合验证方法。该方法在组合仿真模型的行为表示中引入时间因素,并将执行序列表示为LTS,通过将表示组合仿真模型行为的LTS进行比较,得出组合仿真模型的有效性。最后给出了作战坦克修理所实例,结果表明,该方法能够有效验证仿真模型可组合问题。 展开更多
关键词 仿真模型组合 标签转移系统 语义相似度
下载PDF
体系结构层状态型方面的建模和编织——基于LTS的方法 被引量:1
3
作者 杨春花 王海洋 《计算机学报》 EI CSCD 北大核心 2011年第2期342-352,共11页
状态型方面是一种封装反应式关注点的方面,它需要专门的切点机制来跟踪系统的执行历史.然而当前在体系结构层还缺乏支持状态型方面建模的有效机制.针对这一问题,提出一种体系结构层状态型方面的建模和编织方法.它以标记转换系统(Labelle... 状态型方面是一种封装反应式关注点的方面,它需要专门的切点机制来跟踪系统的执行历史.然而当前在体系结构层还缺乏支持状态型方面建模的有效机制.针对这一问题,提出一种体系结构层状态型方面的建模和编织方法.它以标记转换系统(Labelled Transition System,LTS)为底层形式化,建立了用于识别系统运行轨迹中特定模式的切点机制,并定义了支持多种通知类型的编织运算.该方法当前已在一个基于FSP规范的原型编织工具上实现,并用一个实例说明了该方法的有效性. 展开更多
关键词 方面 状态型方面 编织 标记转换系统 面向方面的软件开发
下载PDF
基于LTS的Statecharts操作语义研究
4
作者 钱俊彦 赵岭忠 《计算机工程》 EI CAS CSCD 北大核心 2006年第22期43-45,共3页
Statecharts是一种用于复杂反应式系统行为的可视化规格语言。该文提出了一种基于标签变迁系统(LTS)的Statecharts操作语义描述方法,介绍了Statecharts及其项语法和一步语义,并基于进程代数描述Statecharts的并发行为,使用结构化的操作... Statecharts是一种用于复杂反应式系统行为的可视化规格语言。该文提出了一种基于标签变迁系统(LTS)的Statecharts操作语义描述方法,介绍了Statecharts及其项语法和一步语义,并基于进程代数描述Statecharts的并发行为,使用结构化的操作语义SOS规则描述Statecharts的组合语义,从而得到相应的LTS。 展开更多
关键词 STATECHARTS 操作语义 标签变迁系统
下载PDF
基于LTS图的构件规约匹配
5
作者 林雪云 《福建工程学院学报》 CAS 2009年第6期672-676,共5页
构件重用是缩减软件设计周期和提高软件可靠性的有效方法。基于构件的软件开发(CBSD)主要花费在于构件的检索和修改,而匹配过程则是关键。文章提出一个基于LTS图模型(Labeled Transition System)的形式化构件匹配方法,此方法将构件匹配... 构件重用是缩减软件设计周期和提高软件可靠性的有效方法。基于构件的软件开发(CBSD)主要花费在于构件的检索和修改,而匹配过程则是关键。文章提出一个基于LTS图模型(Labeled Transition System)的形式化构件匹配方法,此方法将构件匹配分为结构匹配和功能匹配两部份。结构匹配过程通过树的同构匹配完成,用于检查构件的可调整性;功能匹配则通过S-Forced模拟完成,用于确保得到适当的功能。 展开更多
关键词 lts ltstree ltsforest S-forcedsimulation ltsgraphmatching
下载PDF
逻辑LTS预备模拟关系的判定算法
6
作者 朱文涛 《计算机工程与应用》 CSCD 北大核心 2016年第17期41-48,共8页
进程代数与时序逻辑是并发理论中应用最为广泛的两大规范系统。近来,Gerald Luttgen等人将二者进行结合,提出了逻辑标记转换系统以及相应的精化关系——LLTS预备模拟。提出了一种LLTS预备模拟关系的等价描述方式——泛化预备模拟,并从... 进程代数与时序逻辑是并发理论中应用最为广泛的两大规范系统。近来,Gerald Luttgen等人将二者进行结合,提出了逻辑标记转换系统以及相应的精化关系——LLTS预备模拟。提出了一种LLTS预备模拟关系的等价描述方式——泛化预备模拟,并从划分对的角度出发,给出与该描述等价的稳定划分对概念。基于这一概念给出一种判定两个逻辑标记转换系统之间是否具有LLTS预备模拟关系的理论算法,并证明其正确性。 展开更多
关键词 逻辑标记转换系统 预备模拟 划分对 稳定性 判定算法
下载PDF
一种云平台可信性分析模型建立方法 被引量:22
7
作者 赵波 戴忠华 +1 位作者 向騻 陶威 《软件学报》 EI CSCD 北大核心 2016年第6期1349-1365,共17页
如何使得用户信任云服务提供商及其云平台,是云计算普及的关键因素之一.针对目前云平台可信性所包含的内容与分析评价依据尚不完善的现状,且缺乏从理论层次对于云平台的部分可信属性进行分析与评估方法的问题,首先对云平台的可信性进行... 如何使得用户信任云服务提供商及其云平台,是云计算普及的关键因素之一.针对目前云平台可信性所包含的内容与分析评价依据尚不完善的现状,且缺乏从理论层次对于云平台的部分可信属性进行分析与评估方法的问题,首先对云平台的可信性进行定义,并结合国内外相关云安全标准与可信性规范以及作者的理解,明确了云平台可信性的子属性与具体分析内容,从而明确了所提出模型的适用范围、分析目的以及依据.在此基础上,提出模型建立方法.该方法以标记变迁系统作为操作语义描述工具,从云平台内部组件交互过程出发,将平台对外提供服务过程刻画为用户与云的交互以及云平台内部实体间的交互,并利用模型分析检测工具Kronos从可用、可靠、安全等多个角度对平台内部状态变化过程进行分析.分析结果不但能够发现已知的可信性问题,还发现了一些未知的隐患,说明了模型建立方法的有效性,并为如何评价云平台的可信性,进而构建可信云提供了理论支撑. 展开更多
关键词 云平台 可信性分析 平台建模 标记变迁系统 KRONOS
下载PDF
基于标记变迁系统的可信计算平台信任链测试 被引量:19
8
作者 徐明迪 张焕国 严飞 《计算机学报》 EI CSCD 北大核心 2009年第4期635-645,共11页
可信计算是当今世界信息安全领域的重要潮流之一.根据国家有关规定,信息安全产品需要经过测评认证,但目前国内外对可信计算测试的理论与技术研究还非常不完善,也无相应测试工具或系统,这必然影响可信计算的发展.该文着眼于规范定义的信... 可信计算是当今世界信息安全领域的重要潮流之一.根据国家有关规定,信息安全产品需要经过测评认证,但目前国内外对可信计算测试的理论与技术研究还非常不完善,也无相应测试工具或系统,这必然影响可信计算的发展.该文着眼于规范定义的信任链行为特征,以进程代数作为指称语义描述工具,以标记变迁系统作为操作语义,对规范定义的信任链行为特征进行了形式化描述,提出了一种基于标记变迁系统的信任链测试模型框架.针对信任链规范与实现之间的问题,从易测性出发对测试集进行了有效约简;并论证了信任链的规范实现与规范说明之间的关系,为测试用例构造方法提供了理论依据,从而解决了信任链测试这一难题. 展开更多
关键词 可信计算平台 信任链 进程代数 标记变迁系统 一致性测试
下载PDF
UML状态机的形式语义 被引量:25
9
作者 蒋慧 谢希仁 林东 《软件学报》 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
嵌入式API测试套生成方法和技术 被引量:2
10
作者 赵会群 孙晶 +1 位作者 张爆 王同林 《软件学报》 EI CSCD 北大核心 2014年第2期373-385,共13页
随着嵌入式计算机系统应用的不断扩展,嵌入式系统的可靠性引起了学术界和工业界的广泛关注,也提出了很多增进可靠性的方法和技术.然而,现有的方法和技术在测试套生成方面论述不多,所以在处理大批量嵌入式系统测试工作中遇到了挑战.讨论... 随着嵌入式计算机系统应用的不断扩展,嵌入式系统的可靠性引起了学术界和工业界的广泛关注,也提出了很多增进可靠性的方法和技术.然而,现有的方法和技术在测试套生成方面论述不多,所以在处理大批量嵌入式系统测试工作中遇到了挑战.讨论抽象测试套生成方法和适配技术,提出了LTS(labeled transition system)到BT(behavior tree)的转换算法,从而使TTCN(test and testing control notation)测试套可以通过转换嵌入式软件的LTS描述产生.还介绍了基于上述转换算法的嵌入式软件测试工具包,以及一个嵌入式物联网识读器测试案例研究. 展开更多
关键词 嵌入式软件 软件测试 测试与测试控制语言 标签转换系统
下载PDF
互模拟的一些基本性质 被引量:8
11
作者 李娜 姚从军 《云南师范大学学报(哲学社会科学版)》 CSSCI 2010年第5期68-73,共6页
由于互模拟的概念几乎同时在计算机科学、模态逻辑和集合论中产生,本文试图给出一种能够刻画计算机科学、模态逻辑和集合论中互模拟概念的统一定义。因此,本文首先简单介绍互模拟产生的原因及作用;其次,给出两个加标转换系统之间的互模... 由于互模拟的概念几乎同时在计算机科学、模态逻辑和集合论中产生,本文试图给出一种能够刻画计算机科学、模态逻辑和集合论中互模拟概念的统一定义。因此,本文首先简单介绍互模拟产生的原因及作用;其次,给出两个加标转换系统之间的互模拟定义,并说明由此定义如何得到计算机科学中、模态逻辑中以及集合论中互模拟的定义;最后证明在这种定义下,互模拟的一些基本性质。 展开更多
关键词 关系结构 加标转换系统 互模拟
下载PDF
一种基于时间自动机的实时系统测试方法 被引量:14
12
作者 陈伟 薛云志 +1 位作者 赵琛 李明树 《软件学报》 EI CSCD 北大核心 2007年第1期62-73,共12页
基于时间自动机(timedautomata,简称TA)的一种变体——时间安全输入/输出自动机(timedsafetyinput/outputautomata,简称TSIOA),提出了一种实时系统测试方法.该方法首先将时间安全输入/输出自动机描述的系统模型转换为不含抽象时间延迟... 基于时间自动机(timedautomata,简称TA)的一种变体——时间安全输入/输出自动机(timedsafetyinput/outputautomata,简称TSIOA),提出了一种实时系统测试方法.该方法首先将时间安全输入/输出自动机描述的系统模型转换为不含抽象时间延迟迁移的稳定符号状态迁移图(untimedstabletransitiongraphofsymbolicstate,简称USTGSS);然后采用基于标号迁移系统(labeledtransitionsystem,简称LTS)的测试方法来静态生成满足各种结构覆盖标准的包含时间延迟变量迁移动作序列;最后,给出了一个根据迁移动作序列构造和执行测试用例的过程,该过程引入了时间延迟变量目标函数,并采用线性约束求解方法动态求解迁移动作序列中的时间延迟变量. 展开更多
关键词 时间安全输入/输出自动机 实时系统测试 最简稳定符号状态迁移图 测试用例生成
下载PDF
一种形式化的协议互操作性测试方法 被引量:6
13
作者 郝瑞兵 吴建平 《计算机学报》 EI CSCD 北大核心 1997年第4期350-359,共10页
对协议实现的互操作性测试是保证网络产品之间互通的一种重要手段.在本文中我们提出了一种基于并发TTCN操作语义的互操作性测试系统的构造方法.并发TTCN是一种能够处理并发测试行为描述的语言,我们通过使用标号变迁系统形式... 对协议实现的互操作性测试是保证网络产品之间互通的一种重要手段.在本文中我们提出了一种基于并发TTCN操作语义的互操作性测试系统的构造方法.并发TTCN是一种能够处理并发测试行为描述的语言,我们通过使用标号变迁系统形式化地定义了它的操作语义,并描述了基于这种语言的操作语义的互操作性测试系统的测试执行和测试判决过程.我们认为这种方法对研究形式化的协议互操作性测试理论是很有帮助的. 展开更多
关键词 协议互操作性测试 协议一致性测试 标号变迁系统
下载PDF
基于标号变迁系统的测试集自动生成 被引量:6
14
作者 蒋凡 宁华中 《计算机研究与发展》 EI CSCD 北大核心 2001年第12期1435-1445,共11页
首先 ,依照 ISO 96 46的定义 ,阐述了协议一致性测试的基本概念 .然后 ,介绍标号变迁系统 (L TS)的形式化理论的定义和基本性质 ,利用 L TS,给出测试例、测试集以及测试生成的形式化定义 .第 3,表述了实现关系在测试生成中的地位和作用 ... 首先 ,依照 ISO 96 46的定义 ,阐述了协议一致性测试的基本概念 .然后 ,介绍标号变迁系统 (L TS)的形式化理论的定义和基本性质 ,利用 L TS,给出测试例、测试集以及测试生成的形式化定义 .第 3,表述了实现关系在测试生成中的地位和作用 ,定义了输入输出系统 ,并在输入输出系统以及Δ变换的基础上引入实现关系 ioco.根据实现关系 ioco给出了一个测试集自动生成算法 .该算法能很好地适用于递归的 L TS. 展开更多
关键词 标号变迁系统 形式化方法 有限状态机 测试集 自动生成 网络协议 ISO9646
下载PDF
软件组件组装行为兼容性检查研究 被引量:1
15
作者 张驰 褚楚 《计算机工程与应用》 CSCD 北大核心 2016年第11期30-33,共4页
在开放环境下,仅包含了语法层信息的组件接口不足以刻画组件交互的行为信息,从而不能对组装后的系统进行兼容性验证。提出了既包含组件接口调用方法又包含内部逻辑行为的组件视图,采用LTS表示组件行为协议,将组件交互过程表示为多个LTS... 在开放环境下,仅包含了语法层信息的组件接口不足以刻画组件交互的行为信息,从而不能对组装后的系统进行兼容性验证。提出了既包含组件接口调用方法又包含内部逻辑行为的组件视图,采用LTS表示组件行为协议,将组件交互过程表示为多个LTS之间的同步变迁;借助LTS操作语义,通过LTS同步积模拟组合系统交互的动态行为,以此为基础,检查同步积中是否出现死锁状态来进行兼容性判定,并设计了判定算法以实现兼容性的自动判定,通过一个典型的电子商务应用检验该方法的有效性。 展开更多
关键词 接口 组件视图 行为兼容性 标签转换系统(lts)
下载PDF
基于动作序列的行为需求模式验证的研究 被引量:2
16
作者 杜军威 徐中伟 江峰 《通信学报》 EI CSCD 北大核心 2011年第1期94-105,共12页
提出了基于动作序列刻画安全关键系统的功能行为需求和安全性行为需求,较传统的类逻辑规范和类图式规范更准确表达交互行为间的时序关系。基于动作序列构造功能需求和安全需求两类行为模式,并给出每个模式的操作语义。为实现基于行为模... 提出了基于动作序列刻画安全关键系统的功能行为需求和安全性行为需求,较传统的类逻辑规范和类图式规范更准确表达交互行为间的时序关系。基于动作序列构造功能需求和安全需求两类行为模式,并给出每个模式的操作语义。为实现基于行为模式的需求验证,重新定义LTS安全性和活性的属性表达、组合操作,给出并证明功能需求模式和安全性需求模式满足的充要条件。该框架在高速铁路CTCS2/3的形式验证与确认得到了广泛应用,对指导构件化安全关键系统的组合形式验证具有较高的理论与实践价值。 展开更多
关键词 安全关键系统 动作序列 行为需求模式 标签变迁系统 模式验证
下载PDF
解决变化问题的自底向上流程建模方法 被引量:4
17
作者 严志民 徐玮 《计算机集成制造系统》 EI CSCD 北大核心 2011年第8期1595-1602,共8页
为使工作流适应业务快速发展而复杂多变的特点,提出一种全新的以数据为中心的业务流程定义和业务流程建模的说明性业务流程建模方法。以自底向上机制分析解剖业务流程,提取出原子工单、活动和业务策略等,将业务要素和业务变化的描述分... 为使工作流适应业务快速发展而复杂多变的特点,提出一种全新的以数据为中心的业务流程定义和业务流程建模的说明性业务流程建模方法。以自底向上机制分析解剖业务流程,提取出原子工单、活动和业务策略等,将业务要素和业务变化的描述分离成不同的层次。执行语义上,以数据中心的业务流程建模的说明性业务流程建模方法借助有限状态自动机来描述单个工单的生命周期,利用标号迁移系统来描述工作流及多个工单间的交互。此外,还进行了从以数据中心的业务流程建模的说明性业务流程建模方法到实现可部署工作流的探讨,并结合杭州市房产管理局的实际工作流程,阐述了该方法的实际应用。 展开更多
关键词 自底向上机制 工单 业务流程建模 有限状态自动机 标号迁移系统 工作流
下载PDF
标记迁移系统的组合可达性分析 被引量:2
18
作者 文艳军 王戟 齐治昌 《计算机科学》 CSCD 北大核心 2005年第12期110-111,145,共3页
标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描... 标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描述和精确表达。本文对其基本原理进行了分析和概括,并作了形式化陈述,证明了相关结论。本文的工作有助于深入理解和澄清组合可达性分析的内部工作机制。 展开更多
关键词 标记迁移系统 计算机辅助设计和验证 组合可达性分析 状态空间爆炸问题 观察等价
下载PDF
一种标记转移系统的构造与执行方法 被引量:1
19
作者 张冠华 张连华 白英彩 《计算机应用与软件》 CSCD 北大核心 2006年第5期84-85,95,共3页
本文提出了一种基于动态树的标记转移系统的构造与执行方法,其具有以下几个显著特点:一是树形结构可以层次清楚地表示标记转移系统并可方便地利用树的遍历算法执行系统;二是通过树的动态生成解决了进程代数的状态递归和回溯的问题;三是... 本文提出了一种基于动态树的标记转移系统的构造与执行方法,其具有以下几个显著特点:一是树形结构可以层次清楚地表示标记转移系统并可方便地利用树的遍历算法执行系统;二是通过树的动态生成解决了进程代数的状态递归和回溯的问题;三是标记转移系统的执行只和当前的动态树相关,降低了执行的复杂度。 展开更多
关键词 进程代数 标记转移系统 动态树
下载PDF
一种软件体系结构级测试序列生成技术 被引量:1
20
作者 徐士华 吕莉媛 赵磊 《微电子学与计算机》 CSCD 北大核心 2012年第1期117-120,共4页
软件体系结构(software architecture,SA)通过对系统构件及其交互的抽象,提供了一个描述大型、复杂系统的高层次模型,软件体系结构的动态描述常被用来指导分析和测试.本文通过CHAM(chemical abstract ma-chine,CHAM)描述的SA规格说明生... 软件体系结构(software architecture,SA)通过对系统构件及其交互的抽象,提供了一个描述大型、复杂系统的高层次模型,软件体系结构的动态描述常被用来指导分析和测试.本文通过CHAM(chemical abstract ma-chine,CHAM)描述的SA规格说明生成LTS,并根据测试需求进行测试功能的选取,提出了基于功能的最小LTS图(M-LTS)生成方法,根据McCabe覆盖方法生成M-LTS图的测试路径.最后以B/S结构为例,验证了该方法在生成SA级的测试路径上是可行的. 展开更多
关键词 软件体系结构 软件测试 标号迁移系统 测试序列
下载PDF
上一页 1 2 3 下一页 到第
使用帮助 返回顶部