Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Compositional analysis using component-oriented interpolation

: Nguyen, Viet Yen; Bittner, Benjamin; Katoen, Joost-Pieter; Noll, Thomas


Lanese, Ivan (Ed.); Madelaine, Eric (Ed.):
Formal aspects of component software. Revised selected papers : 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014
Cham: Springer, 2015 (Lecture Notes in Computer Science (LNCS) 8997)
ISBN: 978-331-91531-7-9
ISBN: 978-331-91531-6-2
International Symposium on Formal Aspects of Component Software (FACS) <11, 2014, Bertinoro>
Fraunhofer IESE ()
component-based system; verification; correctness; algorithm; model checking; formal analysis; formal method

We present a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components. It uses, given an invariant and a component of interest, bounded model checking (BMC) to quickly interpolate an abstraction of that component's environment. The abstraction may be refined by increasing the BMC bound. Furthermore, it is only defined over variables shared between the component and its environment, resulting in an aggressive abstraction with several applications. We demonstrate its use in a verification setting, as we report on our open source implementation in the NuSMV model checker which was used to perform a practical assessment with industrially-sized models from satellite case studies of ongoing missions. These models are expressed in a formalized dialect of the component-oriented and industrially standardized Architecture Analysis and Design Language (AADL).