基于TLA的SaaS业务流程定制及验证机制研究

SaaS模式已成为当前流行的软件服务形式.为满足不同租户个性化的业务服务需求,SaaS模式必须提供灵活的定制机制.为此,提出了一个支持租户业务流程定制行为建模及验证的框架.该框架以层次定制行为约束图作为定制指导,通过TLA(Temporal Logic of Actions)对各层的原子定制活动建模,并以此为基础构建租户的全局定制行为,然后基于应用的业务规则约束设计算法验证全局定制行为的正确性;为有效提高租户的定制效率,基于对多租户已有正确定制结果的统计分析,设计定制推荐算法,合理减少验证次数.仿真实验结果证实了该机制的高效性及可靠性.

基于TLA的UML模型形式化验证

统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。

基于TLA的事件图模型形式化验证方法

针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logicof action,TLA)的事件图模型形式化验证方法。该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型检验工具进行验证。这种方法不仅能够有效提高仿真模型的正确性,而且能够提高模型的可重用性,简化仿真模型建模与验证过程。最后利用TLA模型检验工具对实例进行了验证,实验结果表明了该方法的有效性。

行为时态逻辑TLA定理系统证明及公平性研究

行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向。为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统。在此基础上严格的证明了TLA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件。最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型。

基于TLA+的AFDX冗余管理算法的改进

为了在航空应用中得到更加安全可靠的通讯系统,就目前普遍应用的标准以太网可能会出现的问题,提出了用行为时序逻辑TLA对AFDX冗余管理算法进行形式化分析。在适当的环境中,根据安全性、活性、可用性3个性质,得到两个冗余管理的推论,根据这些性质和推论,提出了3个冗余管理算法,并用TLA+语言进行详细的描述。通过模型检测,表明出RMA13为最优算法。

基于行为时序逻辑TLA的安全协议形式化分析与检测

随着近年来网络协议的不安全性,对安全协议进行形式化分析与检测则显的非常重要。而基于行为时序逻辑TLA的模型检测是形式化分析检测方法中重要的一种。本文主要采用基于TLA的HLPSL语言形式化分析与检测H.530协议。

一种基于TLA的解决N皇后问题的方法

行为时序逻辑语言(TLA+)是一种在模型检测范围内能够表达模型程序和逻辑规约的语言。N皇后问题是一个久远的问题,回溯法是解决该问题一种经典的方法。本文提出如何用行为时序逻辑语言TLA+去描述N皇后问题,然后使用Toolbox工具去检测n=5时该问题的全部解。

基于用户同意的隐私保护协议形式化描述与验证

将用户同意与访问控制相结合是解决隐私保护的主要方法之一.然而,现有的隐私保护访问控制方法仅从数据控制者的角度,不考虑个人对访问决策的参与,无法满足自主可控的需求.为了解决这个问题,本文提出了一种基于用户同意的隐私保护访问控制协议,将用户同意转化为一种同意权限,形成一种同意加授权的双重访问控制机制.本文给出协议的语法、语义及安全性定义和分析,并采用模型检测的方法对协议应满足的性质进行验证,最终证明本文的设计可以从访问控制的角度满足个人信息保护法规的要求.

行为时序逻辑中公平性的研究与完善

基于行为时序逻辑(TLA)的并发系统描述,就是对系统的初始状态、系统行为和行为的公平性进行规约和描述,但TLA中的公平性具有局限性,无法准确地描述某些系统的行为,从而限制了TLA的描述能力。通过研究TLA中公平性的推导过程,分析公平性的概念与定义方法,并以实际例子说明它的局限性。在此基础上,提出以加入两级新的公平性方式对其进行完善。最后,证明了新公平性等级之间的蕴涵关系。完善后的公平性具有更强的描述能力,能够对系统进行更完整的描述与规约。

基于行为时序逻辑的入侵取证研究

提出一种基于行为时序逻辑的入侵取证的形式化方法,其描述语言能够准确描述入侵证据、系统知识以及攻击行为,并具有在部分数据缺失的情况下进行非确定性推理的能力;其自动验证工具能够寻求额外的证据并可检查是否有可能的攻击与这些证据相符。实例研究表明,这种方法不依赖于具体的攻击技术和操作系统,不惧证据的缺失,能够有效搜寻更多的证据并重建可能的攻击场景。

基于时空单词的两人交互行为识别方法

文中提出一种基于时空单词的两人交互行为识别方法,该方法从行为视频中提取丰富的时空兴趣点,基于人体剪影的连通性分析和时空兴趣点的历史信息,把时空兴趣点划分给不同的人体,并在兴趣点样本空间聚类生成时空码本(spatial-temporal codebook).对于给定的时空兴趣点集,通过投票得到表示单人原子行为的时空单词(spatial-temporal words).采用条件随机场模型建模单人原子行为,在两人交互行为的语义建模过程中,人工建立表示领域知识(domain knowledge)的一阶逻辑知识库,并训练马尔可夫逻辑网用以两人交互行为的推理.两人交互行为库上的实验结果证明了该方法的有效性.

可判定的时序动态描述逻辑

