An approach for machine-assisted verification of Timed CSP specifications
An approach for machine-assisted verification of Timed CSP specifications
复制标题
一种机器辅助验证定时 CSP 规范的方法
DOI：
10.1007/s11334-010-0126-z
复制
发表时间：
2010
影响因子：
1.2
通讯作者：
S. Glesner
中科院分区：
文献类型：
--
作者：
T. Göthel;S. Glesner
实时进程演算Timed CSP能够表达诸如死锁自由度和实时约束等属性。因此，它非常适合建模和验证嵌入式软件。然而，关于定时CSP规范的证明不能确保是正确的，因为定时CSP的全面机器辅助还不可用。在本文中，我们提出了我们的形式化的时间CSP的Isabelle/HOL定理证明，我们制定了一个操作的共代数语义与互模拟等价和共代数不变量。这允许对定时CSP规范进行半自动和机械检查的证明。机械检查的证据增强了核查的信心，因为角落的情况不能被忽视。我们还将我们的形式化应用到具有实时约束的抽象规范。这是我们目前工作的基础，我们在其中验证部署在卫星上的简单实时操作系统。由于这个操作系统必须科普任意多个线程，我们使用验证技术，从该地区的参数化系统，我们概述了他们的形式化。
The real-time process calculus Timed CSP is capable of expressing properties such as deadlock-freedom and real-time constraints. It is therefore well-suited to model and verify embedded software. However, proofs about Timed CSP specifications are not ensured to be correct since comprehensive machine-assistance for Timed CSP is not yet available. In this paper, we present our formalization of Timed CSP in the Isabelle/HOL theorem prover, which we have formulated as an operational coalgebraic semantics together with bisimulation equivalences and coalgebraic invariants. This allows for semi-automated and mechanically checked proofs about Timed CSP specifications. Mechanically checked proofs enhance confidence in verification because corner cases cannot be overlooked. We additionally apply our formalization to an abstract specification with real-time constraints. This is the basis for our current work, in which we verify a simple real-time operating system deployed on a satellite. As this operating system has to cope with arbitrarily many threads, we use verification techniques from the area of parameterized systems for which we outline their formalization.
登录
查看更多内容
全局定时双向模拟：简介
DOI：
--
发表时间：
1999
期刊：
Formal Techniques for (Networked and) Distributed Systems
影响因子：
--
作者：
David de Frutos;Natalia López;M. Núñez
通讯作者：
M. Núñez
区域设置 - Isabelle 的切片概念
DOI：
--
发表时间：
1999
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
作者：
F. Kammüller;M. Wenzel;Lawrence Charles Paulson
通讯作者：
Lawrence Charles Paulson
伊莎贝拉/HOL 的 CSP 修正故障发散模型
DOI：
--
发表时间：
1997
期刊：
FME
影响因子：
--
作者：
H. Tej;B. Wolff
通讯作者：
B. Wolff
通过机械化语法分析在 Isabelle/HOL 中充分充分浅嵌入 π 演算
影响因子：
1.1
作者：
C. Röckl;D. Hirschkoff
通讯作者：
D. Hirschkoff