arXiv 0905.39512009-05cs.DCcs.LO

容错系统时序满意度的建模与验证

Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness

Chih-Hong Cheng, Christian Buckl, Javier Esparza, Alois Knoll

备注：: 1. Appear in the 13-th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications (DS-RT'09). 2. Compared to the DS-RT version, we add motivations for editing automata, and footnote that the sketch of editing algo is only applicable in our job-processing element to avoid ambiguity (because actions are chained)
DOI：: 10.1109/DS-RT.2009.20

摘要：

越来越多的基于模型的工具的使用使得形式化验证技术能够在分布式实时系统的上下文中进一步使用。为了避免状态爆炸，有必要构建关注所考虑方面的验证模型。在本文中，我们讨论了如何构建一个验证模型，在分布式实时系统的时序分析。我们（1）给出了关于时间自动机对这些系统建模的限制的观察，（2）制定了关于如何执行模型到模型转换以从系统模型导出验证模型的数学表示，以及（3）提出了一些如何减少模型大小的理论标准。后者尤其重要，因为对于复杂系统的验证，反映所考虑的系统的属性的有效模型对于验证算法本身同样重要。最后，我们提出了一个扩展的基于模型的开发工具FTOS，旨在开发容错系统，证明%的好处，我们的方法。

英文摘要：

The increasing use of model-based tools enables further use of formal verification techniques in the context of distributed real-time systems. To avoid state explosion, it is necessary to construct verification models that focus on the aspects under consideration. In this paper, we discuss how we construct a verification model for timing analysis in distributed real-time systems. We (1) give observations concerning restrictions of timed automata to model these systems, (2) formulate mathematical representations on how to perform model-to-model transformation to derive verification models from system models, and (3) propose some theoretical criteria how to reduce the model size. The latter is in particular important, as for the verification of complex systems, an efficient model reflecting the properties of the system under consideration is equally important to the verification algorithm itself. Finally, we present an extension of the model-based development tool FTOS, designed to develop fault-tolerant systems, to demonstrate %the benefits of our approach.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。