A Formal Framework for Compositional Verification of Organic Computing Systems

Florian Nafz, Hella Seebach, Jan-Philipp Steghöfer, Simon Bäumler, and Wolfgang Reif

Because of their self-x properties Organic Computing systems are hard to verify. Nevertheless in safety critical domains one may want to give behavioral guarantees. One technique to reduce complexity of the overall verification task is applying composition theorem. In this paper we present a technique for formal specification and compositional verification of Organic Computing systems. Separation of self-x and functional behavior has amongst others, advantages for the formal specification. We present how the specification of self-x behavior can be integrated into an approach for compositional verification of concurrent systems, based on Interval Temporal Logic. The presented approach has full tool support with the KIV interactive theorem prover.
published 26.10.2010 in: Xi'an, China Proceedings of the 7th International Conference on Autonomic and Trusted Computing (ATC 2010)

Publisher: Springer