%0 Journal Article
%T 基于线性时序逻辑的实时系统模型检查
%A 李广元？
%A 唐稚松？
%J 软件学报
%P 193-202
%D 2002
%X 模型检查是一种用于并发系统的性质验证的算法技术.ltlc(lineartemporallogicwithclocks)是一种连续时间时序逻辑,它是线性时序逻辑ltl的一种实时扩充.讨论实时系统关于ltlc公式的模型检查问题,将实时系统关于ltlc公式的模型检查化归为有穷状态转换系统关于ltl公式的模型检查,从而可以利用ltl的模型检查工具来对ltlc进行模型检查.由于ltlc既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑ltlc的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.
%K 实时系统
%K 时间自动机
%K 线性时序逻辑
%K 模型检查
%K 性质验证
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20020205&flag=1