A CSP Model for Mobile Channels
A CSP Model for Mobile Channels
复制标题
移动渠道的 CSP 模型
DOI：
10.3233/978-1-58603-907-3-17
复制
发表时间：
2008
影响因子：
11.2
通讯作者：
F. Barnes
中科院分区：
文献类型：
--
作者：
P. Welch;F. Barnes
CSP进程对其环境有一种静态的视角——一组固定的事件，它们通过这些事件相互同步。相比之下，π - 演算基于事件（通道）的动态构建以及它们在预先存在的通道上的分布。通过这种方式，可以动态地构建进程网络，使进程获得新的连接性。对于构建复杂系统，比如互联网交易和生物有机体建模，这种能力具有明显的吸引力。occam - π多处理语言建立在经典的occam之上，其设计和语义基于CSP。为了解决复杂系统的动态性问题，occam - π扩展允许通道（以及多路同步屏障）通过通道移动，并遵循先前occam规则的约束以实现安全高效的编程。本文通过完全在CSP内为移动通道构建一种形式化（操作）语义来协调这些扩展。这些语义提供了两个好处：使用移动通道对occam - π系统进行形式化分析，以及为occam - π编译器和运行时内核所使用的移动对象的实现机制提供形式化规范。
CSP processes have a static view of their environment - a fixed set of events through which they synchronise with each other. In contrast, the π-calculus is based on the dynamic construction of events (channels) and their distribution over pre-existing channels. In this way, process networks can be constructed dynamically with processes acquiring new connectivity. For the construction of complex systems, such as Internet trading and the modeling of living organisms, such capabilities have an obvious attraction. The occam-π multiprocessing language is built upon classical occam, whose design and semantics are founded on CSP. To address the dynamics of complex systems, occam-π extensions enable the movement of channels (and multiway synchronisation barriers) through channels, with constraints in line with previous occam discipline for safe and efficient programming. This paper reconciles these extensions by building a formal (operational) semantics for mobile channels entirely within CSP. These semantics provide two benefits: formal analysis of occam-π systems using mobile channels and formal specification of implementation mechanisms for mobiles used by the occam-π compiler and run-time kernel.