一、时间符号迁移图上的可达性分析（论文文献综述）
吕铃[1]（2019）在《基于复杂网络的公共自行车关键节点选取和网点布设优化研究》文中研究表明近年来,随着公共自行车系统的迅猛发展,其独特的交通流量疏通优势日益展现出来,在广大居民的日常生活中大显身手。与此同时,由于使用需求的激增和运营规模的扩张,系统也逐渐暴露出不少缺陷。比如:高峰时期与高频使用地点车辆周转率不平衡,中心城区与偏远郊区路网流量分配不均、车辆调度难、成本高等问题。这些问题的产生主要是由于部分客流量大的关键节点流量失衡导致的,如何运用科学手段对这些节点合理筛选及优化控制是提高公共自行车系统运行效率的关键。复杂网络是用以描述现实世界中系统及其构成元素之间相互作用关系的重要工具。其中有许多关于网络结构稳定性、演化规律、交通阻塞动力学行为、阻塞疏导方案的研究方法可以借鉴。公共自行车交通系统作为一个离散时间的复杂动力学复杂网络,网络的拓扑结构和网点的布设对整个网络流量的传输效率具有重要的影响。合理筛选关键节点并建立其分流优化方案,就能够较好避免网络拥塞,提高整个系统的运行效率。有资料表明,我国公共自行车系统现有的优化方案研究主要集中在单一指标筛选问题节点上,考虑交通属性和用户出行特性很少,针对筛选出的关键节点,也大多未给出下一步合理的优化方案。基于以上事实和分析,本文采用公共自行车真实租赁数据建立复杂网络,针对公共自行车交通系统中动态拓扑与网点布局优化难点进行分析,评价系统整体运营情况,构建关键节点选取策略,通过对少量关键节点实施动态优化控制,达到系统的整体优化。本文的主要研究和成果如下:1、基于实际的公共自行车系统运营数据,从复杂网络拓扑结构入手,对其进行统计分析。分析结果表明其网络度分布符合幂律分布,整体拓扑分析显示公共自行车的用户需求模式具有无标度和小世界特性,符合“六度空间理论”。系统综合运营情况较好,但网点分布小部分关键节点可进一步优化。2、针对关键节点的动态存量失衡问题,紧扣公共自行车系统的公共交通特性,结合目的地功能区域进行社团划分,设计可达性指标潜力评价模型用以筛选关键节点。将结果与经典度值和介数中心性指标进行对比分析,得出对关键节点的优化方案。3、针对筛选出的关键节点,综合考虑网点之间位置,提出一种基于波面理论的公共自行车关键节点优化方案。利用波面净流阈值辐射法在关键节点附近放置辅助节点缓解关键节点的压力,以达到局部辅助分流作用。实证表明本文提出的基于分区可达性指标筛选关键节点策略能更加充分的反映出各个网络关键节点的特征;波面理论网点优化方案能有效解决网点失衡现象,优化公共自行车初始网点的布设,提高车辆使用率,达到从局部优化提高全局效率的目的,本文的研究成果能够为公共自行车系统的建立提供有益的指导意见。
吕铃,彭雅丽,曾欣怡,杨雨鑫,黄明和[2]（2018）在《公共自行车复杂网络可达性指标潜力评价模型》文中研究表明基于公共自行车系统运营数据,提出了复杂网络可达性指标潜力评价模型,从整体复杂网络拓扑特征分析,到进行交通功能分区的可达性指标潜力评价分析,进而筛选出网络中的关键节点,并能为公共自行车系统优化提供理论依据。整体拓扑分析显示公共自行车的用户需求模式具有无标度和小世界特性,其网点分布仍然有小部分关键节点可进一步优化。依据其中短距离出行需求和在长距离中的公共交通衔接功能划分的网络,其可达性指标潜力评价能筛选出网络中的关键节点,并能进一步将关键节点的实际流量与潜力指标进行对比分析,得出对关键节点更准确的优化建议。实际数据分析显示,基于分区的可达性指标潜力评价模型能为公共自行车更好地发挥其在公共交通中的作用提供理论优化依据。
罗玲[3]（2015）在《扩展π演算的建模、验证与测试》文中研究说明时间相关移动并发系统是以并发性、移动性、时间相关性和异构性等为主要特征的计算系统。对于这类系统,特别是安全攸关的时间相关移动并发系统,如移动支付系统、移动通信系统、交通控制系统等,其失误和崩溃可能会造成重大损失,因此时间相关移动并发系统的正确性、安全性等质量属性受到人们的普遍重视。对时间相关移动并发系统采用以严格数学理论为支撑的形式化方法进行建模、验证与测试是行之有效的减少系统设计错误和保证系统质量的重要途径。进程代数,作为形式化方法的代表,是一种重要的用于对并发系统进行建模和验证的技术。由于所面向的领域和应用背景的不同,涌现出很多进程代数的分支和变种,其中演算就是用于建模移动性的重要的分支。近年来,由于新型网络技术和信息技术的不断发展,使得能够建模和验证移动系统的演算得到人们的广泛关注。但是,演算在对系统建模时并未考虑到动作执行所占用的时间以及系统在某个状态所持续的时间,故而,使得它不适于对时间相关系统进行建模、验证和测试。为了对时间相关移动并发系统进行建模和验证,本文研究了添加时间相关特性的扩展的演算。在此基础上,提出采用扩展演算为时间相关移动并发系统进行建模和推演的方法。进一步地,为了对扩展演算建模的系统进行自动验证,提出将扩展演算转换为建模、仿真验证语言MSVL的方法。此外,为了对扩展演算建模的系统进行测试,文章还给出了采用扩展演算的测试用例生成方法。所取得的研究成果主要有以下几个方面。（1）建立了带区间动作前缀的扩展演算p-π,定义了p-π的语法和操作语义,给出了p-π的代数性质和时间相关性质并对其进行了证明。在此基础上给出了p-π对时间相关行为的建模。此外,还通过实例对p-π的应用效果和相应性质所起的作用进行了分析和说明。（2）提出了采用扩展演算对时间相关移动并发系统进行建模和推演的方法。采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,基于上述迁移系统和执行路径完成对系统性质的推演。通过移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。（3）提出了从扩展演算p-π到MSVL的转换方法。为了完成转换,先在MSVL中对通道和通信原语进行了定义。基于该定义,给出了从p-π到MSVL的结构化转换规则,并对二者采用的通信机制间存在的一致性进行了证明。为了说明转换的合理性,文章还证明在p-π进程和MSVL的格局间存在互模拟关系。这样,通过转换,就可以借助MSVL建模仿真验证工具完成对p-π进程的验证。（4）提出了基于扩展演算的测试用例生成方法。采用p-π为时间相关并发系统建模并由p-π的操作规则构造出系统模型的时间相关标记迁移系统。基于时间相关标记迁移系统和用例规约生成测试用例,测试用例的生成满足执行动作覆盖准则、路径覆盖准则和时间约束覆盖准则,并给出了测试用例的选择策略。同时通过p-π的验证方法,还保证了所产生的测试用例的正确性。
马俊锋[4]（2010）在《面向跨组织业务协作的角色网络模型研究》文中指出随着竞争环境的不断变化、互联网等信息技术的高速发展,跨组织的业务协作日趋频繁和紧密,越来越多的业务流程跨越组织边界,跨组织业务流程正成为组织生存和发展的基础。跨组织业务流程具有动态性、不确定性等特征,目前相关研究难以满足对跨组织业务流程的形式化建模及分析的需要。跨组织业务流程涉及多个组织,规模较大,因此在业务流程实际执行前,需要对流程进行验证和分析,以确保流程的科学可靠。角色网络模型（RNM, Role Network Model）体系深入刻画了组织间业务协作的本质,支持动态业务流程的柔性控制,但在业务流程尤其是动态业务流程的形式化建模和分析方面仍有欠缺。针对这些问题,本文借鉴业务流程管理（BPM）框架,在角色网络理论的基础上结合Pi演算,构建面向跨组织业务协作的角色网络模型（IOBCORNM, Inter-organizational Business Collaborations Oriented Role Network Model）,并在IOBCORNM的基础上提出角色验证及流程的可达性分析方法,本文所做工作如下：（1）对组织间关系进行分析,对跨组织业务协作进行分类,总结跨组织业务流程的特征。（2）借鉴BPM框架,在角色网络理论的基础上结合Pi演算,构建IOBCORNM,包括面向跨组织业务协作的角色模型（IOBCORM, Inter-organizational Business Collaborations Oriented Role Model）和跨组织角色网络模型（IORNM Inter-organizational Role Network Model）,从而实现了对跨组织业务流程的形式化建模,然后基于该模型对实例进行了建模。（3）基于IOBCORNM,提出了角色验证方法和流程的可达性分析方法,从而保证模型的正确性和流程执行的可靠性,并通过实例对两种方法进行了阐述。本研究对角色网络模型进行了扩展,弥补了其在形式化描述动态业务流程以及在业务流程分析方面的不足。在跨组织业务流程尤其是动态业务流程的形式化建模、柔性控制及流程分析等方面具有理论指导意义,并在跨组织业务协作相关的信息系统建设方面具有较强的应用价值。
刘荣胜[5]（2007）在《离散实时Mobile Ambients》文中认为随着计算机技术和网络技术的发展，移动计算与实时计算已经成为计算机科学领域的两个研究热点，受到越来越多的关注。不同领域的学者对这一问题的研究有不同的方法。形式化方法作为研究分布式、并发计算的一个重要重要方法，近年来得到了飞速的发展。形式化专家们提出了许多移动计算和实时计算的形式系统：如自动机、petri网、CCS、Pi演算、Mobile Ambients等。这些形式系统可以刻画、研究并发分布式系统，传值计算以及空间移动系统。但是它们各有特色，比方说Pi演算适合于传值计算；而Mobile Ambients在空间移动计算系统中更能够发挥自己的优势。实时计算作为近年计算机科学领域的另一个研究的热点，形式化专家也提出了它的形式化框架。这些实时形式化框架主要是用时间对原有的形式系统的扩展。新的形式化框架能够研究计算机系统在时间方面的性质，已有的实时系统有Timed Automata，Timed CCS，实时Pi演算等，但这些实时形式系统由于扩展前原型系统的局限性，不能表示空间结构。通过以Mobile Ambients演算为基础的实时扩充，可以很好的将时空统一到同一个形式化框架中研究。本文首先讨论了Mobile Ambients的优点和不足，然后提出一种基于图的实时移动计算模型，接下来用时间对Mobile Ambients进行扩展，提出了一种新的实时形式化系统——离散实时Mobile Ambients。对一个系统作模型验证，不仅需要将系统用形式语言表示，而且还要将系统要求满足的性质表示成模态逻辑公式。为利用离散实时Mobile Ambients对实时移动计算系统做模型验证，本文对Mobile Ambients的时态逻辑也作了扩展，提出了能够描述实时性质的模态逻辑。最后对离散实时Mobile Ambients演算的子集提出了模型验证算法，并且用离散实时Mobile Ambients演算建模Web服务组合语言BPEL4WS。本文的主要内容包括以下几个部分：第一，讨论了mobile ambients的优缺点，并且提出了基于图的实时移动计算模型；第二，对Mobile Ambients作实时扩展，提出新的实时形式系统——离散实时Mobile Ambients；第三，提出离散实时Mobile Ambients演算的时态逻辑，给出离散实时Mobile Ambients的模型验证算法，并给出离散实时Mobile Ambients演算模型验证的可判定性的证明。第四，利用离散实时Mobile Ambients建模Web服务组合语言BPEL4WS，对一个Web服务实例进行模型验证。最后，总结全文工作，并展望了以后的前景。
唐江峻[6]（2004）在《基于STGA的并发程序测试》文中进行了进一步梳理本文提出一种基于带赋值符号迁移系统STGA选取测试同步序列的方法。与传统的基于标号：迁移系统LTS的方法相比，STGA中保留了对测试同步序列的选取有重要影响的结构信息，因此有利于高效率同步序列的选取。实例研究证实了这一优越性。 在这个基础上我们还提出了若干覆盖率标准来指导同步序列的选取，实例研究也表明在发现错误的能力方面，根据这些覆盖率选取出来的同步序列要好于随机选取的同步序列。
张轶[7]（2003）在《并发传值进程模型检测工具的数据类型扩展》文中指出模型检测技术是近二十年来最成功的自动验证技术之一，目前被广泛的应用于有穷状态系统（包括电路设计和通讯协议等）的分析与验证。对于并发传值系统的自动分析与验证是模型检测研究的一个新的方向。 随着并发系统规模的日益增大，对这类系统的模型检测面临着如何处理大规模状态空间问题的挑战，因此需要为实际的大规模并发系统精心选择计算模型，同时设计时空效率较高的算法。但是我们注意到并发传值系统的一个特点是其子系统间的通讯经常涉及复杂数据结构，包括数组、列表和记录等。以往处理复杂数据结构的做法是抽象掉数据信息或者将复杂数据结构打散，因而较大的影响了检测效率。解决这个问题的一个方案是：使用带赋值符号迁移图（STGA）作为并发传值进程的模型，使用谓词μ演算作为刻画性质的逻辑，并采用动态实例化的算法对传值并发进程直接进行模型检测。 本文提出了将复杂数据结构引入上述模型检测方案的办法，扩大了该解决方案可以应用的问题领域。主要工作如下： ·扩展传值CCS使其成为有严格类型规则的易于使用的系统描述语言、扩充了STGA的定义和生成规则使其适于作为实际系统的计算模型。 ·提出了扩展STGA图的优化算法。 ·扩充检测问题的定义语言—脚本语言的格式，使用SML语言实现了脚本语言的编译和扩展STGA图生成模块，并将该模块和检测算法核心连接，实现了整个工具。论文还结合应用实例证明了扩展工作的有效性并分析了工具的性能。
陈靖[8]（2003）在《带实时的传值与移动系统研究》文中研究表明实时系统是一种要求反应或计算必须在规定时间内发生的系统。由于这些系统在工业及国防领域有着重要而广泛的应用，因此对这些系统进行形式化分析也成为近年来的一个研究热点。 随着社会的发展，尤其是网络的普及和应用，包括通讯协议和控制系统在内的越来越多的软件都以并发的方式运行，我们研究的就是这类带并发的实时系统。在对并发系统的研究中，传值和移动计算分别是两个不同的研究热点。在现有文献中，虽然对一些传统的基本并发系统都进行了实时扩充，得到了如Timed CCS，Timed CSP等实时演算，但尚未有能刻划实时传值系统的演算，而对移动演算，虽然有少数对π演算进行实时扩充的工作，但其语义是基于离散时间域的，并不能刻划时间在实数域上连续增长（流逝）等精确行为。 本文的研究工作主要由对实时传值系统和实时移动系统的建模和分析组成。 对于实时传值系统，本文的研究从计算模型与语义理论、分析与验证算法以及支持工具三个层面展开。在计算模型与语义理论方面着重探讨了带并发性的实时传值模型，定义了一个新的计算模型-时间符号迁移图（Timed Symbolic Transition Graph），并建立了合适的语义理论。在分析与验证算法的设计方面，在新的计算模型基础上，我们分析了实时传值进程间各种不同互模拟的特点以及判定方法；尤其针对时间互模拟，根据符号互模拟的思想，本文给出了一个时间符号迁移图上的判定算法并证明了算法的正确性。在模型检测的算法方面，本文首先给出了时间符号迁移图上的一个可达性分析算法，随后还定义了能刻划更复杂性质的实时谓词μ演算并给出了检测这些性质的相应模型检测算法。为了有效地对连续时间进行表示和操作，本文针对通常使用的数据结构的范式化过程中出现的问题提出了一种新的信息消冗算法。在给出基本算法的基础上，我们构造了相应的验证工具-RealM，并在本文中给出了对限时重传协议进行的实例分析。 对于实时移动系统，本文对π演算进行了实时扩充，给出了实时π演算的语法和语义，并定义了该演算上的各种互模拟关系，以及相关的性质。本文不但证明了经典π演算的多数性质在新的模型下得到保持，还进一步给出了与时间有关的一些新的等式公理。最后，本文对实时π演算的一个有穷子集上的强实互模拟以及强互模拟均给出了完备的公理化结果。
陈靖[9]（2003）在《时间符号迁移图上的可达性分析》文中研究表明提出了以时间符号迁移图为建模语言、基于可达性分析的模型检测算法 ,并给出了算法的正确性证明 .该算法可被用于硬件设计和通信协议验证等领域
二、时间符号迁移图上的可达性分析（论文开题报告）
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文主要提出一款精简64位RISC处理器存储管理单元结构并详细分析其设计过程。在该MMU结构中,TLB采用叁个分离的TLB,TLB采用基于内容查找的相联存储器并行查找,支持粗粒度为64KB和细粒度为4KB两种页面大小,采用多级分层页表结构映射地址空间,并详细论述了四级页表转换过程,TLB结构组织等。该MMU结构将作为该处理器存储系统实现的一个重要组成部分。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
三、时间符号迁移图上的可达性分析（论文提纲范文）
（1）基于复杂网络的公共自行车关键节点选取和网点布设优化研究（论文提纲范文）
| 摘要 |
| Abstract |
| 第1章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 交通复杂网络研究现状 |
| 1.2.2 关键节点筛选研究现状 |
| 1.2.3 网点布设优化研究现状 |
| 1.3 研究内容、研究目标和拟解决的关键问题 |
| 1.3.1 研究目标和研究内容 |
| 1.3.2 拟解决的关键问题 |
| 1.4 本文研究的技术路线及结构安排 |
| 第2章 复杂网络基础理论概念和公共自行车系统特征描述 |
| 2.1 复杂网络概述 |
| 2.1.1 四种复杂网络类型 |
| 2.1.2 复杂网络拓扑特性指标 |
| 2.2 公共自行车系统构成要素 |
| 2.3 公共自行车网络特征概述 |
| 2.3.1 构成公共自行车网络的特征和基本要素 |
| 2.3.2 公共自行车复杂网络图论表示方法 |
| 2.4 本章小结 |
| 第3章 可达性指标及潜力模型评价的公共自行车复杂网络关键节点筛选方案 |
| 3.1 公共自行车复杂网络的构建 |
| 3.1.1 公共自行车系统基本数据 |
| 3.1.2 基于用户借还的网络模型构建方式 |
| 3.2 网络可达性指标及潜力评价模型 |
| 3.2.1 网络划分和可达性概念 |
| 3.2.2 网络划分 |
| 3.2.3 可达性指标 |
| 3.2.4 容量潜力模型 |
| 3.3 本章小结 |
| 第4章 波面理论关键节点优化方案 |
| 4.1 净流分析 |
| 4.2 增设节点优化方案 |
| 4.3 优化方案效果评价 |
| 4.4 本章小结 |
| 第5章 实证分析 |
| 5.1 公共自行车复杂网络拓扑性质分析 |
| 5.1.1 无标度特性 |
| 5.1.2 网络分布分析 |
| 5.2 关键节点选取分析 |
| 5.2.1 长距离公共交通衔接区域可达性分析 |
| 5.2.2 中短距离衔接区域可达性分析 |
| 5.2.3 关键节点筛选评价 |
| 5.3 关键节点优化分析 |
| 5.3.1 网点净流分析 |
| 5.3.2 关键节点波面增设分析 |
| 5.3.3 增设节点效率总结 |
| 5.4 本章小结 |
| 第6章 总结与期望 |
| 6.1 研究总结 |
| 6.2 未来研究展望 |
| 参考文献 |
| 致谢 |
| 在读期间公开发表论文(着)及科研情况等 |
（2）公共自行车复杂网络可达性指标潜力评价模型（论文提纲范文）
| 1 引言 |
| 2 公共自行车复杂网络的构建 |
| 2.1 公共自行车系统基本数据 |
| 2.2 基于用户借还的网络模型构建方式 |
| 3 公共自行车复杂网络拓扑性质分析 |
| 3.1 无标度特性 |
| 3.2 网络分布分析 |
| 4 网络可达性指标及潜力评价模型 |
| 4.1 网络划分和可达性概念 |
| 4.1.1 网络划分 |
| 4.1.2 可达性指标 |
| 4.1.3 容量潜力模型 |
| 4.2 长距离公共交通衔接区域可达性分析 |
| 4.3 中短距离衔接区域可达性分析 |
| 4.4 关键节点筛选评价 |
| 5 结束语 |
（3）扩展π演算的建模、验证与测试（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 缩略词对照表 |
| 第一章 绪论 |
| 1.1 研究背景与意义 |
| 1.2 形式化模型 |
| 1.2.1 基于图形化的模型 |
| 1.2.2 基于文本的模型 |
| 1.3 形式化验证 |
| 1.3.1 模型检测 |
| 1.3.2 定理证明 |
| 1.4 基于模型的测试 |
| 1.4.1 基于非形式化模型的测试 |
| 1.4.2 基于形式化模型的测试 |
| 1.5 相关研究工作与本文研究目的 |
| 1.5.1 相关研究工作 |
| 1.5.2 本文研究目的 |
| 1.6 论文的主要工作与组织结构 |
| 第二章 π演算与MSVL |
| 2.1 π演算 |
| 2.1.1 π演算的语法和语义 |
| 2.1.2 π演算的移动性 |
| 2.1.3 π演算的研究进展 |
| 2.2 建模、仿真与验证语言MSVL |
| 2.2.1 投影时序逻辑PTL |
| 2.2.2 MSVL |
| 2.3 本章小结 |
| 第三章 扩展π演算―p-π |
| 3.1 p-π的语法 |
| 3.2 p-π的语义 |
| 3.2.1 结构等价 |
| 3.2.2 操作规则 |
| 3.3 p-π的性质 |
| 3.3.1 代数性质 |
| 3.3.2 时间相关性质 |
| 3.4 时间相关行为的建模 |
| 3.4.1 时间延迟 |
| 3.4.2 超时处理 |
| 3.4.3 中断处理 |
| 3.5 实例 |
| 3.6 本章小结 |
| 第四章 时间相关移动并发系统的建模与推演 |
| 4.1 系统描述 |
| 4.2 系统建模 |
| 4.3 系统推演 |
| 4.3.1 基于操作规则的系统迁移 |
| 4.3.2 基于系统迁移的系统推演 |
| 4.4 本章小结 |
| 第五章 从p-π到MSVL的结构化转换方法 |
| 5.1 MSVL的通道和通信原语 |
| 5.2 从p-π到MSVL的转换 |
| 5.2.1 名字和原子命题的转换 |
| 5.2.2 进程的转换 |
| 5.2.3 Interleaving和True Concurrency间的一致性 |
| 5.2.4 注意 |
| 5.3 转换的合理性 |
| 5.4 应用实例 |
| 5.4.1 系统建模 |
| 5.4.2 转换 |
| 5.4.3 验证 |
| 5.5 本章小结 |
| 第六章 采用扩展π演算的测试用例生成方法 |
| 6.1 时间相关标记迁移系统 |
| 6.2 测试用例生成 |
| 6.2.1 执行路径 |
| 6.2.2 可观察动作与不可观察动作 |
| 6.2.3 覆盖准则 |
| 6.2.4 互模拟进程替换 |
| 6.2.5 基于对象约束语言的用例规约 |
| 6.2.6 测试用例生成算法 |
| 6.2.7 测试用例选择策略 |
| 6.3 应用实例 |
| 6.3.1 OBS的p-π系统进程 |
| 6.3.2 系统的TDLTS |
| 6.3.3 测试用例生成 |
| 6.4 相关方法比较 |
| 6.5 本章小结 |
| 第七章 总结与展望 |
| 7.1 全文总结 |
| 7.2 未来的研究工作 |
| 附录A |
| 参考文献 |
| 致谢 |
| 作者简介 |
| 1. 基本情况 |
| 2. 教育背景 |
| 3. 攻读博士学位期间的研究成果 |
（4）面向跨组织业务协作的角色网络模型研究（论文提纲范文）
| 摘要 |
| Abstract |
| 1 绪论 |
| 1.1 选题背景 |
| 1.2 研究思路与研究意义 |
| 1.3 技术路线和研究内容 |
| 2 相关研究进展和文献综述 |
| 2.1 BPM相关研究 |
| 2.1.1 BPM |
| 2.1.2 业务流程建模方法与技术 |
| 2.1.3 业务流程分析 |
| 2.2 Pi演算和角色网络理论 |
| 2.2.1 Pi演算 |
| 2.2.2 角色网络理论 |
| 2.2.3 Pi演算与角色网络的比较分析 |
| 2.3 组织间协作关系 |
| 3 面向跨组织业务协作的角色网络模型 |
| 3.1 跨组织业务协作分析 |
| 3.1.1 组织间关系分析 |
| 3.1.2 跨组织协作关系分类 |
| 3.1.3 跨组织业务流程特征分析 |
| 3.2 面向跨组织业务协作的角色模型 |
| 3.2.1 角色的定义及描述 |
| 3.2.2 角色间的协作接口 |
| 3.2.3 角色与协作接口的映射 |
| 3.2.4 基于IOBCORM的跨组织业务协作的描述 |
| 3.3 跨组织角色网络模型 |
| 3.3.1 概念模型 |
| 3.3.2 形式化描述 |
| 3.4 基于IOBCORNM的实例建模 |
| 3.4.1 企业登记注册实例 |
| 3.4.2 企业登记注册实例建模 |
| 3.5 基于IOBCORNM的跨组织业务流程的描述 |
| 3.5.1 静态业务流程的描述 |
| 3.5.2 动态业务流程的描述 |
| 4 基于IOBCORNM的角色验证与可达性分析方法 |
| 4.1 角色验证方法 |
| 4.1.1 角色描述表 |
| 4.1.2 单角色验证 |
| 4.1.3 多角色验证 |
| 4.1.4 角色验证实例 |
| 4.2 可达性分析方法 |
| 4.2.1 静态业务流程的可达性分析 |
| 4.2.2 动态业务流程的可达性分析 |
| 4.2.3 可达性分析实例 |
| 结论 |
| 参考文献 |
| 攻读硕士学位期间发表学术论文情况 |
| 致谢 |
（5）离散实时Mobile Ambients（论文提纲范文）
| 摘要 |
| Abstract |
| 目录 |
| 第一章 绪论 |
| 1.1 研究背景 |
| 1.2 研究现状和发展 |
| 1.3 本课题的主要工作 |
| 1.3.1 研究设想和主要研究内容 |
| 1.3.2 本文的主要贡献和创新之处 |
| 1.4 论文的组织结构 |
| 第二章 Ambient时间树 |
| 2.1 Mobile Ambients演算 |
| 2.1.1 Mobile Ambients语法 |
| 2.1.2 Mobile Ambients操作语义 |
| 2.2 Ambient图 |
| 2.2.1 Mobile Ambients的图表示 |
| 2.2.2 Ambient图归约 |
| 2.3 Ambient时间树 |
| 2.3.1 Ambient时间同步树的表示 |
| 2.3.2 Ambient时间同步树的结构 |
| 2.4 小结 |
| 第三章 离散实时Mobile Ambients |
| 3.1 离散实时Mobile Ambients的语法 |
| 3.2 离散实时Mobile Ambients的语义 |
| 3.2.1 离散实时Mobile Ambients的归约语义 |
| 3.2.2 离散实时Mobile Ambients的指称语义 |
| 3.3 离散实时Mobile Ambients的性质 |
| 3.4 小结 |
| 第四章 离散实时Mobile Ambients模态逻辑 |
| 4.1 离散实时Mobile Ambients模态逻辑语法 |
| 4.2 离散实时Mobile Ambient模态逻辑语义 |
| 4.3 离散实时Mobile Ambients模型验证算法 |
| 4.4 离散实时Mobile Ambients模型验证的判定性 |
| 4.5 小结 |
| 第五章 离散实时Mobile Ambients建模BPEL4WS |
| 5.1 BPEL4WS简介 |
| 5.2 离散实时Mobile Ambients建模BPEL4WS |
| 5.2.1 编码顺序控制结构 |
| 5.2.2 编码通道 |
| 5.2.3 名字匹配的编码 |
| 5.2.4 非确定性选择 |
| 5.3 BPEL4WS基本活动建模 |
| 5.4 实例建模 |
| 5.5 小结 |
| 第六章 总结与展望 |
| 参考文献 |
| 附录1 攻读硕士期间发表的学术论文 |
| 附录2 致谢 |
（6）基于STGA的并发程序测试（论文提纲范文）
| 第1章 引言 |
| 1.1 测试 |
| 1.2 顺序程序测试 |
| 1.2.1 黑盒测试 |
| 1.2.2 白盒测试 |
| 1.2.3 测试流程 |
| 1.2.4 测试种类 |
| 1.3 并发程序测试 |
| 1.4 本文的主要工作 |
| 1.5 本文的组织 |
| 第2章 并发程序测试简介 |
| 2.1 同步错误 |
| 2.2 并发程序测试方法 |
| 2.2.1 非确定性测试 |
| 2.2.2 确定性测试 |
| 2.2.3 综合性测试 |
| 2.3 同步序列生成 |
| 第3章 LTS、CCS和STGA |
| 3.1 LTS |
| 3.2 CCS |
| 3.2.1 基本CCS |
| 3.2.2 传值CCS |
| 3.3 STGA |
| 第4章 同步序列的生成 |
| 4.1 从LTS中生成同步序列 |
| 4.2 从STGA图生成同步序列 |
| 第5章 符号同步序列的覆盖率标准 |
| 第6章 测试实例与分析 |
| 第7章 结论 |
| 参考文献 |
| 附录A MSMIE协议的VP描述 |
| 附录B 满足路径覆盖的同步序列组 |
| 附录C 满足动作组覆盖的同步序列组 |
| 在学期间发表论文 |
| 致谢 |
（7）并发传值进程模型检测工具的数据类型扩展（论文提纲范文）
| 插图目录 |
| 表格目录 |
| 第1章 引言 |
| 1.1 背景 |
| 1.2 论文主要工作 |
| 1.3 论文的组织 |
| 第2章 并发传值系统和模型检测 |
| 2.1 并发传值系统 |
| 2.2 模型检测 |
| 2.3 并发传值进程模型检测工具 |
| 第3章 CCS和μ演算 |
| 3.1 纯CCS和传值CCS |
| 3.2 μ演算 |
| 3.2.1 模态逻辑 |
| 3.2.2 时序逻辑 |
| 3.2.3 命题μ演算 |
| 3.2.4 谓词μ演算 |
| 第4章 系统模型和检测算法 |
| 4.1 在传值CCS中引入赋值动作 |
| 4.2 STGA图的扩展 |
| 4.2.1 基本STGA图及操作语义 |
| 4.2.2 在STGA图迁移边上引入赋值列表 |
| 4.2.3 扩展STGA图的优化算法 |
| 4.3 嵌套等式系和模态图 |
| 4.3.1 嵌套等式系和分块等式系 |
| 4.3.2 模态图的语法和语义 |
| 4.4 模型检测算法 |
| 4.5 反例生成 |
| 第5章 系统的结构和实现 |
| 5.1 系统结构 |
| 5.2 脚本语言 |
| 5.2.1 脚本语言文法 |
| 5.2.2 脚本语言翻译方案和类型检查 |
| 5.3 实现细节 |
| 5.3.1 STGA图生成和优化的几个问题 |
| 5.3.2 有关模型检测算法的几个问题 |
| 第6章 检测实例 |
| 6.1 读者写者问题 |
| 6.2 RETHER协议的检测和性能分析 |
| 第7章 结束语 |
| 参考文献 |
| 附录 |
| 附录A RETHER协议脚本文件 |
| 附录B RETHE协议SQO版本脚本文件 |
| 附录C RETHER协议验证性质 |
| 附录D RETHER协议SQO版本RTF性质验证反例 |
| 在学期间发表论文 |
| 致谢 |
（8）带实时的传值与移动系统研究（论文提纲范文）
| 摘要 |
| 第一章 引言 |
| 1.1 并发系统 |
| 1.2 实时系统 |
| 1.3 形式化验证 |
| 1.4 本文的目标、贡献和组成 |
| 第二章 实时传值系统的计算模型 |
| 2.1 实时传值系统现状 |
| 2.2 时间符号迁移图(TSTG) |
| 第三章 实时传值系统上的等价关系 |
| 3.1 几种重要的互模拟 |
| 3.2 基于等价类划分的判定方法 |
| 3.2.1 域(Region)等价 |
| 3.2.2 时间抽象互模拟的判定方法 |
| 3.2.3 时间互模拟的判定方法 |
| 3.2.4 时间互模拟算法及其正确性证明 |
| 3.2.5 无穷数据域及其他情况的处理 |
| 第四章 连续时间的数据表示和操作 |
| 4.1 时间区域的表示方法 |
| 4.1.1 DBM |
| 4.1.2 更一般的“区”的表示 |
| 4.2 范式化与信息消冗 |
| 第五章 实时传值系统上的模型检测 |
| 5.1 模型检测简介 |
| 5.2 基本约定 |
| 5.3 基于可达性分析的模型检测 |
| 5.4 验证工具及实现 |
| 5.5 协议验证实例分析-限时重传协议 |
| 5.5.1 文件传输服务 |
| 5.5.2 使用RealM建模和验证 |
| 5.6 更一般的模型检测 |
| 5.6.1 一阶谓词实时μ演算 |
| 5.6.2 布尔图 |
| 5.6.3 一个局部算法 |
| 5.6.4 数据无关变量处理 |
| 第六章 实时移动进程演算 |
| 6.1 移动进程演算简介 |
| 6.2 语法和语义 |
| 6.3 强实互模拟和强互模拟关系 |
| 6.4 弱实互模拟和弱互模拟关系 |
| 6.5 公理化 |
| 6.5.1 强实互模拟的公理化 |
| 6.5.2 强互模拟的公理化 |
| 第七章 结论 |
| 7.1 总结以及相关工作讨论 |
| 7.2 进一步工作的讨论 |
| 参考文献 |
| 攻读博士学位论文期间发表和录用的文章 |
| 致谢 |
| 附录A RealM接收语言的语法定义 |
四、时间符号迁移图上的可达性分析（论文参考文献）
- [1]基于复杂网络的公共自行车关键节点选取和网点布设优化研究[D]. 吕铃. 江西师范大学, 2019(01)
- [2]公共自行车复杂网络可达性指标潜力评价模型[J]. 吕铃,彭雅丽,曾欣怡,杨雨鑫,黄明和. 计算机工程与科学, 2018(01)
- [3]扩展π演算的建模、验证与测试[D]. 罗玲. 西安电子科技大学, 2015(03)
- [4]面向跨组织业务协作的角色网络模型研究[D]. 马俊锋. 大连理工大学, 2010(05)
- [5]离散实时Mobile Ambients[D]. 刘荣胜. 湖南师范大学, 2007(06)
- [6]基于STGA的并发程序测试[D]. 唐江峻. 中国科学院研究生院（软件研究所）, 2004(03)
- [7]并发传值进程模型检测工具的数据类型扩展[D]. 张轶. 中国科学院研究生院（软件研究所）, 2003(01)
- [8]带实时的传值与移动系统研究[D]. 陈靖. 中国科学院研究生院（软件研究所）, 2003(01)
- [9]时间符号迁移图上的可达性分析[J]. 陈靖. 计算机学报, 2003(01)