使用 Spin / Promela 来模拟心跳协议？
Using Spin / Promela to model heartbeat protocol?
我是 Spin 的新手，想知道 Spin 是否可以或已经用于在面对间歇性或故障网络时对心跳协议进行建模。
我纠结这个问题的一个原因是 Spin 抽象了时间维度（只有 "before" 和 "after" 的概念），但心跳本质上是一个与时间相关的概念。在我们当前的分布式系统心跳设计中（我想使用 Spin 来改进），当网络变得不稳定时，可能会发生一些不好的事情。最终，事情会自行解决（系统重新启动），但 "eventually consistent" 在这种情况下还不够好——而且 Spin 模型似乎认为最终一致不是错误。在我们的案例中，客户有一定的实时响应需求。
很抱歉这是一个模糊的问题；总结一下，有没有心跳相关的自旋模型的例子？或者关于如何为此类系统建模的任何建议？
TL;DR: 您可能想查看 Sphin 或其他一些 model-checker for 混合实时系统.
有可能以某种方式使用 Promela 设计一个具有 discretized clock signal 的系统，然后表达一些 LTL 属性 在一些内部变量上跟踪时间流。然而，我这样做只是为了小玩具的例子，我不建议在更大的项目中使用它。
来自 Promela 的 documentation （重点是我的）:
In the basic Promela language there is no mechanism for expressing
properties of clocks or of time related properties or events. There
are good algorithms for integrating real-time constraints into the
model checking process, but most attention has so far been given to
real-time verification problems in hardware circuit design, rather
than the real-time verification of asynchronous software, which is the
domain of the Spin model checker.
The best known of these algorithms incur significant performance
penalties compared with untimed verification. Each clock variable
added to a model can increase the time and memory requirements of
verification by an order of magnitude. Considering that one needs at
least two or three such clock variables to define meaningful
constraints, this seems to imply, for the time being, that a real-time
capability requires at least three to four orders of magnitude more
time and memory than the verification of the same system without time
constraints.
The good news is that if a correctness property can be proven for an
untimed Promela model, it is guaranteed to preserve its correctness
under all possible real-time constraints. The result is therefore
robust, it can be obtained efficiently, and it encourages good design
practice. In concurrent software design it is usually unwise to link
logical correctness with real-time performance.
Promela is a language for specifying systems of asynchronous
processes. For the definition of such a system we abstract from the
behavior of the process scheduler and from any assumption about the
relative speed of execution of the various processes. These
assumptions are safe, and the minimal assumptions required to allow us
to construct proofs of correctness. The assumptions differ
fundamentally from those that can be made for hardware systems, which
are often driven by a single known clock, with relative speeds of
execution precisely known. What often is just and safe in hardware
verification is, therefore, not necessarily just and safe in software
verification.
Spin guarantees that all verification results remain valid independent
of where and how processes are executed, timeshared on a single CPU,
in true concurrency on a multiprocessor, or with different processes
running on CPUs of different makes and varying speeds. Two points are
worth considering in this context: first, such a guarantee can no
longer be given if real-time constraints are introduced, and secondly,
most of the existing real-time verification methods assume a true
concurrency model, which inadvertently excludes the more common method
of concurrent process execution by timesharing.
It can be hard to define realistic time bounds for an abstract
software system. Typically, little can be firmly known about the
real-time performance of an implementation. It is generally unwise to
rely on speculative information, when attempting to establish a
system's critical correctness properties.
我是 Spin 的新手，想知道 Spin 是否可以或已经用于在面对间歇性或故障网络时对心跳协议进行建模。
我纠结这个问题的一个原因是 Spin 抽象了时间维度（只有 "before" 和 "after" 的概念），但心跳本质上是一个与时间相关的概念。在我们当前的分布式系统心跳设计中（我想使用 Spin 来改进），当网络变得不稳定时，可能会发生一些不好的事情。最终，事情会自行解决（系统重新启动），但 "eventually consistent" 在这种情况下还不够好——而且 Spin 模型似乎认为最终一致不是错误。在我们的案例中，客户有一定的实时响应需求。
很抱歉这是一个模糊的问题；总结一下，有没有心跳相关的自旋模型的例子？或者关于如何为此类系统建模的任何建议？
TL;DR: 您可能想查看 Sphin 或其他一些 model-checker for 混合实时系统.
有可能以某种方式使用 Promela 设计一个具有 discretized clock signal 的系统，然后表达一些 LTL 属性 在一些内部变量上跟踪时间流。然而，我这样做只是为了小玩具的例子，我不建议在更大的项目中使用它。
来自 Promela 的 documentation （重点是我的）:
In the basic Promela language there is no mechanism for expressing properties of clocks or of time related properties or events. There are good algorithms for integrating real-time constraints into the model checking process, but most attention has so far been given to real-time verification problems in hardware circuit design, rather than the real-time verification of asynchronous software, which is the domain of the Spin model checker.
The best known of these algorithms incur significant performance penalties compared with untimed verification. Each clock variable added to a model can increase the time and memory requirements of verification by an order of magnitude. Considering that one needs at least two or three such clock variables to define meaningful constraints, this seems to imply, for the time being, that a real-time capability requires at least three to four orders of magnitude more time and memory than the verification of the same system without time constraints.
The good news is that if a correctness property can be proven for an untimed Promela model, it is guaranteed to preserve its correctness under all possible real-time constraints. The result is therefore robust, it can be obtained efficiently, and it encourages good design practice. In concurrent software design it is usually unwise to link logical correctness with real-time performance.
Promela is a language for specifying systems of asynchronous processes. For the definition of such a system we abstract from the behavior of the process scheduler and from any assumption about the relative speed of execution of the various processes. These assumptions are safe, and the minimal assumptions required to allow us to construct proofs of correctness. The assumptions differ fundamentally from those that can be made for hardware systems, which are often driven by a single known clock, with relative speeds of execution precisely known. What often is just and safe in hardware verification is, therefore, not necessarily just and safe in software verification.
Spin guarantees that all verification results remain valid independent of where and how processes are executed, timeshared on a single CPU, in true concurrency on a multiprocessor, or with different processes running on CPUs of different makes and varying speeds. Two points are worth considering in this context: first, such a guarantee can no longer be given if real-time constraints are introduced, and secondly, most of the existing real-time verification methods assume a true concurrency model, which inadvertently excludes the more common method of concurrent process execution by timesharing.
It can be hard to define realistic time bounds for an abstract software system. Typically, little can be firmly known about the real-time performance of an implementation. It is generally unwise to rely on speculative information, when attempting to establish a system's critical correctness properties.