Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Generating component interfaces by integrating static and symbolic analysis, learning, and runtime monitoring

: Howar, Falk; Giannakopoulou, Dimitra; Mues, Malte; Navas, Jorge


Margaria-Steffen, T.:
Leveraging applications of formal methods, verification and validation. 8th International Symposium, ISoLA 2018. Pt.2: Verification : Limassol, Cyprus, November 5-9, 2018; Proceedings
Cham: Springer International Publishing, 2018 (Lecture Notes in Computer Science 11245)
ISBN: 978-3-030-03420-7 (Print)
ISBN: 978-3-030-03421-4 (Online)
ISBN: 3-030-03420-8
International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) <8, 2018, Limassol>
Fraunhofer ISST ()

Behavioral interfaces describe the safe interactions with a component without exposing its internal variables and computation. As such, they can serve as documentation or formal contracts for black-box components in safety-critical systems. Learning-based generation of interaces relies on learning algorithms for inferring behavioral interfaces from observations, which are in turn checked for correctness by formal analysis techniques. Learning-based interface generation is therefore an interesting target when studying integration and combination of different formal analysis methods. In this paper, which accompanies an invited talk at the ISoLA 2018 track “A Broader View on Verification: From Static to Runtime and Back”, we introduce interpolation and symbolic search for validating inferred interfaces. We discuss briefly how interface validation may utilize information from runtime monitoring.