Session Types for Broadcasting
Session Types for Broadcasting
复制标题
广播的会话类型
DOI：
10.4204/eptcs.155.4
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
S. Gay
中科院分区：
文献类型：
--
作者：
Dimitrios Kouzapas;Ramunas Gutkovas;S. Gay
并发系统，即并行进程的系统，几乎无处不在，验证此类系统的正确性正在成为一个重要的课题。为此目的发明了许多形式主义，然而，引入了新类型的系统并且需要处理更大的系统。一个例子是在各个领域越来越多地部署无线传感器网络；特别是安全关键领域，例如丛林火灾探测。因此，确保它们的正确性很重要。过程演算是一种用于建模并发系统的形式语言。圆周率演算是这种具有消息传递并发性的语言的一个突出例子。 Psi-calculi 是一个参数化框架，它用任意数据和逻辑扩展了 pi 演算。 psi演算具有通用理论，其结果在自动定理证明器中检查，确保其正确性。在本论文中，我们通过引入排序系统和广义模式匹配来扩展psi演算的表达能力和建模精度。我们证明了扩展的 psi 演算具有相同的元理论结果。我们开发了 Pwb，它是 psi 演算框架的工具。该工具提供高级交互式符号执行和自动行为等效性检查。我们通过开发无线传感器网络数据收集协议的高级可执行模型来举例说明该工具的使用。我们是第一个为通信不可靠的系统引入基于会话类型的系统的公司。值得注意的是，我们不需要为类型添加特定的扩展来适应此类系统。我们证明类型系统的标准理想属性也适用于我们的类型系统。
Concurrent systems, i.e., systems of parallel processes, are nearly ubiquitous and verifying the correctness of such systems is becoming an important subject. Many formalisms were invented for such purpose, however, new types of systems are introduced and there is a need for handling larger systems. One examples is wireless sensor networks that are being deployed in increasing numbers in various areas; and in particular safety-critical areas, e.g., bush fire detection. Thus, ensuring their correctness is important.A process calculus is a formal language for modeling concurrent systems. The pi-calculus is a prominent example of such a language featuring message-passing concurrency. Psi-calculi is a parametric framework that extends the pi-calculus with arbitrary data and logics. Psi-calculi feature a universal theory with its results checked in an automated theorem prover ensuring their correctness.In this thesis, we extend psi-calculi expressiveness and modeling precision by introducing a sort system and generalised pattern matching. We show that the extended psi-calculi enjoy the same meta-theoretical results.We have developed the Pwb, a tool for the psi-calculi framework. The tool provides a high-level interactive symbolic execution and automated behavioral equivalence checking. We exemplify the use of the tool by developing a high-level executable model of a data collection protocol for wireless sensor networks.We are the first to introduce a session types based system for systems with unreliable communication. Remarkably, we do not need to add specific extensions to the types to accommodate such systems. We prove the standard desirable properties for type systems hold also for our type system.