A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification
A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification
复制标题
CSP定时输入输出关系和机械化一致性验证策略
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
A. Mota
中科院分区：
文献类型：
--
作者：
Gustavo Carvalho;A. Sampaio;A. Mota
在这里，我们提出了一种基于过程代数 CSP 的定时输入输出一致性关系（名为 CSPTIO）。与其他关系相比，CSPTIO 分析数据流反应式系统，并通过重用成功的技术和工具，在高级策略方面实现一致性验证的机械化：细化检查（特别是使用 FDR 工具）和 SMT 求解（使用 Z3）。因此，一致性验证不需要实现特定的算法或操作复杂的数据结构。此外，机械化也被证明是良好的。为了分析 CSPTIO 的实用性，我们首先考虑一个玩具示例。然后我们分析两个不同领域的关键系统：航空和汽车。 CSPTIO 在分析的实施模型中检测到所有不良行为。
Here we propose a timed input-output conformance relation (named CSPTIO) based on the process algebra CSP. In contrast to other relations, CSPTIO analyses data-flow reactive systems and conformance verification is mechanised in terms of a high-level strategy by reusing successful techniques and tools: refinement checking (particularly, using the FDR tool) and SMT solving (using Z3). Therefore, conformance verification does not require the implementation of specific algorithms or the manipulation of complex data structures. Furthermore, the mechanisation is proved sound. To analyse the usefulness of CSPTIO, we first consider a toy example. Then we analyse critical systems from two different domains: aeronautics and automotive. CSPTIO detected all undesired behaviours in the analysed implementation models.