The symbiosis of concurrency and verification: teaching and case studies
The symbiosis of concurrency and verification: teaching and case studies
复制标题
并发与验证的共生：教学与案例研究
DOI：
10.1007/s00165-017-0447-x
复制
发表时间：
2018
影响因子：
1
通讯作者：
Pedersen J
中科院分区：
文献类型：
--
作者：
Pedersen J
并发性开始被接受为本科生CS课程的核心知识领域--不再是孤立的，例如，作为操作系统模块中的一种支持机制，或者作为一门高级学科保留下来供以后学习。系统属性的形式化验证通常被认为是一个困难的主题领域，需要大量的数学知识，通常仅限于使用时序逻辑的较小系统。本文介绍了将并发性和验证性作为一门统一学科的教学材料、方法和经验，尽可能早地在课程中进行，使它们成为我们软件工程工具包的基本元素--理所当然地每天都要一起使用。并发性和验证性应该共生。对于并发系统来说，验证是必不可少的，因为面对复杂的非确定性(因此，很难重复)行为，测试变得特别不充分。并发性应该通过反映计算机系统运行的世界的并发性(因此，必须建模)来简化大多数规模和形式的计算机系统的表达；简化的表达导致简化的推理，从而导致验证。我们的方法可以让学生在不需要接受基本正规数学培训的情况下发展这些技能。相反，我们基于那些将必要的数学设计到我们使用的并发模型(CSP，-演算)、允许我们探索和验证这些系统的模型检查器(FDR)以及允许我们在这些模型中设计和构建高效可执行系统的编程语言/库(Occam-、Go、JCSP、ProcessJ)中的人的工作。本文介绍了一种用于并发系统开发和验证的工作流方法，并对作者所在的两所大学开发的两个开放式案例研究进行了介绍和反思。分析的问题包括安全性(不做坏事)、活跃性(做好事)和低概率死锁(测试未能发现)。给出了必要的技术背景，使本论文内容完备，其工作易于复制和推广。
Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum—no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as anadvanceddiscipline for later study. Formal verification of system properties is often considered adifficultsubject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. This paper presents materials, methods and experiences of teaching concurrency and verification as a unified subject, as early as possible in the curriculum, so that they becomefundamentalelements of our software engineering tool kit—to be used together every day as a matter of course. Concurrency and verification should live in symbiosis. Verification is essential for concurrent systems as testing becomes especially inadequate in the face of complex non-deterministic (and, therefore, hard to repeat) behaviours. Concurrency shouldsimplifythe expression of most scales and forms of computer system by reflecting the concurrency of the worlds in which they operate (and, therefore, have to model); simplified expression leads to simplified reasoning and, hence, verification. Our approach lets these skills be developed without requiring students to be trained in the underlying formal mathematics. Instead, we build on the work of those who have engineered that necessary mathematics into the concurrency models we use (CSP,-calculus), the model checker (FDR) that lets us explore and verify those systems, and the programming languages/libraries (occam-, Go, JCSP, ProcessJ) that let us design and build efficient executable systems within these models. This paper introduces a workflow methodology for the development and verification of concurrent systems; it also presents and reflects on two open-ended case studies, using this workflow, developed at the authors’ two universities. Concerns analysed include safety(don’t do bad things), liveness(do good things)and low probability deadlock(that testing fails to discover). The necessary technical background is given to make this paper self-contained and its work simple to reproduce and extend.
登录
查看更多内容
验证安全协议：CSP 的应用
DOI：
--
发表时间：
2004
期刊：
25 Years Communicating Sequential Processes
影响因子：
--
作者：
Steve A. Schneider;Rob Delicata
通讯作者：
Rob Delicata
正式模型
DOI：
--
发表时间：
1988
期刊：
影响因子：
--
作者：
T. Patten
通讯作者：
T. Patten
编译CSP
DOI：
--
发表时间：
2006
期刊：
Communicating Process Architectures Conference
影响因子：
--
作者：
F. Barnes
通讯作者：
F. Barnes
DOI：
10.1007/bfb0000463
发表时间：
1997
期刊：
2010 Third International Joint Conference on Computational Science and Optimization
影响因子：
--
作者：
B. Buth;M. Kouvaras;J. Peleska;Hui Shi
通讯作者：
Hui Shi
使用 CSP 和细化检查面向流程的操作系统行为
DOI：
10.1145/1713254.1713265
发表时间：
2010
期刊：
ACM SIGOPS Operating Systems Review
影响因子：
--
作者：
Barnes F
通讯作者：
Barnes F