In a nutshell

The task is to develop a method to synthesize capacity bounds for deployment components in Real-Time ABS [1].

Background & motivation

Real-Time ABS is an executable modeling language, which is suitable for modeling resource-aware distributed systems at a high level of abstraction. The language is object-oriented and features concurrent object groups that communicate via asynchronous method calls and futures. A particular characteristic of Real-Time ABS is the support for deployment components which act like resource centers and provision resources to processes with declared cost expressions and deadlines. This enables resource-aware programming. Models in Real-Time ABS are nondeterministic, in particular the provisioning of resources in deployment components depends on the scheduling decisions of the runtime system. The challenge is to synthesize bounds at compile time on the resources given to the deployment components, which allows the deadlines of the processes to be met. This enables Real-Time ABS programs in which the resource capacities are given as logical variables rather than concrete values by the programmer. We aim to leverage a state-of-the art satisfiability modulo theories solver, like Z3 [2], which is well suited for static analysis tools. It enables efficient reasoning for first-order logical formulas in theories for e.g. real numbers, integers, uninterpreted functions and common data structures like lists and arrays.

Problem description

The thesis will consist of both conceptual and implementation work. On the conceptual side, a sound analysis will be developed for resource consumption in Real-Time ABS, and formulated in first-order logic. The analysis will be materialized as an automated tool utilizing Z3 and integrated in the Real-Time ABS compiler.

Requirements

Recommended knowledge includes acquaintance or at least interest with areas like programming language semantics, type theory, programming logics.

References

[1] E. B. Johnsen, R. Schlatte, and S. L. T. Tarifa. “Integrating deployment architectures and resource con- sumption in timed object-oriented models”. In: J. Log. Algebr. Meth. Program. 84.1 (2015), pp. 67–91.

[2] L. M. de Moura and N. Bjørner. “Z3: An Efficient SMT Solver”. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Ed. by C. R. Ramakrishnan and J. Rehof. Vol. 4963. Lecture Notes in Computer Science. Springer, 2008, pp. 337–340.