Mälardalen University, Västerås, Sweden.
School of Electronics and Computer Science, University of Southampton, Southampton, UK.
Sci Rep. 2022 Jan 25;12(1):1287. doi: 10.1038/s41598-022-05308-6.
Constructing a large biological model is a difficult, error-prone process. Small errors in writing a part of the model cascade to the system level and their sources are difficult to trace back. In this paper we extend a recent approach based on Event-B, a state-based formal method with refinement as its central ingredient, allowing us to validate for model consistency step-by-step in an automated way. We demonstrate this approach on a model of the heat shock response in eukaryotes and its scalability on a model of the [Formula: see text] signaling pathway. All consistency properties of the model were proved automatically with computer support.
构建大型生物模型是一个困难且容易出错的过程。模型的某个部分编写过程中的小错误会级联到系统级别，并且难以追溯其来源。在本文中，我们扩展了一种基于事件 B 的最新方法，事件 B 是一种基于状态的形式化方法，其核心是细化，允许我们以自动化的方式逐步验证模型的一致性。我们在真核生物热激反应模型及其 [Formula: see text] 信号通路模型上演示了这种方法。模型的所有一致性属性都在计算机的支持下自动证明。
