A Formal Framework for Compositional Verification of Organic Computing Systems
A Formal Framework for Compositional Verification of Organic Computing Systems
复制标题
有机计算系统组成验证的形式框架
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
W. Reif
中科院分区：
文献类型：
--
作者：
Florian Nafz;H. Seebach;J. Steghöfer;S. Bäumler;W. Reif
由于有机计算系统的自x特性，很难进行验证。然而，在安全关键领域，人们可能想要给出行为保证。一种降低整体验证任务复杂性的技术是应用合成定理。本文提出了一种有机计算系统的形式化描述和成分验证技术。自x行为和函数行为的分离对于形式化规范有许多好处。提出了一种基于区间时态逻辑的并发系统成分验证方法，并给出了如何将自x行为规范集成到并发系统成分验证方法中。在KIV交互式定理证明器的支持下，该方法得到了完全的工具支持。
Because of their self-x properties Organic Computing systems are hard to verify. Nevertheless in safety critical domains one may want to give behavioral guarantees. One technique to reduce complexity of the overall verification task is applying composition theorem. In this paper we present a technique for formal specification and compositional verification of Organic Computing systems. Separation of self-x and functional behavior has amongst others, advantages for the formal specification. We present how the specification of self-x behavior can be integrated into an approach for compositional verification of concurrent systems, based on Interval Temporal Logic. The presented approach has full tool support with the KIV interactive theorem prover.