A Lightweight Framework for Regular Expression Verification
A Lightweight Framework for Regular Expression Verification
复制标题
DOI：
10.1109/hase.2019.00011
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Xiao Liu;Yufei Jiang;Dinghao Wu
中科院分区：
文献类型：
--
作者：
Xiao Liu;Yufei Jiang;Dinghao Wu
正则表达式和有限状态自动机在模式搜索和字符串匹配程序中被广泛使用。不幸的是，尽管正则表达式很受欢迎，但即使是有经验的程序员也很难理解和验证。传统的测试技术仍然是一个挑战，因为大型正则表达式经常用于安全目的，如输入验证和网络入侵检测。本文提出了一个轻量级的正则表达式验证框架。在这个框架中，不需要大量的测试用例，而是接受自然语言描述中的需求来自动合成形式规范。通过检查合成的规范和目标正则表达式之间的等价性，将检测错误并报告反例。我们已经构建了一个Web应用原型，并通过两个案例说明了它的可用性。
Regular expressions and finite state automata have been widely used in programs for pattern searching and string matching. Unfortunately, despite the popularity, regular expressions are difficult to understand and verify even for experienced programmers. Conventional testing techniques remain a challenge as large regular expressions are constantly used for security purposes such as input validation and network intrusion detection. In this paper, we present a lightweight verification framework for regular expressions. In this framework, instead of a large number of test cases, it takes in requirements in natural language descriptions to automatically synthesize formal specifications. By checking the equivalence between the synthesized specifications and target regular expressions, errors will be detected and counterexamples will be reported. We have built a web application prototype and demonstrated its usability with two case studies.