Computer Science ›› 2017, Vol. 44 ›› Issue (Z6): 571-574.doi: 10.11896/j.issn.1002-137X.2017.6A.128

Previous Articles     Next Articles

Validation for Probability Real-time System with Data Constraints

ZHANG Chun-yan and SUN Jun   

  • Online:2017-12-01 Published:2018-12-01

Abstract: A probabilistic real-time system with data constraints is a computing system with both probabilistic time constraints and data constraints.At present,there exist a few studies of the specification and verification that uniform discrete data constraints and sequence time constraint work in the probability model.In this paper,we proposed a specification based on sequence time probability ZIA,which has both sequence data anstraints and discrete data constraints,and gave its temporal logic.For CTL and PCTL,although the logic is very powerful,it can only reflect the temporal properties.This paper proposed a new formal language CTML to express the metric properties of query which retaines the ability to express temporal properties and gave the validation algorithm of probability of ZIA specification.

Key words: Data constraints,Probability of real-time system,Continuous time,ZIA

[1] 李广元,唐稚松.带有时钟变量的线性时序逻辑与概率实时系统验证[J].软件学报,2002,13(1):33-41.
[2] 戎玫,张广泉.模型检测新技术研究[J].计算机科学,2003,30(5):102-104.
[3] BRARD 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!
Full text



No Suggested Reading articles found!