导读:本文包含了抽象状态机论文开题报告文献综述及选题提纲参考文献，主要关键词:需求建模语言,实时,嵌入式软件,形式化定义
抽象状态机论文文献综述
单锦辉,张路,王金波,张涛[1]（2019）在《实时嵌入式软件时间抽象状态机的扩展》一文中研究指出针对时间抽象状态机(TASM)存在的不足,对TASM进行扩展,增加数组数据类型、while循环处理规则以及"%","&","|","^",">>"和"<<"等运算符,定义扩展后TASM的语法和语义。采用扩展后的TASM为实际的实时嵌入式软件需求建模,通过实验,验证了采用扩展后的TASM为实时嵌入式软件需求建模的有效性。(本文来源于《北京大学学报(自然科学版)》期刊2019年02期）
杨志斌,胡凯,赵永望,马殿富,Jean-Paul,BODEVEIX[2]（2015）在《基于时间抽象状态机的AADL模型验证》一文中研究指出提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.(本文来源于《软件学报》期刊2015年02期）
易良辰,黄林鹏[3]（2013）在《基于抽象状态机的普适服务组合分析与验证》一文中研究指出提出了一个普适环境下服务组合的框架,使用抽象状态机对服务的行为进行不同精化层级的形式化描述,然后利用CoreASM这一模型检测工具对服务组合进行模拟执行验证,从而验证服务组合的正确性.最后给出了一个运用此方法进行服务组合验证的典型应用场景.(本文来源于《微电子学与计算机》期刊2013年03期）
易良辰[4]（2012）在《普适环境下基于抽象状态机的服务组合的分析与验证》一文中研究指出自20世纪90年代W1eiser[’2]提出“普适计算”概念以来，嵌入式系统，无线通信等技术的发展为“服务无时不在，无处不在”的普适计算从理论变成现实提供了客观的技术基础。普适计算的目标是将由网络和传感器以及移动设备组成的信息空间和现在的物理空间结合起来，支持用户随时随地获取所需的服务。因此如何在普适环境下进行有效的服务组合逐渐成为了一个热点。在普适环境下，不仅有网络上的web服务，还有传感器和移动设备等提供的设备服务以及各类其他的服务，结合SOA思想[3]，共同组成了组合服务并将其最终构建应用模型。但是，由于普适计算环境所具有的自治性，动态性和设备资源的约束性，使得在这样的环境下进行服务组合时面临着特有的问题和挑战[4]，比如服务组合过程中错误的处理、检测，比如设备的动态加入和删除等。因此在普适环境中，如何为用户提供可信的服务组合成为了普适环境下服务组合的关键问题。本文分析了己有的服务组合的技术以及服务组合模型，并在此基础上提出了一个基于抽象状态机的服务组合模型，并提出验证方法。使用抽象状态机对服务的行为进行刻画，能够很好地对服务进行不同精化层级上的形式化描述，从而达到不同层级的正确性验证需求。然后结合SPIN进行安全性、可达性的模型检测。最后本文在实验中利用工具CoreASM和SPIN对文中提出的服务组合模型进行验证，从而保证服务组合的正确性。实验结果表明，我们所提出的服务组合模型和验证方法能够较好地适应普适环境下服务组合系统的需求，验证其正确性，对后续的基于这样的服务组合的实际应用和开发带来积极的意义。(本文来源于《上海交通大学》期刊2012-12-01）
蒋晶晶[5]（2012）在《基于抽象状态机的位置服务推荐模型的研究》一文中研究指出随着智能信息化时代的到来，在日常生活中人们更多的关注与吃、住、行相关的服务信息，因此，智能设备就成为人们随时随地获得这些服务的便捷途径，而这些服务与位置紧密相关，如人们出行在外，想知道距离自己所在位置较近的餐饮有哪些，并希望能获得与自己所喜欢的餐饮相关的推荐，又如在旅行过程中希望能推荐一条自己感兴趣的旅游路线等信息或将自己走过的旅游路线分享给其他人，为他们的出行提供参考等。对于这些需求，通过移动通讯网络或定位技术获得移动终端用户的个人位置信息，再结合地理位置信息系统为用户提供基于位置的服务(Location Based Service，LBS)已经成为一个研究热点。而LBS所提供与位置相关的服务都不同程度地使用了个性化推荐，如facebook、贝多网、网易八方和去哪网等应用。然而现有的基于位置服务推荐系统缺乏统一的理论模型，并且其推荐质量有待提高，因此我们主要针对如何建立具有理论依据的位置推荐模型和用户轨迹模式进行挖掘。具体研究成果包括：1.提出了一种基于抽象状态机的位置服务推荐模型。该模型利用抽象状态机方法进行建模，用简单的数学结构描述位置服务推荐计算的状态构建清晰易懂的位置服务推荐模型。而且该模型可以作为基准模型，可按具体需求对其任意进行水平和垂直调整。我们利用抽象状态机对构建的模型进行语义描述，即可对该模型的不同抽层次进行描述。2.将位置服务推荐模型扩展为个性化路线推荐模型，并对扩展模型各模块所涉及的数据处理、聚类、计算用户路线相似度算法分别进行了研究，特别是我们提出了新的计算用户路线相似度方法最长语义轨迹相似度（Longest Semantic TrajectorySimilarity，LSTS），结合动态规划的思想避免了计算路线子序列的重复计算问题，主要是对传统算法的实效性和准确性进行了改善。3.我们还用AsmL对整个路线推荐模型内部一致性和合理性进行了验证，AsmL测试所生成的有限状态自动机的状态迁移证明了整个模型的可靠性。基于个性化路线推荐模型实现了旅游路线推荐系统，并在此系统应用了我们提出的数据预处理方法和计算用户相似度算法LSTS。我们还将LSTS算法与传统的计算用户相似度方法进行了比较，实验结果表明LSTS算法的准确率和时间效率方面都优于传统方法。(本文来源于《湘潭大学》期刊2012-05-18）
张引,何浩,赵丽娜,张叁元[6]（2010）在《网构软件模型中的抽象状态机设计》一文中研究指出为了更好地支持和实现网构软件的自动化,提出在网构软件模型中使用抽象状态机(ASM).在Internet的计算环境下,采用peer-to-peer(P2P)拓扑结构作为网构软件模型的支撑网络环境,使用ASM的方法从较高的抽象层次(概念层)描述整个系统的行为与状态变迁,使系统特征易于把握.分析网构软件模型中ASM的架构,详细阐述ASM的运行规则,说明了系统状态特征的变迁情况.根据ASM方法所涉及到的各种状态、事件、方法、数据、规则等进行相应的设计和实现,已经初步形成一个网构软件设计和运行的支撑平台,证明了ASM在网构软件模型中的可行性以及ASM能够实现网构软件的自动化特性.(本文来源于《浙江大学学报(工学版)》期刊2010年05期）
米海波,王怀民,尹刚[7]（2010）在《Chord协议的抽象状态机模型》一文中研究指出P2P是构筑于互联网的大规模分布计算协议,采用形式化方法对P2P协议的本质原理进行分析,将有助于P2P协议的优化和改进。本文采用抽象状态机(ASM)对经典P2P协议Chord进行分析,用基于抽象状态机语言(Asml)对其建模,设计了核心运行规则,并得到了该协议的有限状态机模型。本文的工作有助于分析、优化P2P协议。(本文来源于《计算机工程与科学》期刊2010年04期）
杨丹丹[8]（2010）在《基于抽象状态机的协议软件测试方法研究》一文中研究指出随着软件开发技术的发展,软件越来越复杂,人们对软件的需求也越来越多,软件是否是按需求开发,能否正确有效的运行,成为软件开发者日益重视的问题。软件测试在整个软件开发过程中也是耗费最大的一个方面,不仅是耗费人力,物力,并且还缺乏系统的工程方法、清晰的语义、以及充分的工具支持,这就使得软件测试方法的研究越来越重要。本文研究的目的在于根据当前国内外基于模型的软件测试研究现状,结合面向对象的软件开发方法的特征,设计并实现了用抽象状态机语言描述统一建模语言状态图的过程,实现了基于抽象状态机语言的软件一致性测试。本文首先介绍了软件测试的基本概念以及基于模型的软件测试研究现状,分析了目前构建软件模型主要的形式化方法,比较其各自的优缺点。其次介绍了抽象状态机的基本理论和抽象状态机语言,并论述其用做测试的理论基础和优点。在此基础上,设计出了统一建模语言状态图用抽象状态机语言描述的方法,并演示对比统一建模语言状态图与抽象状态机,研究了基于抽象状态机进行一致性测试的原理和方法。用.NET环境下分布式程序设计框架实现基于实时传输协议的远程教育系统,用抽象状态机语言描述所用的实时传输协议,并实现其一致性测试。在前面所论述的理论基础上,构建系统的抽象状态机模型,实现了远程教育系统的一致性测试,并给出测试结果并进行了分析。在论文的结束部分简述了本人工作及研究中尚需解决的问题,对其中一些问题给出了进一步研究的思路和改进意见,并展望了抽象状态机方法在测试方面的研究和发展方向。(本文来源于《西安电子科技大学》期刊2010-01-01）
刘晖,李明禄[9]（2003）在《基于抽象状态机的网格系统设计和分析》一文中研究指出基于可执行规范的实现 测试同步开发模式可以将错误尽早消灭在各个开发阶段的初期 .其理论基础是抽象状态机ASM ,实现工具是支持 .NET的AsmL .本文首先介绍了基于可执行规范的实现 测试同步开发模式、ASM起源和定义 ,然后采用ASM描述了网格高层次系统语义 ,并举例说明了采用AsmL生成有限状态机分析模型语义的方法步骤 .本文认为基于ASM的网格系统设计和分析值得学术界和工业界的共同关注(本文来源于《电子学报》期刊2003年S1期）
抽象状态机论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
抽象状态机论文参考文献
[1].单锦辉,张路,王金波,张涛.实时嵌入式软件时间抽象状态机的扩展[J].北京大学学报(自然科学版).2019
[2].杨志斌,胡凯,赵永望,马殿富,Jean-Paul,BODEVEIX.基于时间抽象状态机的AADL模型验证[J].软件学报.2015
[3].易良辰,黄林鹏.基于抽象状态机的普适服务组合分析与验证[J].微电子学与计算机.2013
[4].易良辰.普适环境下基于抽象状态机的服务组合的分析与验证[D].上海交通大学.2012
[5].蒋晶晶.基于抽象状态机的位置服务推荐模型的研究[D].湘潭大学.2012
[6].张引,何浩,赵丽娜,张叁元.网构软件模型中的抽象状态机设计[J].浙江大学学报(工学版).2010
[7].米海波,王怀民,尹刚.Chord协议的抽象状态机模型[J].计算机工程与科学.2010
[8].杨丹丹.基于抽象状态机的协议软件测试方法研究[D].西安电子科技大学.2010
[9].刘晖,李明禄.基于抽象状态机的网格系统设计和分析[J].电子学报.2003