On the use of formal specifications as part of running programs

Issues related to large scale systems made of autonomous components encompass interoperability among independently developed software and adaptability to changing environmental conditions. Formal specifications are traditionally used at design time for software engineering tasks. However, recently, several attempts of using formal specifications at run-time have been realised that let envisage a future use of formal specifications at run-time that will enhance interoperability and adaptability of autonomous components. This paper intends to highlight the potentialities of the use of formal specifications at run-time as a support for the correct execution of such components. This paper reviews and discusses the use of formal specifications at run-time from different perspectives: software engineering, run-time code evolution, adaptive middleware, trust and security, or business applications. It highlights the potentialities of the use of formal specifications at run-time as a support for interoperability and adaptability of interacting autonomous components. It identifies as well application domains and open issues related to the combination of specifications and code in the framework of large scale systems.