paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Model-based testing of networked applications

基于模型的网络应用测试
ISSTA Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis2021匹配度 3/10 · 该论文属于形式化方法与软件测试交叉，使用 Coq 嵌入式 DSL 建模并测试网络协议，与用户关注的 LLM/Agent 和程序分析、浮点分析、贝叶斯程序分析等核心方向均无直接关联。虽然涉及形式验证和 DSL，但并非用户主要追踪的 AI×PL 或静态分析议题。引用 9 inbox
Yishuai Li, Benjamin C. Pierce, Steve Zdancewic
测试、调试与修复领域特定语言与建模
crossref: 2026-09-12

AI 速览

一句话：提出一个基于Coq嵌入式DSL的非确定性服务器模型，实现应用层协议自动测试并平滑过渡到形式验证。

本文针对应用层协议测试缺乏原则性自动化框架的问题，提出了一种基于模型的自动测试方法。其核心创新是设计了一种领域特定嵌入式语言，用于编写网络服务器行为的非确定性模型。这些模型直接定义在Coq交互式定理证明器内部，使得测试与形式验证之间能够平滑过渡：同一套模型既可用于自动生成测试用例，又可为后续机器化验证提供基础。该方法旨在提升网络应用协议测试的系统性与可靠性，并借助Coq的表达能力处理服务器行为中的不确定性。摘要未给出具体评估数据，但强调了该框架在测试与验证统一方面的潜力。

问题
应用层网络协议的测试缺乏原则性的自动化测试框架，难以系统化地覆盖服务器行为中的不确定性。
方法
设计一种嵌入Coq的领域特定语言，用于编写网络服务器行为的非确定性模型，并基于该模型自动测试应用层协议。
评估
摘要未详述具体评估，但指出模型定义在Coq中，支持从测试到形式验证的平滑过渡。
原文摘要（Abstract）

We present a principled automatic testing framework for application-layer protocols. The key innovation is a domain-specific embedded language for writing nondeterministic models of the behavior of networked servers. These models are defined within the Coq interactive theorem prover, supporting a smooth transition from testing to formal verification.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot6687,
  title = {Model-based testing of networked applications},
  author = {Yishuai Li and Benjamin C. Pierce and Steve Zdancewic},
  booktitle = {ISSTA},
  year = {2021},
  doi = {10.1145/3460319.3464798}
}