Introduction
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.
This work has been partially funded by the Bavarian Ministry for Economics, Infrastructure, Traffic and Technology under the IuK initiative RAJA, IUK-0805-0005.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
UPPAAL Model Checker, http://www.uppaal.com/
Adam, L.: Verification of timed output-compatibility and timed input-compatibility in networks of timed input/output-automata. Submitted for ECRTS 2011 (2010)
Alur, R., Dill, D.: A theory of timed automata. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 45–73. Springer, Heidelberg (1992)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995 Part III. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Bowman, H.: Modelling timeouts without timelocks. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 334–353. Springer, Heidelberg (1999)
de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 108–122. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Adam, L. (2012). Performance Verification in Complex Enterprise-Level Component Systems. In: Barbosa, L.S., Lumpe, M. (eds) Formal Aspects of Component Software. FACS 2010. Lecture Notes in Computer Science, vol 6921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27269-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-27269-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27268-4
Online ISBN: 978-3-642-27269-1
eBook Packages: Computer ScienceComputer Science (R0)