论文标题
真实随机定时系统的适度模型和工具的概述
An Overview of Modest Models and Tools for Real Stochastic Timed Systems
论文作者
论文摘要
我们依赖于从智能电网到航空电子组件的网络物理系统的安全，可靠和及时的操作。其中许多涉及时间依赖性行为，并且会受到随机性的影响。因此，建模语言和验证工具需要支持这些定量方面。在我在2022年3月的邀请演讲中，我使用适度的建模语言和适度的工具集对定量验证进行了介绍，并强调了最近的三个最近的案例研究，对模型表现力和工具能力的需求越来越高：在芯片上建模为Markov Chain的网络上的电源噪声案例；卫星星座中使用马尔可夫决策过程中的消息路由的情况；以及通过Markov Automata模型检查优化对比特币的攻击的情况。本文总结了演示文稿。
We depend on the safe, reliable, and timely operation of cyber-physical systems ranging from smart grids to avionics components. Many of them involve time-dependent behaviours and are subject to randomness. Modelling languages and verification tools thus need to support these quantitative aspects. In my invited presentation at MARS 2022, I gave an introduction to quantitative verification using the Modest modelling language and the Modest Toolset, and highlighted three recent case studies with increasing demands on model expressiveness and tool capabilities: A case of power supply noise in a network-on-chip modelled as a Markov chain; a case of message routing in satellite constellations that uses Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. This paper summarises the presentation.
