计算机科学 ›› 2017, Vol. 44 ›› Issue (Z6): 571-574.doi: 10.11896/j.issn.1002-137X.2017.6A.128
张春燕,孙俊
ZHANG Chun-yan and SUN Jun
摘要： 带数据约束的概率实时系统是指一种既带有概率时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个概率模型中的规范及验证研究较少。提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的概率ZIA规范,并给出了它的时序逻辑。对于CTL和PCTL而言,尽管这些逻辑很强大,但是只能反映时序性质,因此提出一个新的形式化语言CTML来表达度量性质查询,同时保留表达时序性质的能力并给出概率ZIA规范的验证算法。
| [1] 李广元,唐稚松.带有时钟变量的线性时序逻辑与概率实时系统验证[J].软件学报,2002,13(1):33-41. [2] 戎玫,张广泉.模型检测新技术研究[J].计算机科学,2003,30(5):102-104. [3] BRARD B,BIDOIT M,FINKEL A,et al.Systems and software verification:model-checking techniques and tools[M].Springer Publishing Company,Incorporated,2010. [4] 王晶,戎玫,张广泉,等.基于概率模型检测的 Web 服务组合验证[J].计算机科学,2012,39(1):120-123. [5] CAO Z,WANG H.Extending interface automata with z notation[M]∥Fundamentals of Software Engineering.Springer Berlin Heidelberg,2012:359-367. [6] CAO Z,WANG H.Hybrid ZIA and its Approximated Refinement Relation[C]∥Proceedings of the 6th International Confe-rence on Evaluation of Novel Approaches to Software Enginee-ring.Beijing,China,2011:260-265 [7] 狄杨思.形式规范的自动验证算法的研究[D].南京:南京航空航天大学,2012. [8] 狄杨思,曹子宁,王辉.一种基于形式规范ZIA的自动验证方法[J].光电与控制,2011,18(增刊):113-120. [9] CLARKE E M,GRUMBERG O,PELED D A.Model checking[M].MIT Press,1999. [10] 周从华,刘志锋,王昌达.概率计算树逻辑的限界模型检测[J].软件学报,2012,3(7):1656-1668. [11] MINER A S,JING Y.A formal language toward the unification of model checking and performance evaluation[M]∥Analytical and Stochastic Modeling Techniques and Applications.Springer Berlin Heidelberg,2010:130-144. [12] KOYMANS R.Specifying message passing and time-critical systems with temporal logic[M].Springer,1992. [13] EMERSON E A,MOR A K,SISTLA A P,et al.Quantitative temporal reasoning[M]∥Computer-Aided Verification.Springer Berlin Heidelberg,1991:136-145. [14] ALUR R,DILL D L.A theory of timed automata[J].Theoretical computer science,1994,126(2):183-235. [15] ALUR R.Timed automata[M]∥Computer Aided Verification.Springer Berlin Heidelberg,1999:8-22. [16] ALUR R.Techniques for automatic verification of real-time systems[D].Stanford University,1991. [17] ALUR R,COURCOUBETIS C,DILL D.Model-checking forreal-time systems[C]∥Fifth Annual IEEE Symposium on Logic in Computer Science,1990(LICS’90).IEEE,1990:414-425. [18] 钱俊彦,赵岭忠,古天龙.一种基于时间自动机的时钟等价性优化方法[J].计算机工程,2005,31(18):71-73. |
| No related articles found! |
|
||
首页