University of Bamberg
open search form
You are here

Information Systems and Applied Computer Sciences

Software Technologies Research Group

  1.  University of bamberg
  2. Faculties
  3. Information Systems and Applied Computer Sciences
  4. Subject groups
  5. Computer Science
  6. Software Technologies Research Group
  7. Research
  8. Automatic Verification and Synthesis for Asynchronous Systems of Components

Automatic Verification and Synthesis for Asynchronous Systems of Components

The emergence of multi-core architectures and the advent of outsourcing local computing power to the cloud demands software developers to write code based on a set of software components that run concurrently, are distributed either locally or network-wide, and communicate by asynchronous message passing.  As the underlying developed systems are often required to be safety-critical, robust and reliable, guaranteeing their correctness becomes one of the most crucial tasks of software engineering.

This research project develops formal models for state-of-the-art programming paradigms and APIs, such as Grand-Central-Dispatch, which directly allow programmers to write code that is asynchronous and concurrent. Its goal is to support software engineers in writing such programs that due to their development are proven to be correct. Our research is based on formal models from automata theory and graph transition systems, and focusses on establishing (semi-)algorithms for automatic verification based on novel abstraction techniques. The project's long-term aim is the development of innovative algorithmic approaches to automatic synthesis, especially in the context of local and distributed scheduler synthesis, which are inspired from game theory (e.g., concurrent, imperfect information games) and machine learning (e.g., unsupervised gray/black-box learning).

The project's collaborators are Dr. Grégoire Sutre (LaBRI Bordeaux, France), Dr. Tristan Le Gall (CEA Saclay, France), Prof. Jean-Francois Raskin und Dr. Gilles Geeraerts (ULB Brüssel, Belgium), sowie Dr. Chris Poskitt (ETH Zürich, Switzerland).

Kontakt: Dr. Alexander Heußner

Publications:

  • Geeraerts, G., Heußner, A. and Raskin, J.-F. Queue-Dispatch Asynchronous Systems. 13th Intl. Conf. on Application of Concurrency to System Design (ACSD 2013), pp. 150-159, Barcelona, Spain, July 2013. IEEE.
  • Heußner, A., Le Gall, T. and Sutre, G. McScM: A general framework for the verification of communicating machines. In C. Flanagan and B. König, eds., 18th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), vol. 7214 of Lecture Notes in Computer Science, pp. 478-484, Tallinn, Estonia, March 2012. Springer-Verlag.
  • Heußner, A., Leroux, J., Muscholl, A. and Sutre, G. Reachability analysis of Communicating Pushdown Automata. Logical Methods in Computer Science, 8(3), 2012.