论文标题
关于定时电路的规格和证明
On Specifications and Proofs of Timed Circuits
论文作者
论文摘要
给定一个离散状态连续的反应系统，例如数字电路，经典方法是将其首先建模为状态过渡系统，然后证明其属性。我们的贡献提倡一种不同的方法：直接对此类系统的投入输出行为进行操作，而不必首先识别状态及其过渡。我们讨论了某些示例中这种方法的好处，这些示例表明它与自动化和容忍性的概念很好地整合在一起。我们还详细阐述了框架中模块组成的一些意外文物，并以一些开放的研究问题得出结论。
Given a discrete-state continuous-time reactive system, like a digital circuit, the classical approach is to first model it as a state transition system and then prove its properties. Our contribution advocates a different approach: to directly operate on the input-output behavior of such systems, without identifying states and their transitions in the first place. We discuss the benefits of this approach at hand of some examples, which demonstrate that it nicely integrates with concepts of self-stabilization and fault-tolerance. We also elaborate on some unexpected artefacts of module composition in our framework, and conclude with some open research questions.
