COSTABS: a cost and termination analyzer for ABS
COSTABS: a cost and termination analyzer for ABS
复制标题
COSTABS：ABS 成本和终止分析器
DOI：
10.1145/2103746.2103774
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
G. Puebla
中科院分区：
文献类型：
--
作者：
E. Albert;P. Arenas;S. Genaim;M. Gómez;G. Puebla
ABS是一种抽象的行为规范语言，用于对分布式并发系统进行建模。ABS的特点是：(1)它允许从实现细节中抽象出来，同时保持可执行性：使用抽象数据类型上的功能子语言来指定内部的顺序计算；(2)命令式子语言通过异步方法调用、方法定义中的发布点和方法激活的协作调度提供灵活的并发和同步机制。本文提出了一个成本与终止分析器COSTABS，它能够证明程序的终止，并获得程序命令式片段和功能片段的资源使用界限。COSTABS可以推断的资源包括终止、执行步骤数、内存消耗、异步调用数等。分析边界提供了正式的保证，保证程序的执行永远不会超过推断的资源量。该系统可以作为免费软件从其网站下载，该网站还提供了示例库和web界面。据我们所知，COSTABS是第一个能够对并发语言执行资源分析的系统。
ABS is an abstract behavioural specification language to model distributed concurrent systems. Characteristic features of ABS are that: (1) it allows abstracting from implementation details while remaining executable: a functional sub-language over abstract data types is used to specify internal, sequential computations; and (2) the imperative sub-language provides flexible concurrency and synchronization mechanisms by means of asynchronous method calls, release points in method definitions, and cooperative scheduling of method activations. This paper presents COSTABS, a COSt and Termination analyzer for ABS, which is able to prove termination and obtain resource usage bounds for both the imperative and functional fragments of programs. The resources that COSTABS can infer include termination, number of execution steps, memory consumption, number of asynchronous calls, among others. The analysis bounds provide formal guarantees that the execution of the program will never exceed the inferred amount of resources. The system can be downloaded as free software from its web site, where a repository of examples and a web interface are also provided. To the best of our knowledge, COSTABS is the first system able to perform resource analysis for a concurrent language.