Generating and Checking Probabilistic Models

生成和检查概率模型

• 批准号: RGPIN-2019-06372
• 负责人: vanBreugel, Franck
• 金额: $ 1.68万
• 依托单位: York University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=716052
• 关键词: Generating; Checking; Probabilistic; Models

Nowadays, many software systems rely on randomness. For example, it is well known that randomness provides computer games with the ability to surprise players, which is a key factor in their long-term appeal. Randomness is also prominent in machine learning, as exemplified by the use of randomized algorithms such as stochastic gradient descent. Randomness is also ubiquitous in cryptography. These are just three examples that show how pervasive randomness is in today's software. As Dijkstra wrote half a century ago, “Program testing can be used to show the presence of bugs, but never to show their absence!” Testing is the most commonly used technique to detect bugs in software systems. Software with randomness usually gives rise to multiple, potentially different, executions. Hence, running a test on software with randomness multiple times does not provide any guarantee that different executions are checked. Furthermore, if a bug has been found, reproducing it is difficult. Therefore, in the presence of randomness, techniques complementary to testing are essential for detecting bugs. Model checking, a technique introduced by Clarke, Emerson, and Sifakis, complements testing in the quest to find bugs. Roughly, this technique consists of three major steps. Firstly, the software system is modeled. The resulting model is usually a state machine, where each state is an abstraction of a snapshot of the system and transitions between states describe all possible ways the system can evolve. Secondly, the properties of interest of the software system are expressed as formulas of a logic. Thirdly, the model checker is run. A model checker is a tool that takes as input a model and a property and attempts to check whether the property is satisfied in the model. Generally, there are three outcomes. Either the model checker confirms that the property holds in the model, or it provides a counterexample demonstrating that the property does not hold (which may indicate a bug in the modeled software system), or it runs out of memory or time. In this proposal, I focus on models of software systems with randomness, which are often called probabilistic models. Checking properties of such models is known as probabilistic model checking. To evaluate new techniques and tools for probabilistic model checking, researchers either have considered less than a handful of realistic probabilistic models or have used randomly generated probabilistic models. Both approaches have serious shortcomings. The former approach gives us little confidence in the results. The latter approach only gives us useful results if the generated models have the same characteristics as models encountered in practice. The two goals of my research program are - developing techniques and tools that support probabilistic model checking, and - generating realistic instances of probabilistic models to evaluate those techniques and tools.

如今，许多软件系统都依赖于随机性，例如，众所周知，随机性为计算机游戏提供了给玩家带来惊喜的能力，这是其长期吸引力的关键因素，随机性在机器学习中也很突出。通过使用随机算法（例如随机梯度下降），随机性在密码学中也很普遍。这只是三个例子，说明了随机性在当今的软件中是多么普遍。 正如 Dijkstra 在半个世纪前所写的那样，“程序测试可以用来显示错误的存在，但永远不能显示它们的不存在！”测试是最常用的检测软件系统中的错误的方法，具有随机性的软件通常会产生多个错误。 ，可能不同的执行。因此，多次对具有随机性的软件运行测试并不能保证检查不同的执行。此外，如果发现错误，则很难重现它。技术互补测试对于检测错误至关重要。 模型检查是 Clarke、Emerson 和 Sifakis 提出的一种技术，它是对寻找错误的测试的补充。粗略地说，该技术包括三个主要步骤：首先，对软件系统进行建模。生成的模型通常是一个状态机。其中每个状态都是系统快照的抽象，状态之间的转换描述了系统演化的所有可能方式。其次，软件系统的感兴趣的属性被表达为逻辑公式。第三，运行模型检查器。 。一个模型检查器是一种将模型和属性作为输入并尝试检查模型中是否满足该属性的工具。通常，模型检查器会确认模型中是否存在该属性，或者提供三种结果。反例证明该属性不成立（这可能表明建模软件系统中存在错误），或者内存或时间不足。 在本提案中，我重点关注具有随机性的软件系统模型，这些模型通常称为概率模型。为了评估概率模型检查的新技术和工具，研究人员考虑了以下方法。一些现实的概率模型或使用随机生成的概率模型，前一种方法使我们对结果缺乏信心，而后一种方法仅在生成的模型具有相同特征的情况下才为我们提供有用的结果。实践中遇到的模型。 我的研究计划的两个目标是 - 开发支持概率模型检查的技术和工具，以及 - 生成概率模型的真实实例来评估这些技术和工具。