题名 基于TLA的UML模型形式化验证
被引量：3
1
作者
梁盟磊 王小平 薛小平 李刚
机构
同济大学电子与信息工程学院计算机科学与技术系 同济大学电子与信息工程学院信息与通信工程系
出处
《计算机工程》
CAS
CSCD
北大核心
2011年第2期72-74,共3页
基金
国家自然科学基金资助项目(60972036)
文摘
统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。
关键词
形式化方法 形式化验证 统一建模语言 行为时序逻辑
Keywords
formal method formal verification UML temporal logic of actions （tla ）
分类号
TP391
[自动化与计算机技术—计算机应用技术]
题名 并发系统中谓词行为图的行为时序逻辑表达
2
作者
黄贻望 袁科
机构
铜仁学院数学与计算机科学系 武汉大学计算机学院软件工程国家重点实验室 南开大学信息技术科学学院
出处
《计算机应用研究》
CSCD
北大核心
2013年第9期2752-2754,共3页
基金
中央高校基本科研业务费专项资金资助项目(2012211020201) 贵州省科学技术厅 +3 种基金 铜仁市科学技术局 铜仁学院联合基金资助项目(黔科合J字LKT[2012]04号 黔科合J字LKT[2012]24号) 铜仁学院科研启动基金资助项目(TS10013)
文摘
行为时序逻辑(TLA)组合时序逻辑与行为逻辑,可以对并发系统进行描述与验证,它引入动作和行为的概念,使得系统和属性可用它的规约公式表示,但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图,对于并发转移可以用谓词行为图进行图形化表示,谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则,用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性,并用系统规约的TLA公式对谓词行为图表达能力进行证明,表明两者具有等价性,为描述和分析并发转换系统提供了一种可行的方法。
关键词
并发性 规约 谓词行为图 行为时序逻辑
Keywords
concurrent reduction predicate behavior graph temporal logic of actions （tla ）
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
题名 行为时序逻辑与自反线性时序逻辑的关系
3
作者
白金山 冯天亮 吴应江 丘文峰 王梦
机构
广东医学院信息工程学院
出处
《现代计算机（中旬刊）》
2014年第1期3-7,共5页
基金
广东医学院博士启动基金(No.B2011006)
文摘
为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中,对行为时序逻辑公式的语义进行形式化定义,从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系,提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念,定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统,以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。
关键词
模型检测 行为时序逻辑 语义 语法 自反性
Keywords
Model Checker temporal logic of actions （tla ） Semantics Syntax Reflective
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
题名 基于动作时序逻辑的Web服务组合
4
作者
周倩朝 史衍琪 刘卫红
机构
东南大学计算机科学与工程学院 安徽工业大学计算机学院
出处
《计算机应用与软件》
CSCD
2010年第12期142-144,173,共4页
文摘
为了更有效地实现Web服务组合,提出一种使用动作时序逻辑TLA(Temporal Logic of Actions)进行Web服务组合的方法。Web服务组合与工作流有着共同特征,首先根据工作流的基本控制模式,将服务之间的关系用TLA进行描述,然后提出了基于图的宽度优先搜索的Web服务自动组合算法,并采用TLA模型检验器TLC验证组合逻辑的正确性以及是否存在死锁问题,最后给出了现有的Web服务组合平台BPEL4WS向TLA转化的方法。
关键词
动作时序逻辑 BPEL4WS WEB服务组合
Keywords
temporal logic of actions （ tla ） BPEL4WS（ Business Process Execution Language for Web Services） Web service composition
分类号
TP393.4
[自动化与计算机技术—计算机应用技术]
题名 基于TLA的事件图模型形式化验证方法
被引量：4
5
作者
夏薇 姚益平 慕晓冬
机构
国防科学技术大学计算机学院 第二炮兵工程学院计算机系
出处
《计算机应用研究》
CSCD
北大核心
2011年第11期4171-4173,4187,共4页
基金
国家自然科学基金资助项目(60773019) 国家博士点基金资助项目(200899980004)
文摘
针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logicof action,TLA)的事件图模型形式化验证方法。该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型检验工具进行验证。这种方法不仅能够有效提高仿真模型的正确性,而且能够提高模型的可重用性,简化仿真模型建模与验证过程。最后利用TLA模型检验工具对实例进行了验证,实验结果表明了该方法的有效性。
关键词
仿真模型 验证、确认和认定 模型检验 行为时态逻辑 事件图
Keywords
simulation models verification validation ＆ accreditation（VV＆A） model checking temporal logic of action （tla ） event graph
分类号
TP391
[自动化与计算机技术—计算机应用技术]
题名 普适计算环境中基于上下文的使用控制模型
被引量：1
6
作者
武海鹰
机构
武警工程学院通信工程系
出处
《计算机工程》
CAS
CSCD
2012年第5期281-284,共4页
基金
武警工程学院基础理论研究基金资助项目(WJY201021)
文摘
使用控制模型可以解决普适计算环境中访问控制的动态授权问题,但该模型没有考虑上下文信息。为此,提出一种普适计算环境中基于上下文的使用控制模型。在使用决策因素中增加上下文信息,包括时间、位置和环境因素,采用行为时态逻辑定义模型的核心规则集。以基于普适计算的智能教室为实例进行分析,证明该模型在普适计算环境中的有效性。
关键词
普适计算 访问控制 使用控制 上下文 行为时态逻辑
Keywords
pervasive computing access control Usage Control（UCON） context temporal logic of action （tla ）
分类号
TP309
[自动化与计算机技术—计算机系统结构]
题名 采用动作时序逻辑的Web服务组合方法
被引量：2
7
作者
周宁 刘慧 王红兵 谢俊元
机构
南京大学计算机软件新技术国家重点实验室 南京大学计算机科学与技术系 东南大学计算机科学与工程学院
出处
《计算机科学与探索》
CSCD
2011年第3期208-220,共13页
基金
国家自然科学基金 国家教育部重点项目 江苏省科技支撑计划~~
文摘
基于有限状态自动机理论,将Web服务建模成一个有限状态自动机。针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展,提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法,从而可以用TLA对服务行为进行形式化描述和规范,为描述Web服务提供了一个新的方法。讨论了在动作时序逻辑中,服务组合时各组件服务的有限状态自动机的组合方式,以及伴随着服务组合,单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题,并在此基础上,提出了实现TLA规范正确组合的算法思想。
关键词
网络服务组合 动作时序逻辑(tla ) 网络服务描述语言(WSDL) 有限状态自动机(FSA)
Keywords
Web services composition temporal logic of action （tla ） Web services description language（WSD L） finite state automata（FSA）
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
