| 带有时钟变量的线性时序逻辑与实时系统验证 |
| |
| 引用本文： | 李广元,唐稚松.带有时钟变量的线性时序逻辑与实时系统验证[J].软件学报,2002,13(1):33-41. |
| |
| 作者姓名： | 李广元 唐稚松 |
| |
| 作者单位： | 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 |
| |
| 基金项目： | 国家自然科学基金资助项目(60073020);国家"九五"重点科技攻关项目(98-780-01-07-01);国家863高科技发展计划资助项目(863-306-ZT02-04-1) |
| |
| 摘 要： | 为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.
|
| 关 键 词： | 实时系统 时间自动机 线性时序逻辑 规范语言 系统描述语言 性质验证 |
| 文章编号： | 1000-9825/2002/13(01)0033-09 |
| 收稿时间： | 2000/7/20 0:00:00 |
| 修稿时间： | 2000年7月20日 |
A Linear Temporal Logic with Clocks for Verification of Real-Time Systems |
| |
| LI Guang-yuan; and TANG Zhi-song.A Linear Temporal Logic with Clocks for Verification of Real-Time Systems[J].Journal of Software,2002,13(1):33-41. |
| |
| Authors: | LI Guang-yuan; and TANG Zhi-song |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
