The aim of our DAAD ppp project SMT4ABS is to bring together researchers from the field of program analysis on the one hand, and SMT solving on the other hand, to exploit the power of modern SMT-solving technologies for the analysis of real-time systems.

 

Funding

This project has been supported 2015-2016 by the DAAD ppp exchange program.

 

Team

RWTH Aachen University, Germany
      Erika Abraham
      Florian Corzilius
      Gereon Kremer
  University of Oslo, Norway
      Einar Broch Johnsen
      Ka I Violet Pun
      Martin Steffen
      S. Lizeth Tapia Tarifa
      Ingrid Chieh Yu

 

Contents

Real-time systems are systems, whose correct functioning requires not only correct data computations, but also that the durations (response times) of those computations do not exceed some upper limits (response time deadlines). For soft real-time systems the impact of a few missed response time deadlines can be neglected, but missing too many deadlines can lead to, e.g., a reduced system quality. However, keeping the deadlines is absolutely crucial for the correctness and safety of hard real-time systems, where the violation of a response time deadline can lead to high-risk situations such as danger to life. In this project we focus on hard real-time software systems. Some examples are autopilot programs, automotive control software, programmable logic controller (PLC) programs controlling the physical state of chemical plants, or computer assistance systems for surgeries.
We consider the ABS (abstract behavioral specification) language, co-developed by the Norwegian partner of this proposal. ABS can be used to design executable models of distributed object-oriented systems, including their real-time behavior. It combines advanced concurrency and synchronization mechanisms for concurrent object groups with a functional language for modeling data. ABS uses asynchronous method calls, interfaces for encapsulation, and cooperative scheduling of method invocations inside concurrent objects. This feature combination results in a concurrent object-oriented model which is inherently compositional. Recently, the on-going EU FP7 project Envisage, coordinated by the Norwegian partner of this proposal, has extended ABS to the development of scalable, virtualized systems for deployment on the cloud. This extension supports dynamic deployment decisions and resource management strategies at runtime.
The analysis of the real-time behavior of dynamically deployed ABS programs involves the satisfiability check of real-arithmetic constraint systems, i.e., Boolean combinations of constraints comparing polynomial expressions over real-valued variables. Though there are pure algebraic techniques, their heuristic embedding in SAT-modulo-theories (SMT) solving shaped up as much more efficient in practice. SMT solvers for real arithmetic use highly tuned SAT-solving techniques to find solutions for the Boolean structure of a real-arithmetic problem. The Boolean solutions are validated in the underlying theory using real-algebraic decision procedures like, e.g., the virtual substitution method (VS) , the cylindrical algebraic decomposition (CAD) method, or methods using Gröbner bases.
The German partners maintain SMT-RAT, an open-source C++ library providing real-arithmetic theory modules for the development of SMT solvers. Besides basic algebraic computations, the library contains implementations of all three above-mentioned real-algebraic decision procedures, extended with further functionalities like, e.g., incrementality and the generation of explanations for infeasibility, to make them SMT-compliant. Further modules are available for preprocessing and solving linear problems. To improve the applicability, SMT-RAT supports the problem-dependent composition of its modules to  SMT-solving strategies.

Problem statement

We are interested in compositional verification techniques to prove a fundamental form of service-level agreement: that the response of a program or a program fragment is always delivered within a given deadline. We study this problem in the context of dynamic deployment and resource management strategies which are relevant both for embedded devices and for virtualized programs and cloud computing, based on the notion of design by contract. Such techniques allow the program developer to predict the behavior of a program before it is deployed, in contrast to the techniques currently in use, which assess timing behavior after deployment.
Problem 1: Deadline specification As a basis, we need a formalism to specify hard real-time deadline requirements, execution cost, and resource provisioning for software running on (virtualized) deployment architectures.
Problem 2: Response time computation As hard real-time systems are inherently safety critical, their safety analysis is of high importance. To analyze their real-time behavior, some of the available techniques use simulation to specify lower bounds on the response times, and can therefore prove deadline violations. Other techniques are available to determine upper response time bounds on the computation of single operations on a fixed hardware architecture, where the bounds might depend also on the operands’ values. Having such bounds for atomic statements, we aim at computing upper bounds on the response times of (terminating) program fragments on virtualized architectures. These computations can be quite challenging for complex program structures and data types, for example in the presence of loops, dynamically created and deployed objects, and recursive method calls.
Problem 3: Proof of the absence of deadline violations The computed method response time bounds are often complex non-linear real-arithmetic expressions, where the variables represent method parameters. Therefore, in order to decide whether the response time of a method always satisfies its deadline, we need to decide a real-arithmetic problem. Though the logic of real arithmetic is decidable, solving real-arithmetic formulas is hard: quantifier elimination is in general doubly exponential in the number of variables (singly exponential for the existential fragment, which we need to solve here).

Project goals

In our project, we tackle the above problems as follows:
Goal 1: Type system extension to cover deadlines To reflect the importance of the time behavior of hard real-time systems, we want to specify response time deadlines in ABS at the basic level of types: the type of methods gets extended with a new component to specify their deadlines. This allows the design by contract methodology to be extended to real-time behavior.
Goal 2: Type checking rules We assume that (verified) upper bounds on the computation times for atomic operations are available as functions of the operands. Using this input, we want to extend the type checking system of ABS to cover the check whether all method response time deadlines can be guaranteed. The corresponding type checking rules should allow the automatic derivation of upper bounds on the response times of program fragments (parameterized in, e.g., method parameters). Type correctness requires that the derived upper bounds for methods do not exceed their deadlines.
Goal 3: Automated type checking During type checking, complex real-arithmetic expressions are computed as upper bounds on response times. Firstly, we want to apply available SMT-solving technologies for the on-the-fly reduction of these expressions during their generation. Secondly, we want to use advanced SMT-solving techniques to check the type correctness conditions, stating that the resulting upper bounds on the method response times are less or equal their deadlines.

To achieve the above goals, we start with restricted forms of the ABS language and of the response time specifications, and extend both the language and the expressivity of the specifications in a stepwise manner. In the first phase we consider the simple setting of sequential programs without loops and recursion, where the execution time of atomic statements is constant. In the second phase we extend the language with non-constant execution time for atomic statements, loops and recursion (depending, e.g., on the input to methods and the state of objects), and finally in the third phase with parallelism. For the latter, we consider extending the type system with permissions.