Petrify: 基于Petri网的Java字节码并发性质分析

中文摘要 AI 辅助

自动化形式验证领域充斥着各种技术，它们在权衡中做出显著不同的选择：一些侧重于表达力和精度，支持复杂性质的验证；另一些则倾向于可扩展性和实用性，以便适用于使用不同特性的更大程序。本文提出Petrify，一种新颖的并发性质自动化验证技术，实现了独特的权衡。Petrify将Java字节码程序的语义编码为Petri网（PN），可通过最先进的模型检测工具（如LoLA）进行分析。正如我们的实验所展示的，Petrify的方法提供了表达力和实用性的有趣结合：PN是对程序并发行为的相当精确的编码；同时，Petrify的PN编码简洁，使得其分析对参数大小相当不敏感。针对字节码的另一个实际好处是，实现Petrify技术的原型工具jPetrify适用于任何版本Java编写的程序，甚至适用于Kotlin的一个子集（另一种编译为Java字节码的语言），而其他类似工具仅限于旧版本Java。虽然本文的实验侧重于分析死锁等基本性质，但Petrify的方法可扩展到其他类型的并发分析，我们计划在未来工作中解决这些问题。

英文摘要

The landscape of automated formal verification is populated by techniques that make prominently different trade-offs: some focus on expressiveness and precision, supporting the verification of complex properties; others favor scalability and practicality, so that they are applicable to larger programs using different features. This paper presents Petrify, a novel automated verification technique for concurrency properties that achieves a distinctive trade-off. Petrify encodes the semantics of Java bytecode programs into Petri nets (PNs), which can be analyzed by state-of-the-art model checking tools such as LoLA. As our experiments demonstrate, Petrify's approach offers an interesting combination of expressiveness and practicality: PNs are a fairly precise encoding of the concurrent behavior of programs; at the same time, Petrify's PN encoding is succinct, so that its analysis remains quite insensitive to parameter size. Another practical benefit of targeting bytecode is that jPetrify, the prototype tool that implements the Petrify technique, is applicable to programs written in any version of Java and even a subset of Kotlin (another language that compiles to Java bytecode) while other similar tools are limited to older versions of Java. While this paper's experiments focus on analyzing fundamental properties like deadlock, Petrify's approach lends itself to be extended to other kinds of concurrency analysis, which we plan to tackle in future work.

发表机构

• Software Institute, USI Università della Svizzera italiana（瑞士意大利语大学软件研究所）

机构由 AI 辅助整理，请以论文原文为准。