论会话类型的可监控性：理论与实务（扩展版）
编程语言
2021-05-25 v2
摘要
在并发与分布式系统中，软件组件被期望按照预定协议和 API 进行通信——若某组件不遵守，系统的可靠性便会受损。此外，隔离和修复协议/API 错误可能非常困难。人们已提出多种方法来检查通信系统的正确性，从编译时验证到运行时验证不一而足；其中，会话类型已被应用于静态类型检查和运行时监控。本工作从理论与实务两方面重新审视使用会话类型对通信系统进行运行时验证。在理论方面，我们开发了会话监控进程的新形式化模型；借助该模型，我们提出并证明了关于会话类型可监控性的新结果，将其运行时与静态验证在可靠性（即监控器是否仅标记不良类型进程）和完备性（即是否所有不良类型进程都能被监控器标记）方面联系起来。在实务方面，我们表明我们的监控理论确实可实现：基于我们的形式化模型，我们开发了一个用于自动生成会话监控器的 Scala 工具包。我们的可执行监控器可用于检测用任何编程语言编写的黑盒进程；我们通过一系列基准测试评估了我们方法的可行性。
引用
@article{arxiv.2105.06291,
title = {On the Monitorability of Session Types, in Theory and Practice (Extended Version)},
author = {Christian Batrolo Burlò and Adrian Francalanza and Alceste Scalas},
journal= {arXiv preprint arXiv:2105.06291},
year = {2021}
}