期刊文献+
共找到17篇文章
< 1 >
每页显示 20 50 100
A unified linear-time temporal logic solution to the steam-boiler control specification problem
1
作者 闫安 唐稚松 《Science China(Technological Sciences)》 SCIE EI CAS 1999年第3期244-251,共8页
The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole process of program development, i.e. from the abstract specification to... The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole process of program development, i.e. from the abstract specification to the efficiently executable program in a formal, precise and convenient way. The steam boiler control specification problem, a large case study in the fields of real time, hybrid and communication systems, is discussed with XYZ/E. The approach covers physical model construction, formal specification, stepwise refinement, verification, executable program and visual user interface programming. 展开更多
关键词 temporal logic language hybrid real-time system XYZ/E program specification STEPWISE REFINEMENT verification.
原文传递
Hybridity in Embedded Computing Systems
2
作者 虞慧群 孙永强 《Journal of Computer Science & Technology》 SCIE EI CSCD 1996年第1期90-96,共7页
An embedded system is a system that computer is used as a componelit ina larger device. In this paper, we study hybridity in embedded systems andpresent an interval based temporal logic to express and reason about hyb... An embedded system is a system that computer is used as a componelit ina larger device. In this paper, we study hybridity in embedded systems andpresent an interval based temporal logic to express and reason about hybridproperties of such ldnd of systems. 展开更多
关键词 embedded systems hybridity temporal logic specification verification
原文传递
一种使用STL逻辑监控CPS的可解释规范挖掘方法
3
作者 刘峰 曹子宁 +1 位作者 王福俊 李振 《小型微型计算机系统》 CSCD 北大核心 2024年第1期9-15,共7页
随着信息物理融合系统(CPS)日益复杂,很难捕获其相关行为并以一种可解释的方式检测它.因此本文提出了一种基于线性支持向量机(LSVM)框架的规范挖掘算法,从有限长度的信号轨迹中挖掘具有可解释性的信号时序逻辑(STL)公式.挖掘出的STL公... 随着信息物理融合系统(CPS)日益复杂,很难捕获其相关行为并以一种可解释的方式检测它.因此本文提出了一种基于线性支持向量机(LSVM)框架的规范挖掘算法,从有限长度的信号轨迹中挖掘具有可解释性的信号时序逻辑(STL)公式.挖掘出的STL公式可以作为监控行为的抽象,用于CPS运行时验证的监控机制中.该算法根据一组被标记的有限时间轨迹和STL模板公式,将信号时序逻辑特有的鲁棒性满意度与LSVM的优化算法相结合生成所需规范.另外,本文还将对一维信号轨迹的规范挖掘技术扩展到多维信号上.最后,通过两个案例研究来说明提出算法的可行性和优势,结果表明该算法在保证高准确率的前提下,执行效率和可解释性都优于其他的规范挖掘算法. 展开更多
关键词 机器学习 规范挖掘 运行时验证 信息物理融合系统 信号时序逻辑
下载PDF
带有时钟变量的线性时序逻辑与实时系统验证 被引量:16
4
作者 李广元 唐稚松 《软件学报》 EI CSCD 北大核心 2002年第1期33-41,共9页
为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系... 为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精. 展开更多
关键词 实时系统 线性时序逻辑 系统描述语言 性质验证 时钟变量 计算机控制系统
下载PDF
开放式体系结构数控系统实时性的建模与分析 被引量:5
5
作者 曹宇男 张辉 +1 位作者 叶佩青 王田苗 《机械工程学报》 EI CAS CSCD 北大核心 2011年第1期108-116,共9页
给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)... 给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)。TTM/ATRTTL提供一整套方法用于对OAC系统的硬实时性和反馈特性进行建模并使用该形式化方法在系统层对OAC系统进行建模。分别给出开环OAC,系统级逻辑控制器以及任务间通信和同步机制的TTM模型,并最终给出具有调度机制的闭环OAC系统TTM模型。该模型为系统验证体系结构的基础。最后,给出系统验证体系结构并用模型验证工具STeP和CAD工具SF2STeP实现之。在系统验证过程中,首先解决STeP中遇到的若干模型验证问题,这些问题包括重写规则,验证规则,状态爆炸问题,以及时间约束限制问题。通过模型验证试验解决OAC系统运行过程中出现的死锁以及系统各模块执行时间约束检验问题。试验结果表明该方法可以有效地对OAC系统进行建模并对系统的实时特性进行验证。 展开更多
关键词 开放式体系结构数控系统 形式化描述与验证方法 时间转化模型/全时轴实时时态逻辑 实时性 建模
下载PDF
混合投影时序逻辑与混合系统的形式化验证 被引量:4
6
作者 张海宾 段振华 《计算机科学》 CSCD 北大核心 2007年第11期279-282,共4页
为了描述混合系统的性质和行为,10多年来,各种时序逻辑,如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范,但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑(Hybrid Projection Tempora... 为了描述混合系统的性质和行为,10多年来,各种时序逻辑,如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范,但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑(Hybrid Projection Temporal Logic,简称HPTL),既能刻画混合系统的性质,又能表示混合系统的实现。这样,混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时,给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。 展开更多
关键词 混合系统 混合自动机 区间时序逻辑 形式化验证
下载PDF
基于XYZ/E描述和验证容错系统 被引量:5
7
作者 郭亮 唐稚松 《软件学报》 EI CSCD 北大核心 2002年第5期913-920,共8页
研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序PF;基于P,F和恢复算法R,通过容错转换给出容错程序PF-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢... 研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序PF;基于P,F和恢复算法R,通过容错转换给出容错程序PF-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质. 展开更多
关键词 验证 容错系统 时序逻辑语言 XYZ/E语言 软件系统
下载PDF
一种面向软件工程的时序逻辑语言 被引量:15
8
作者 唐稚松 赵琛 《软件学报》 EI CSCD 北大核心 1994年第12期1-16,共16页
XYZ系统由时序逻辑语言XYZ/E及一组基于该语言的CASE工具集组成.XYZ/E语言的目的是欲使逐步求精,描述及验证、快速原型等一些软件工程方法更加有效.特别地,它还能表示实时通信进程中的动态成分.在统一的框架下,... XYZ系统由时序逻辑语言XYZ/E及一组基于该语言的CASE工具集组成.XYZ/E语言的目的是欲使逐步求精,描述及验证、快速原型等一些软件工程方法更加有效.特别地,它还能表示实时通信进程中的动态成分.在统一的框架下,不仅能表示不同层次的抽象描述,而且能表示普通高级语言的各种重要性质.本文是关于这一时序逻辑语言最新、最完整的介绍. 展开更多
关键词 软件工程 时序逻辑语言 CASE
下载PDF
分布实时系统的概率规范和证明形式化
9
作者 罗铁庚 陈火旺 齐治昌 《计算机科学》 CSCD 北大核心 1995年第6期16-18,共3页
1引言 随着数字系统变得越来越小、越来越便宜,它们用于物理过程控制和与物理过程互协作的机会将越来越多。互相协作的过程如果出现意外行为,后果将可能很严重。
关键词 实时系统 概率规范 证明形式化 操作系统
下载PDF
用于反应系统的修改时序逻辑
10
作者 贾国平 郑国梁 《软件学报》 EI CSCD 北大核心 1997年第9期663-672,共10页
本文提出了一个用于反应系统规范及验证的修改时序逻辑.它包含一个用于显示区分程序执行步同环境执行步的机制.环境的特性可以在系统开发时进行考虑.文中首先给出了程序的一个可复合计算模型──模块转换系统.基于此模型,给出了修... 本文提出了一个用于反应系统规范及验证的修改时序逻辑.它包含一个用于显示区分程序执行步同环境执行步的机制.环境的特性可以在系统开发时进行考虑.文中首先给出了程序的一个可复合计算模型──模块转换系统.基于此模型,给出了修改时序逻辑以及它的证明规则.本文提出的方法基于Manna-Pnueli的时序逻辑框架.经典的资源分配问题的例子用于说明此方法.最后给出了并行复合原理,它可以看成是Abadi和LamPort的关于复合假设/保证规范研究工作的具体应用. 展开更多
关键词 反应系统 时序逻辑 模块转换系统 软件开发
下载PDF
一个统一的程序验证框架
11
作者 贾国平 郑国梁 《软件学报》 EI CSCD 北大核心 1997年第2期107-114,共8页
本文提出了一个简单的方法,其中程序和其性质都由一个逻辑:时序逻辑中的公式表示.文中给出了一个程序的转换模块的定义,提出了时序执行语义的概念.它是一个时序公式,精确地说明了一个程序.将时序逻辑作为规范语言,程序正确性就... 本文提出了一个简单的方法,其中程序和其性质都由一个逻辑:时序逻辑中的公式表示.文中给出了一个程序的转换模块的定义,提出了时序执行语义的概念.它是一个时序公式,精确地说明了一个程序.将时序逻辑作为规范语言,程序正确性就意味着说明程序的公式蕴含说明性质的公式,其中蕴含即为一般的逻辑蕴含.因此,本文的方法为并发程序的规范及验证提供了一个统一的框架.它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统.一个缓冲系统的简单例子用来说明本文的方法. 展开更多
关键词 程序验证 规范 程序正确性
下载PDF
基于 XYZ/ E的混成系统(英文) 被引量:3
12
作者 阎安 唐稚松 《软件学报》 EI CSCD 北大核心 2000年第1期1-7,共7页
混成系统是由计算机和物理设备组成的嵌入式实时计算系统 .它允许在交互式实时系统中引入连续变化的单元 .XYZ/ E是基于 Manna- Pnueli的线性时序逻辑的程序设计语言 .它将程序的动态语义与静态语义统一在同一框架中 ,支持从抽象的程序... 混成系统是由计算机和物理设备组成的嵌入式实时计算系统 .它允许在交互式实时系统中引入连续变化的单元 .XYZ/ E是基于 Manna- Pnueli的线性时序逻辑的程序设计语言 .它将程序的动态语义与静态语义统一在同一框架中 ,支持从抽象的程序规范到可执行代码的逐步求精的全过程 .该文使用 XYZ/ E语言描述和验证混成系统 .首先介绍了计算模型 ,然后介绍了 XYZ语言对混成系统的形式化描述 ,最后介绍了混成系统的验证 .与同类工作相比 ,XYZ/ E支持状态转换 ,从而可以方便地描述复杂的控制算法 . 展开更多
关键词 混成系统 时序逻辑语言 程序规范 XYZ/E语言
下载PDF
一个命题投影时序逻辑符号模型检测器 被引量:3
13
作者 逄涛 段振华 刘晓芳 《软件学报》 EI CSCD 北大核心 2015年第8期1968-1982,共15页
现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection tempora... 现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection temporal logic,简称PPTL)符号模型检测工具——PLSMC(PPTL symbolic model checker)的设计与实现过程.该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证. 展开更多
关键词 符号模型检测 时序逻辑 模型检测器 嵌入式系统验证
下载PDF
在 XYZ/ E中实现混成实时系统——蒸气锅炉控制问题的解决(英文) 被引量:3
14
作者 闫安 唐稚松 《软件学报》 EI CSCD 北大核心 2000年第6期711-719,共9页
XYZ/E is a temporal logic system as well as a programming language. The temporal logic language XYZ/E can represent both high level and low level specifications in the same framework, so that the specification and imp... XYZ/E is a temporal logic system as well as a programming language. The temporal logic language XYZ/E can represent both high level and low level specifications in the same framework, so that the specification and implementation of software systems are very convenient. A specification and an implementation of the Steam Boiler Control Specification Problem in XYZ/E is presented in this paper. A visual user interface is also implemented. 展开更多
关键词 时序逻辑语言 混成实时系统 描述 XYZ/E
下载PDF
铁路系统的模型检查和参数分析 被引量:1
15
作者 鲍峥嵘 虞慧群 +1 位作者 邵志清 宋国新 《华东理工大学学报(自然科学版)》 CAS CSCD 北大核心 1999年第2期182-187,共6页
研究铁路系统的自动验证技术。建立火车和控制器的混合自动机模型,用时态逻辑ICTL描述铁路系统的性质规范,使用模型检查技术自动验证铁路系统,并且对铁路系统的一些参数进行分析。
关键词 嵌入式系统 铁路系统 模型检查 参数分析 安全性
下载PDF
数字系统投影时序逻辑描述及验证 被引量:1
16
作者 张鹏飞 叶永升 《淮北师范大学学报(自然科学版)》 CAS 2013年第4期61-66,共6页
投影时序逻辑是一种具有离散时间模型的时序逻辑,其部分子集又是一种程序设计语言,可处理顺序和并发计算.文章讨论应用投影时序逻辑对数字系统进行形式描述和验证的方法,该方法可在数字系统的不同层级设计过程中,使用投影时序逻辑对其... 投影时序逻辑是一种具有离散时间模型的时序逻辑,其部分子集又是一种程序设计语言,可处理顺序和并发计算.文章讨论应用投影时序逻辑对数字系统进行形式描述和验证的方法,该方法可在数字系统的不同层级设计过程中,使用投影时序逻辑对其系统行为和性质进行形式化的描述及验证,从而提高系统设计的可信性. 展开更多
关键词 投影时序逻辑 形式化描述 系统验证
下载PDF
基于嵌入式可信平台的运行时监控方法
17
作者 孙召昌 马建峰 +1 位作者 孙聪 卢笛 《网络与信息安全学报》 2017年第10期44-51,共8页
当前可信计算平台缺乏对自身运行时安全属性的监控,对此,提出一种针对嵌入式可信平台的运行时监控方法。通过自动化的代码插入和运行时实时监控,保证可信平台的运行时安全功能符合设计规范,并保证系统性能和运行状态符合特定条件约束,... 当前可信计算平台缺乏对自身运行时安全属性的监控,对此,提出一种针对嵌入式可信平台的运行时监控方法。通过自动化的代码插入和运行时实时监控,保证可信平台的运行时安全功能符合设计规范,并保证系统性能和运行状态符合特定条件约束,同时对相应的异常进行实时处理。实验结果表明,随着监控节点数的增长,监控的准确性和实时性提高,而监控开销和异常处理开销处于合理范围。 展开更多
关键词 可信计算 运行时监控 嵌入式系统 线性时序逻辑
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部