Quantitative Evaluation of Systems - 16th International Conference, QEST 2019, Glasgow, UK, September 10-12, 2019, Proceedings
Quantitative Evaluation of Systems - 16th International Conference, QEST 2019, Glasgow, UK, September 10-12, 2019, Proceedings
复制标题
系统定量评估 - 第 16 届国际会议，QEST 2019，英国格拉斯哥，2019 年 9 月 10-12 日，会议记录
DOI：
10.1007/978-3-030-30281-8_14
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Mu C
中科院分区：
文献类型：
--
作者：
Mu C
Security-sensitive computerised communication systems are of increasing importance, however checking that they function correctly can be non-trivial. We propose automated verification techniques for the formal analysis of quantitative properties of such systems. Since communication networks typically require the collaboration of their participants to work effectively, we adopt a game-theoretic approach. Utility functions for each player, such as the degree of security offered and the communication costs incurred, are formally specified using quantitative temporal logics. Then, building upon probabilistic verification techniques for parametric Markov chains, we develop methods to identify Nash equilibria representing stable strategies for the participants. We implement our methods as an extension of the PRISM model checker, and illustrate their applicability by studying anonymity-cost trade-offs in the Crowds anonymity protocol.
