[1]王晓燕,韩啸,彭君,等.实时并发系统的PTSL模型检测[J].智能系统学报,2017,12(5):694-701.[doi:10.11992/tis.201706008]
WANG Xiaoyan,HAN Xiao,PENG Jun,et al.PTSL model checking of timed concurrent system[J].CAAI Transactions on Intelligent Systems,2017,12(5):694-701.[doi:10.11992/tis.201706008]
点击复制
WANG Xiaoyan,HAN Xiao,PENG Jun,et al.PTSL model checking of timed concurrent system[J].CAAI Transactions on Intelligent Systems,2017,12(5):694-701.[doi:10.11992/tis.201706008]
实时并发系统的PTSL模型检测
《智能系统学报》[ISSN 1673-4785/CN 23-1538/TP] 卷:
12
期数:
2017年第5期
页码:
694-701
栏目:
学术论文—智能系统
出版日期:
2017-10-25
- Title:
- PTSL model checking of timed concurrent system
- Keywords:
- model checking; probabilistic timed concurrent game structure; probabilistic timed strategy logic; probabilistic timed automata; region graph; timed concurrent system; game model
- 分类号:
- TP311
- 摘要:
- 随着实时并发系统的软件规模越来越大、复杂性日趋增加，如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质，它不仅包括对系统模型的遍历以及基于图形的分析方法，而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型（CGS）的扩展，在此基础上添加了概率与时间性质，提出了概率时间并发博弈结构（PTCGS）。同时本文还提出了新的逻辑语言-概率时间策略逻辑（PTSL），它显式地把策略作为一阶逻辑中的对象，从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求，从而提高系统的可靠性。最后，本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。
- Abstract:
- With the increased scale and complexity of real-time concurrent software systems, ensuringtheir correctness and reliability has become a matter of urgency. Current model-checking technology uses an automated demonstration algorithm to judgesystem properties, which must include the traversal in the system model and graph-based analysis techniques as well asextensive numerical computations. In this paper, we consider the timed concurrency model as an extension of the concurrent game model (CGS) and addprobability and time properties to propose a new probabilistic timed concurrent game structure (PTCGS). We also propose a new logic language called probabilistic timed strategy logic (PTSL), which uses strategy as the object in the first-order logic to specify the nonzero-sum attributes in a simple and natural way. Lastly, we give an example usingthe ZeroConf protocol to demonstrate the correctness of the PTSL model checking method.
- 参考文献/References:
-
[1] CLARKE E, GRUMBERG O, PELED D. Model Checking[M]. Cambridge:MIT press, 1999:5-60.
[2] BEAUQUIER D. On probabilistic timed automata[J]. Theoretical computer science, 2003, 292(1):65-84.
[3] KWIATKOWSKA M, NORMAN G, SEGALA R, et al. Automatic verification of real-time systems with discrete probability distributions[J]. Theoretical computer science,2002, 282:101-150.
[4] CLARKE E, EMERSON A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]//Proceedinns of the Workshop Logic of Programs.Newyork, US, 1981:52-71.
[5] HANSSON H, JONSSON B. A logic for reasoning about time and reliability[J]. Formal aspects of computing, 1994, 6(5):512-535.
[6] ALFARO de L. Temporal Logics for the Specification of Performance and Reliability[C]//Proc STACS’97.New York, US, 1997:165-176.
[7] ALUR R, HENZINGER T A, KUPFERMAN O. Alternating-time temporal logic[J]. Journal of the ACM, 2002, 49:672-713.
[8] CHATTERJEE K, HENZINGER T A. Strategy improvement for stochastic Rabin and Strett Games[C]//Proc DBLP 2006. Bonn, Germany, 2006:375-389.
[9] CHATTERJEE K, HENZINGER T A, PITERMAN N. Strategy logic[J]. Information and computation, 2007, 208(6):677-693.
[10] Basset N, Kwiatkowska M, Topcu U, et al. Strategy synthesis for stochastic games with multiple long-run objectives[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Germany, 2015:256-271.
[11] KRISHNENDU Chatterjee, LUCA de Alfaro, THOMAS A,et al. Strategy improvement for concurrent reachability and turn-based stochastic safety games[J]. Journal of computer and system sciences, 2013, 79:640-657.
[12] ALFARO L de, FAELLA M, HENZINGER T, et al. The element of surprise in timed games[C]//14th International Conference on Concurrency Theory. Marceille, France,2003:144-158.
[13] THOMAS Brihaye, FRAN Cois, LAROUSSINIE, et al. Timed Concurrent Game Structures[C]//Proceedings of the 18th international conference on Concurrency Theory. Lisbon, Portugal, 2007:445-459.
[14] RAJEEV A, THOMAS A, HENZINGER, et al. Alternating-time temporal logic[J]. Journal of the ACM, 2002,49(5):672-713.
[15] CHEN Taolue, LU Jian. Probabilistic alternating-time temporal logic and model checking algorithm[C]//Fourth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD), 2007. Haikou, China, 2007:35-39.
[16] CHRISTEL Baier, TOMÁ? Brázdil, MARCUS Größer, et al. Stochastic game logic[C]//Conference:Quantitative Evaluation of Systems. Edinburgh, UK,2007:227-236.
[17] MARTA Kwiatkowska A, GETHIN Norman A, JEREMY Sproston B, et al. Symbolic model checking for probabilistic timed automata[J]. Information and computation, 2007, 205(2):1027-1077.
[18] MARTA Kwiatkowska, GETHIN Norman, DAVID Parker, et al. Performance analysis of probabilistic timed automata using digital clocks[J]. Formal methods in system design, 2006, 29(1):33-78.
- 相似文献/References:
-
[1]朱创营,常亮,徐周波,等.含有合取查询的时态描述逻辑ALC-LTL模型检测[J].智能系统学报,2014,9(6):714.[doi:10.3969/j.issn.1673-4785.201303034]
ZHU Chuangying,CHANG Liang,XU Zhoubo,et al.Research on the model checking of temporal description logic ALC-LTL containing conjunctive query[J].CAAI Transactions on Intelligent Systems,2014,9():714.[doi:10.3969/j.issn.1673-4785.201303034]
备注/Memo
收稿日期:2017-06-05。
基金项目:国家自然科学基金项目（61502196）.
作者简介:王晓燕,女,1977年生,讲师,博士,主要研究方向为软件建模与验证技术、软件开发新方法。申请发明专利2项,并获得2010年中国国家专利优秀奖,2008年吉林省科技进步一等奖,中国商业科技进步二等奖。发表论文20余篇,其中被SCI收录5篇;韩啸,男,1981年生,编辑,博士研究生,主要研究方向为网络协同、软件建模和网络技术;彭君,男,1981年生,讲师,博士,主要研究方向为模型驱动技术、构件技术、软件体系结构。
通讯作者:王晓燕.E-mail:wangxy@jlu.edu.cn
更新日期/Last Update:
2017-10-25