Ernst-Rüdiger Olderog - Model Checking, Synthesis, and Learning: Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday

The traditional measure of quality assurance is testing. Verification, or even the synthesis of programs were considered the higher art of achieving system reliability, accomplished via so-called formal methods. Practice has shown, however, that there are no ways around test-based quality assurance: the verification problems are typically undecidable, and even if they were decidable, they would only cover a certain level of abstraction and not the entire system as it runs in its productive environment.

This Festschrift, dedicated to Bengt Jonsson on the occasion of his 60th birthday, indicates such a return to the basics. While the beginning of Bengts career was clearly devoted to verfication, later he became interested in test-based methods, which of course he approached in a truly formal methods-based fashion. And always with the goal to reach the stars, or, more technically expressed, to do battle with the limits of decidability. The nine invited contributions and the corresponding wealth of references to Bengts work provided in this Festschrift illustrate the style and influence of his trendsetting efforts.

Reliability is a central concern of software system development. It can be approached in three ways, in a post-mortem fashion via verification of an unknown artefact, by construction applying correctness preserving steps, and via testing of the final product. In this paper, we introduce the nine contributions to the Festschrift dedicated to Bengt Jonsson on the occasion of his 60th birthday. Verification is addressed here from the model checking perspective, correctness by construction via synthesis, and testing as both a means and a as by-product of active automata learning while reflecting on the impact Bengt had on these developments.