期刊文献+
共找到25篇文章
< 1 2 >
每页显示 20 50 100
Test Selection on Extended Finite State Machines with Provable Guarantees
1
作者 Bo Guo Mahadevan Subramaniam 《Journal of Software Engineering and Applications》 2013年第9期500-510,共11页
Building high confidence regression test suites to validate new system versions is a challenging problem. A modelbased approach to build a regression test suite from a given test suite is described. The generated test... Building high confidence regression test suites to validate new system versions is a challenging problem. A modelbased approach to build a regression test suite from a given test suite is described. The generated test suite includes every test that will traverse a change performed to produce the new version, and consists of only such tests to reduce the testing costs. Finite state machines extended with typed variables (EFSMs) are used to model systems and system changes are mapped to EFSM transition changes adding/deleting/replacing EFSM transitions and states. Tests are a sequence of input and expected output messages with concrete parameter values over the supported data types. An invariant is formulated to characterize tests whose runtime behavior can be accurately predicted by analyzing their descriptions along with the model. Incremental procedures to efficiently evaluate the invariant and to select tests for regression are developed. Overlaps among the test descriptions are exploited to extend the approach to simultaneously select multiple tests to reduce the test selection costs. Effectiveness of the approach is demonstrated by applying it to several protocols, Web services, and model programs extracted from a popular testing benchmark. Our experimental results show that the proposed approach is economical for regression test selection in all these examples. For all these examples, the proposed approach is able to identify all tests exercising changes more efficiently than brute-force symbolic evaluation. 展开更多
关键词 FORMAL Methods MODEL-BASED Software TESTING Regression TESTING Extended finite state machineS
下载PDF
Aspect-Oriented Modeling and Verification with Finite State Machines
2
作者 徐殿祥 Omar El-Ariss +1 位作者 许巍峰 王林章 《Journal of Computer Science & Technology》 SCIE EI CSCD 2009年第5期949-961,共13页
Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties... Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties and even destroys the conceptual integrity of programs. To assure the quality of an aspect-oriented system, rigorous analysis and design of aspects are highly desirable. In this paper, we present an approach to aspect-oriented modeling and verification with finite state machines. Our approach provides explicit notations (e.g., pointcut, advice and aspect) for capturing crosscutting concerns and incremental modification requirements with respect to class state models. For verification purposes, we compose the aspect models and class models in an aspect-oriented model through a weaving mechanism. Then we transform the woven models and the class models not affected by the aspects into FSP (Finite State Processes), which are to be checked by the LTSA (Labeled Transition System Analyzer) model checker against the desired system properties. We have applied our approach to the modeling and verification of three aspect-oriented systems. To further evaluate the effectiveness of verification, we created a large number of flawed aspect models and verified them against the system requirements. The results show that the verification has revealed all flawed models. This indicates that our approach is effective in quality assurance of aspect-oriented state models. As such, our approach can be used for model-checking state-based specification of aspect-oriented design and can uncover some system design problems before the system is implemented. 展开更多
关键词 aspect-oriented modeling finite state machines MODELING VERIFICATION model checking
原文传递
基于Isabelle/HOL的文件系统形式化设计与验证
3
作者 王文斌 钱振江 +4 位作者 靳勇 孙高飞 邢晓双 苏超 孙天琦 《计算机工程》 CAS CSCD 北大核心 2024年第4期277-285,共9页
对于构建可信操作系统而言,文件系统设计和实现的正确性至关重要,即使是已经得到广泛运用的文件系统仍然有漏洞被检测出来。采用形式化方法对文件系统的设计和实现的正确性进行严格的验证是公认的可行方法。当前文件系统的形式化验证工... 对于构建可信操作系统而言,文件系统设计和实现的正确性至关重要,即使是已经得到广泛运用的文件系统仍然有漏洞被检测出来。采用形式化方法对文件系统的设计和实现的正确性进行严格的验证是公认的可行方法。当前文件系统的形式化验证工作大多基于宏内核操作系统,而忽视了微内核操作系统架构下文件系统的验证。为此,提出一种微内核架构下采用内联数据机制的文件系统的形式化设计和验证方法。以高阶逻辑(HOL)和自动机模型为基础,将文件系统中的工作对象和系统资源抽象为系统对象来构建文件系统的工作状态,形式化地描述文件系统的相关系统调用的功能语义,将系统调用提供服务的过程抽象为系统工作状态发生跃迁的过程,并给出文件系统功能正确性和安全属性的断言。以实现的安全可信微内核操作系统(VSOS)中的安全可信文件系统(VSFS)为例,在设计阶段构建VSFS的有限状态机模型,并在Isabelle/HOL中抽象描述VSFS的可移植操作系统接口(POSIX)系统调用,分析和归纳出VSFS文件系统正确性断言,使用定理证明的方式来验证VSFS的正确性。实验结果表明,该方法在Isabella/HOL中完成VSFS有限状态机模型细粒度的形式化验证,满足预期的安全需求规范。 展开更多
关键词 形式化验证 文件系统 定理证明 有限状态机 微内核
下载PDF
Statechart规格语言的语法分析研究 被引量:2
4
作者 钱俊彦 蔡国永 +1 位作者 古天龙 庞健雄 《桂林电子工业学院学报》 1999年第3期12-17,共6页
Statechart是一种用以规约复杂反应式系统行为的可视化语言。它在一些方面上扩展了典型的状态转移图,保留甚至发挥了可视化要求。实际上, Statechart 满足层次的描述,包括高层和低层事件,更显著地是采用广播... Statechart是一种用以规约复杂反应式系统行为的可视化语言。它在一些方面上扩展了典型的状态转移图,保留甚至发挥了可视化要求。实际上, Statechart 满足层次的描述,包括高层和低层事件,更显著地是采用广播通信机制产生连锁反应而引起多层并发。通过对 Statechart语言进行了分析研究后给出了其形式化文法表示。在此基础上,讨论了 Statechart规格语言语法正确性分析的问题。 展开更多
关键词 有限状态机 stateCHART 形式化方法 可视化语言
下载PDF
面向语用的仿真组件形式化建模及组合技术研究 被引量:3
5
作者 胡鹏 沈建京 吴善明 《计算机应用研究》 CSCD 北大核心 2015年第9期2697-2701,共5页
语法和语义层次的组合并不足以保证仿真组件组合的完整性、有效性和实用性,在语用组合问题分析的基础上,提出了基于扩展有限状态自动机的仿真组件模型形式化描述,包含了仿真组件行为语义和仿真运行语境约束信息,并在此基础上设计了基于... 语法和语义层次的组合并不足以保证仿真组件组合的完整性、有效性和实用性,在语用组合问题分析的基础上,提出了基于扩展有限状态自动机的仿真组件模型形式化描述,包含了仿真组件行为语义和仿真运行语境约束信息,并在此基础上设计了基于XML的仿真组件模型描述规范。最后,通过应用实例具体描述了面向语用组合的仿真组件模型组合过程。组合中考虑了模型发现、组合判定、仿真运行与仿真语境之间的关系,并且实现了面向语用的仿真系统自动化动态构建。 展开更多
关键词 语用 组合 仿真组件 形式化建模 扩展有限状态自动机
下载PDF
形式验证中同步时序电路的VHDL描述到S^2-FSM的转换 被引量:3
6
作者 贝劲松 李洪星 +2 位作者 边计年 薛宏熙 洪先龙 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 1999年第3期196-199,共4页
符号模型检查(SymbolicModelChecking,SMC)是一种有效的形式验证方法.该方法主要有2个难点:一个是建模,即如何建立并用有限内存来表示电路的状态机模型;另一个是在此模型基础上的验证算法.由于验证时... 符号模型检查(SymbolicModelChecking,SMC)是一种有效的形式验证方法.该方法主要有2个难点:一个是建模,即如何建立并用有限内存来表示电路的状态机模型;另一个是在此模型基础上的验证算法.由于验证时间和有限状态机模型的大小是直接相关的,因而模型的大小就成为SMC中的关键问题.本文提出一种基于同步电路行为描述的新的有限状态机模型S2-FSM,并给出从同步电路的VHDL描述建立这种模型的过程.由于该模型的状态转换函数是基于时钟周期的,消去了与时钟无关的大量中间变量,所以同Deharbe提出的模型相比,它的状态数大大减少.若干电路的实验结果表明,该模型由于减少了状态规模,建模时间和可达性分析时间大大减少,效果十分显著. 展开更多
关键词 形式验证 VHDL S^2-FSM 同步时序电路
下载PDF
基于标号变迁系统的测试集自动生成 被引量:6
7
作者 蒋凡 宁华中 《计算机研究与发展》 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
参数化运行时验证研究和工具实现 被引量:2
8
作者 王哲民 陈哲 +1 位作者 朱云龙 黄志球 《小型微型计算机系统》 CSCD 北大核心 2016年第12期2667-2672,共6页
随着软件规模的不断增大,如何保证软件的可靠性和安全性成为学术界和工业界越来越关注的问题.运行时验证是一种新型的程序自动验证技术,弥补了静态分析和模型检测等常用方法的缺点.设计一种针对C程序的监控器规约语言,用于描述针对C程... 随着软件规模的不断增大,如何保证软件的可靠性和安全性成为学术界和工业界越来越关注的问题.运行时验证是一种新型的程序自动验证技术,弥补了静态分析和模型检测等常用方法的缺点.设计一种针对C程序的监控器规约语言,用于描述针对C程序的形式化规约.该语言支持基于有限状态自动机和正则表达式的参数化运行时验证.本文借助开源工具flex和bison实现了支持该语言的参数化运行时验证工具M OVEC.为了对运行时产生的大量监控器进行索引,我们提出并实现了一种层次哈希森林的数据结构.实验证明该工具是可行且高效的. 展开更多
关键词 运行时验证 形式化规约 层次哈希森林 有限状态自动机
下载PDF
协议一致性测试用例生成模型研究 被引量:2
9
作者 齐建业 李强 余祥 《计算机工程与设计》 CSCD 北大核心 2014年第3期1110-1114,F0003,共6页
为设计并生成有效的测试用例,通过测试用例的自动生成,提高了设计和执行测试用例的效率。建立了协议一致性测试用例生成模型,由形式活动图、扩展有限状态机和相关的转换算法组成。在定义形式活动图和扩展有限状态机概念的基础上,设计了... 为设计并生成有效的测试用例,通过测试用例的自动生成,提高了设计和执行测试用例的效率。建立了协议一致性测试用例生成模型,由形式活动图、扩展有限状态机和相关的转换算法组成。在定义形式活动图和扩展有限状态机概念的基础上,设计了从形式活动图生成扩展有限状态机的算法和从扩展有限状态机自动生成测试用例的算法。对算法进行了分析与比较,分析结果表明,该算法在测试序列的长度、错误覆盖度等方面具有一定的优越性。 展开更多
关键词 协议测试 一致性测试 测试用例 形式活动图 扩展有限状态机
下载PDF
关于通信协议测试生成形式方法的探讨 被引量:2
10
作者 刘积仁 都军 《东北大学学报(自然科学版)》 EI CAS CSCD 1995年第2期165-170,共6页
结合作者最近提出的基于UIO序列的形式叠加测试方法,通过一个实例讨论了基于FSM的5种主要的测试生成形式方法,它们分别是:UIO方法、SUIO方法、MUIO方法、叠加方法和形式叠加方法.并且,针对以上五种方法分别给出... 结合作者最近提出的基于UIO序列的形式叠加测试方法,通过一个实例讨论了基于FSM的5种主要的测试生成形式方法,它们分别是:UIO方法、SUIO方法、MUIO方法、叠加方法和形式叠加方法.并且,针对以上五种方法分别给出各自生成的测试序列的长度的上界. 展开更多
关键词 形式方法 测试序列 计算机通信 通信协议
下载PDF
基于监控理论的EFSM设计方法 被引量:1
11
作者 王向云 赵雷 蔡开元 《计算机工程与应用》 CSCD 北大核心 2009年第6期20-24,81,共6页
随着扩展有限状态机(EFSM)模型在计算机科学和工程领域的广泛应用,EFSM的设计逐渐成为一个重要的问题。目前EFSM的设计仍然主要依赖于个人经验,缺乏理论基础。由于EFSM中每个转移的谓词可以看作此转移的一个监控器,所以可以用离散事件... 随着扩展有限状态机(EFSM)模型在计算机科学和工程领域的广泛应用,EFSM的设计逐渐成为一个重要的问题。目前EFSM的设计仍然主要依赖于个人经验,缺乏理论基础。由于EFSM中每个转移的谓词可以看作此转移的一个监控器,所以可以用离散事件系统的监控理论为EFSM设计提供理论基础。首先定义了有限状态机(FSM)导出的EFSM及其产生的语言。然后,基于监控理论中的受控对象和监控器,提出了一种设计EFSM的方法,用离散事件系统监控理论为EFSM设计提供理论依据。最后用两个实际例子说明了提出方法的可用性和有用性。 展开更多
关键词 形式化方法 软件控制论 离散事件系统 扩展有限状态机(EFSM) 有限状态机(FSM)
下载PDF
一种n个通信有限状态机的交互式生成法 被引量:3
12
作者 张尧学 乔松 《计算机学报》 EI CSCD 北大核心 1994年第4期264-269,共6页
通信有限状态机(CFSM)是一种直观、易懂且描述能力较强的形式描述工具.它被广泛地用于协议的形式描述、验证及测试、协议变换等.但是,由于描述对象的复杂性和缺少适当的支援工具,CFSM的产生一般依靠手工完成.这除了描述... 通信有限状态机(CFSM)是一种直观、易懂且描述能力较强的形式描述工具.它被广泛地用于协议的形式描述、验证及测试、协议变换等.但是,由于描述对象的复杂性和缺少适当的支援工具,CFSM的产生一般依靠手工完成.这除了描述效率低之外,更重要的是所产生的CFSM的性能取决于描述人员的习惯、经验、能力等.本文提出一种由协议文本交互式地产生n个CFSM的生成方法.使用该方法,描述人员可得到n个不包含常见逻辑错误的互相传递消息的CFSM.该方法可用于计算机网络及分布式系统中的协议设计和开发. 展开更多
关键词 通信协议 CFSM 形式描述
下载PDF
基于NS2软件验证随机早期检测算法RED的优越性 被引量:1
13
作者 孙栋栋 王玉斌 +1 位作者 马争先 张净 《广西科学院学报》 2010年第4期426-428,共3页
在构造RED算法的网络拓扑模型和建立该模型的有限状态机的基础上,用目前主流的网络模拟软件NS2进行仿真,得到当前队列大小、平均队列大小和TCP数据源窗口大小的仿真图形,通过对仿真图形的比较和分析,说明RED算法的高效性和优越性。
关键词 队列管理 RED 形式化 有限状态机 NS2
下载PDF
映射ELOTOS到基于FSM的性能估价模型
14
作者 罗铁庚 陈火旺 +1 位作者 龚正虎 齐治昌 《软件学报》 EI CSCD 北大核心 1997年第10期788-792,共5页
ELOTOS是协议描述规范语言LOTOS的扩展.本文用标号转换系统LTS(labeledtransitionsystem)给出了ELOTOS的语义.然后,通过对LTS进行踪迹等价住分析,将ELOTOS映射到基于有穷状态机FSM(finitestatemachine)的性能估价模型.
关键词 ELOTOS FSM 性能模型 网络协议 计算机网络
下载PDF
N个有限状态机的死锁和死环回避算法
15
作者 张尧学 《计算机学报》 EI CSCD 北大核心 1994年第A00期53-58,共6页
死锁和死环是分布式系统或计算机网络中进程间通信时经常发生的逻辑错误.它们往往造成分布式系统中的部分主机或整个系统瘫痪.本文提出两个回避死锁和死环的算法.这些算法可被用来设计分布式系统的通信协议,从而提高分布式系统的可... 死锁和死环是分布式系统或计算机网络中进程间通信时经常发生的逻辑错误.它们往往造成分布式系统中的部分主机或整个系统瘫痪.本文提出两个回避死锁和死环的算法.这些算法可被用来设计分布式系统的通信协议,从而提高分布式系统的可靠性和减少协议开发成本. 展开更多
关键词 死锁 死环 有限状态机 回避算法
下载PDF
基于有限状态机的操作系统需求层形式化验证 被引量:8
16
作者 张锦坤 杨孟飞 +2 位作者 乔磊 杨桦 刘波 《空间控制技术与应用》 CSCD 北大核心 2019年第2期48-55,共8页
操作系统是航天器必备的基本软件,操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障,但仍存在不能完全排除缺陷的情况,因此对空间操作系统开展形式化验证研究势在必行.需... 操作系统是航天器必备的基本软件,操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障,但仍存在不能完全排除缺陷的情况,因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分,本文在分析操作系统需求的基础上,采用有限状态机在操作系统需求层进行形式化描述,并针对应用在某航天器上的SpaceOS2在需求层进行了建模,相应地在定理证明工具Coq中进行了描述建模;然后定义了六条操作系统应满足的全局性质并进行了形式化描述,给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的,为进一步全面形式化验证奠定了基础. 展开更多
关键词 操作系统 形式化验证 系统需求 有限状态机 COQ
下载PDF
基于场景的形式化测试模型生成方法 被引量:3
17
作者 黄龙 缪淮扣 +1 位作者 王皙 郭亮 《上海大学学报(自然科学版)》 CAS CSCD 北大核心 2011年第5期595-599,共5页
在复杂的Web应用软件中,如何有效地实现自动化测试是当前软件测试研究中的热点与难点.使用统一建模语言(unified modeling language,UML)状态图对Web应用软件的行为建模,利用已有的方法将已建好的模型形式化成有限状态机(finite state m... 在复杂的Web应用软件中,如何有效地实现自动化测试是当前软件测试研究中的热点与难点.使用统一建模语言(unified modeling language,UML)状态图对Web应用软件的行为建模,利用已有的方法将已建好的模型形式化成有限状态机(finite state machine,FSM);然后使用UML顺序图表示场景,通过使用场景规约系统行为,最终得到约简后的形式化测试模型用以实现自动测试. 展开更多
关键词 WEB应用 自动化测试 状态图 有限状态机 顺序图 场景 形式化测试模型
下载PDF
片上系统高层等价性检验研究进展 被引量:1
18
作者 胡健 李暾 李思昆 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2016年第3期371-380,共10页
针对近年来SoC领域的工作,首先分析了高层等价性检验的难点;然后从算法类型归类角度对各种高层等价性检验方法进行了概述评论,同时分析了各类算法的优缺点和现有算法的主要技术手段;最后讨论了SoC高层等价性检验方法目前面临的挑战,并... 针对近年来SoC领域的工作,首先分析了高层等价性检验的难点;然后从算法类型归类角度对各种高层等价性检验方法进行了概述评论,同时分析了各类算法的优缺点和现有算法的主要技术手段;最后讨论了SoC高层等价性检验方法目前面临的挑战,并对该领域今后的研究方向进行了展望. 展开更多
关键词 等价性检验 带数据通路的有限状态机 符号模拟 形式化方法
下载PDF
一种通用中间件安全模型及形式化描述 被引量:3
19
作者 吴景阳 毋国庆 《计算机工程与科学》 CSCD 2006年第1期112-114,共3页
本文通过对中间件安全性的分析,结合传统安全模型的特点,从中间件安全模型设计要求的特点出发,建立了一个可应用于任何中间件技术的通用中间件安全模型;最后对该模型的特征进行分析,并运用有穷状态自动机(FSM)对该模型进行形式化描述,... 本文通过对中间件安全性的分析,结合传统安全模型的特点,从中间件安全模型设计要求的特点出发,建立了一个可应用于任何中间件技术的通用中间件安全模型;最后对该模型的特征进行分析,并运用有穷状态自动机(FSM)对该模型进行形式化描述,并证明了系统的安全性。 展开更多
关键词 中间件安全性 安全模型 体系结构 有穷状态自动机FSM
下载PDF
维吾尔语动词体范畴的有限状态自动机的构建 被引量:4
20
作者 阿孜古丽.夏力甫 早克热.卡德尔 吐尔根.依布拉音 《中文信息学报》 CSCD 北大核心 2012年第4期61-65,84,共6页
维吾尔语动词的体范畴是维吾尔语动词语法范畴中极为复杂的范畴,也是维吾尔语信息处理中的难点问题之一,计算机对维吾尔语动词体范畴的处理是在对人称、时、否定等语法范畴处理之后才进行处理。但是难点就是体范畴重叠问题的解决。维吾... 维吾尔语动词的体范畴是维吾尔语动词语法范畴中极为复杂的范畴,也是维吾尔语信息处理中的难点问题之一,计算机对维吾尔语动词体范畴的处理是在对人称、时、否定等语法范畴处理之后才进行处理。但是难点就是体范畴重叠问题的解决。维吾尔语动词的体范畴词尾按照一定的规则连接在词干,这使得维吾尔语动词体范畴的重叠形式可用有限状态自动机形式化描述。因此它根据重叠规则构造从右向左的非确定自动机,之后把从右向左方向的自动机转换成从左向右的非确定自动机,最后把非确定自动机转换成确定自动机来实现维吾尔语动词体范畴的形式化描述。 展开更多
关键词 维吾尔语 动词 体范畴 有限状态自动机 形式化
下载PDF
上一页 1 2 下一页 到第
使用帮助 返回顶部