Verification of control systems using Circus
Verification of control systems using Circus
复制标题
使用 Circus 验证控制系统
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
P. Clayton
中科院分区：
文献类型：
--
作者：
Ana Cavalcanti;P. Clayton
控制系统的设计通常是基于控制律的图解定义。独立使用Z和CSP来验证它们的实现已经取得了成功，即使是对于非常大的应用程序;基于称为ProofPower的定理证明器的工具已经实现了高水平的自动化。我们已经扩展了这种方法，使用称为Circus的符号来集成Z和CSP的使用;因此，我们可以处理更大的图集并证明实现的更多属性。在本文中，我们将展示如何重用现有的工具和经验，以在新技术的背景下提供自动化。这使我们对它在工业上的适用性充满信心
The design of control systems is usually based on diagrammatic definitions of control laws. The independent use of Z and CSP to verify their implementations has been successful, even for very large applications; high levels of automation have been achieved with tools based on a theorem prover called ProofPower. We have extended this approach to integrate the use of Z and CSP using a notation called Circus; as a result, we can handle a larger set of diagrams and prove more properties of the implementation. In this paper, we show how we can reuse the existing tools and experience to provide automation in the context of the new technique. This gives us confidence in its applicability in industry