Jähnig, NilsGöthel, ThomasGlesner, Sabine2020-03-092020-03-092016-06-23978-3-319-41590-1978-3-319-41591-80302-9743https://depositonce.tu-berlin.de/handle/11303/10899http://dx.doi.org/10.14279/depositonce-9792Formal model refinement aims at preserving safety and liveness properties of models. However, there is usually a verification gap between model and executed code, especially if concurrent processes are involved. The reason for this is that a manual implementation and further code optimizations can introduce implementation errors. In this paper, we present a framework that allows for formally proving a failures refinement between a CSP specification and its low-level implementation. The implementation is given in a generic unstructured language with gotos and an abstract communication instruction. We provide a failures-based denotational semantics of it with an appropriate Hoare calculus. Since failures-based refinement is compositional w.r.t. parallel composition of concurrent components and preserves safety and liveness properties, this contributes to reducing the verification gap between high-level specifications and their low-level implementations.en005 Computerprogrammierung, Programme, Datengotosunstructured codeformal semanticsHoare calculusCSPfailures refinementConference Object1611-3349