Performance verification in complex enterprise-level component systems

Abstract

More and more complex enterprise-scale systems are considered to be time critical: These applications provide a correct functionality only if certain time constraints for their program execution are met. In these time-critical environments, the aspect of performance becomes a relevant functional aspect and needs to be verifiable.We aim to find a solution for this problem by providing a practical approach for the implementation of complex enterprise-level systems, whose timing properties can be formally verified. In the following we concentrate on the formal aspects of our work by giving an overview on a methodology for the formal specification of timed component behaviour and its verification in Sect. 2. We then outline our current work on using this methodology to verify execution constraints within component services in Sect. 3. © 2012 Springer-Verlag.