COSTABS: a cost and termination analyzer for ABS

E Albert, P Arenas, S Genaim… - Proceedings of the …, 2012 - dl.acm.org
Proceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and …, 2012dl.acm.org
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 …
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.
ACM Digital Library