论文标题
实施编舞提取
Implementing Choreography Extraction
论文作者
论文摘要
编排是对并发组件之间相互作用的全局描述，最著名的是用于验证和合成正确构造软件的设置。他们需要一种自上而下的方法：程序员首先编写编排，然后使用它们来验证或综合其程序。但是，大多数软件尚未伴随着编排，从而阻止其应用。为了攻击这个问题，先前的工作调查了编舞提取，该编排会自动构建一个编排，该编排描述了给定的一组程序或协议规范的行为。 我们提出了一种新的提取方法，可以改善最新技术：我们可以处理配备状态和内部计算的程序，并且时间复杂性会更好。我们还实施了这一理论，并表明，尽管其理论上的指数复杂性，但它在实践中还是可用的。我们讨论有效实施所需的数据结构，引入一些优化并执行系统的实际评估。
Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behaviour of a given set of programs or protocol specifications. We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation and time complexity is dramatically better. We also implement this theory and show that, in spite of its theoretical exponential complexity, it is usable in practice. We discuss the data structures needed for an efficient implementation, introduce some optimisations, and perform a systematic practical evaluation.