动态描述逻辑DDL(dynamic description logic)提供了一种基于描述逻辑的动作理论,适用于语义Web环境下对动态领域知识的刻画和推理.为了将分支时序逻辑的刻画能力引入到动态描述逻辑中,将时间的进展体现为原子动作的执行,从而将时序维与动态维统一起来.在此基础上,从描述逻辑ALCQIO出发构建了一个时序动态描述逻辑TDALCQIO,给出了TDALCQIO的Tableau判定算法,并证明了算法的可终止性和正确性.TDALCQIO不仅兼容了构建在描述逻辑ALCQIO基础上的动态描述逻辑的刻画和推理能力,而且还可从可达性、安全性等角度对整个动态领域的时序特征进行刻画和推理,从而为语义Web环境下对动态领域知识的刻画和推理提供了进一步的逻辑支持.

时态数据库时间轴的动态逻辑模型

尽管在1994年,Gabbay等人论证了时态逻辑的公理化系统和证明论方法是不适合于时态数据库查询语言建模的,但是仍需要通过对时间轴的公理化建模,利用公理化系统的可靠和完全等性质对时间轴作"细精度"的语义刻画.只有这样才能准确地在数据库中反映时间和时间属性的本质特点,并应用于与时间轴模型直接相关的时态查询语言.因此,从分析时间轴的性质出发,对时间轴的序关系和谓词逻辑性质进行了研究和阐述.随后分别用经典的时态逻辑Tense Logic和动态逻辑对时态数据库的时间轴进行了公理化建模,这样刻画的目的是为了"细精度"地体现时间轴的特点,并借助逻辑的方法对其分析.在TDB(temporal database)时间轴的动态逻辑建模部分,相对于原时态逻辑系统较为静态,着重处理了时间的动态性,并参照了TenseLogic中的Lin.Z系统,将其转化为动态Lin.Z系统,在其中添加了参数化处理.该参数化的处理是基于动作执行的,主要工作在动作指数的数值化和函数化两个方面,其结果体现了时态数据库中规则生存周期和"Now"节点的一些特点以及知识表达和解决方法,研究结果将对后续时态知识表达和时态数据库查询语言的研究起到积极的作用.

交互式用户界面的形式化描述与性质验证

随着人机交互技术的发展，计算机和用户之间的接口越来越自然，但用户界面管理系统内部的复杂度却大大地增加了.目前提出的新一代用户界面的模型大都停留在概念模型阶段，缺乏对模型的严格描述和证明.该文结合对基于自然交互方式的用户界面的研究成果，归纳出了一个交互式用户界面的通用模型．为了保证系统设计的正确性，文章讨论了如何使用形式化描述语言LOTOS（languageoftemporalorderingspecification）和基于动作的时序逻辑ACTL（actionbasedtemporallogical）对系统进行描述与验证，这有利于人们对交互式用户界面的动态行为进行研究、评估与定义．

采用动作时序逻辑的Web服务组合方法

基于有限状态自动机理论,将Web服务建模成一个有限状态自动机。针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展,提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法,从而可以用TLA对服务行为进行形式化描述和规范,为描述Web服务提供了一个新的方法。讨论了在动作时序逻辑中,服务组合时各组件服务的有限状态自动机的组合方式,以及伴随着服务组合,单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题,并在此基础上,提出了实现TLA规范正确组合的算法思想。

描述逻辑的动态时序扩展

在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTLALC公式可满足性。利用该类扩展,可以表达组合动作执行过程中域变化的时间特性,该类扩展为语义Web服务等动态应用建模和推理提供了一条有效途径。

基于时间区间的并行行为与并发事件逻辑

在基于时间区间的时态逻辑基础上,提出了一种处理主体并行行为与并发事件的逻辑理论框架。文章提出的逻辑系统将事件与动作置于同一个逻辑体系下,以时间区间为基础,深入分析了二者之间的关系,充分发挥了事件的作用,动作的描述得到简化。文章给出了逻辑系统的语法和语义描述,还提出了基于领域描述结构的并发事件冲突消解方法。

基于时序逻辑的工作流建模与分析方法

提出了一种基于活动时序逻辑（TLA）的工作流建模与模型分析的形式化方法。该方法将模型及模型的性质都表示为一个，TLA公式，对工作流模型性质的分析可以等价为对，TLA中两个公式之间是否存在蕴涵关系的检验，从而建立了一个工作流模型各层次分析统一框架。一个工作流建模和分析的实例验证了所提出方法的有效性，该方法在建模、模型分析以及指导模型设计等方面都有较好的应用前景。

普适计算环境中基于上下文的使用控制模型

使用控制模型可以解决普适计算环境中访问控制的动态授权问题,但该模型没有考虑上下文信息。为此,提出一种普适计算环境中基于上下文的使用控制模型。在使用决策因素中增加上下文信息,包括时间、位置和环境因素,采用行为时态逻辑定义模型的核心规则集。以基于普适计算的智能教室为实例进行分析,证明该模型在普适计算环境中的有效性。

一种安全转移系统模型的构造及其运用

为提高安全性,一般利用密码技术,但系统运行过程的安全尚显不足,为此基于行为时序逻辑TLA提出一种安全转移系统模型。通过设置安全属性,构造安全行为,使得系统在运行过程中的每次转移都满足安全属性,从而提高过程的安全性。为此,定义初始安全态、安全转移条件、安全状态、安全行为、安全运迹和安全转移系统,并证明在安全转移系统中状态处处安全。安全转移系统中强调的是系统转移过程的安全性,从而增强了系统运行的安全。通过实例的运用表明面向过程安全的建模为提高系统的安全性是有意义的。