Abstract
Refining high-level system invariants into lower-level software obligations has been successfully employed in the design of ensemble-based systems. In order to obtain guarantees of design correctness, it is necessary to formalize the invariants in a form amenable to mathematical analysis. This paper provides such a formalization and demonstrates it in the context of the Invariant Refinement Method. The formalization is used to formally define invariant patterns at different levels of abstraction and with respect to different (soft) real-time constraints, and to provide proofs of theorems related to refinement among these patterns.
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
Abeywickrama, D.B., Bicocchi, N., Zambonelli, F.: SOTA: Towards a General Model for Self-Adaptive Systems. In: Proc. of WETICE, pp. 48–53. IEEE (2012)
Bures, T., Gerostathopoulos, I., Hnetynka, P., Keznikl, J., Kit, M., Plasil, F.: DEECo — an Ensemble-Based Component System. In: Proc. of CBSE 2013, Vancouver, Canada, pp. 81–90. ACM (June 2013)
Buttazzo, G.C.: Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications, 3rd edn. Springer (2011)
Darimont, R., van Lamsweerde, A.: Formal Refinement Patterns for Goal-Driven Requirements Elaboration. In: Gollmann, D. (ed.) FSE 1996. LNCS, vol. 1039, pp. 179–190. Springer, Heidelberg (1996)
Fuxman, A., Pistore, M., Mylopoulos, J., Traverso, P.: Model Checking Early Requirements Specifications in Tropos. In: Proc. of RE 2001, Toronto, ON, Canada, pp. 174–181. IEEE (August 2001)
Giorgini, P., Kolp, M., Mylopoulos, J., Pistore, M.: The Tropos Methodology: An Overview. In: Methodologies and Software Engineering For Agent Systems, pp. 89–106. Kluwer Academic Publishers (2004)
Hölz, M., Wirsing, M.: Towards a System Model for Ensembles. In: Formal modeling, pp. 241–261. Springer (2012)
Hölzl, M., et al.: Engineering Ensembles: A White Paper of the ASCENS Project. ASCENS Deliverable JD1.1 (2011), http://www.ascens-ist.eu/whitepapers
Hölzl, M., Rauschmayer, A., Wirsing, M.: Software engineering for ensembles. In: Wirsing, M., Banâtre, J.-P., Hölzl, M., Rauschmayer, A. (eds.) Soft-Ware Intensive Systems. LNCS, vol. 5380, pp. 45–63. Springer, Heidelberg (2008)
Keznikl, J., Bures, T., Plasil, F., Gerostathopoulos, I., Hnetynka, P., Hoch, N.: Design of Ensemble-Based Component Systems by Invariant Refinement. In: Proc. of CBSE 2013, Vancouver, Canada, pp. 91–100. ACM (June 2013)
Knapp, A., Störrle, H.: Efficient Representation of Timed UML 2 Interactions. In: Amyot, D., Fonseca i Casas, P., Mussbacher, G. (eds.) SAM 2014. LNCS, vol. 8769, pp. 110–125. Springer, Heidelberg (2014)
Koymans, R. (ed.): Specifying Message Passing and Time-Critical Systems with Temporal Logic. LNCS, vol. 651. Springer, Heidelberg (1992)
Lamsweerde, A.V.: Requirements engineering in the year 00: a research perspective. In: Proceedings of ICSE 2000, Limerick, Ireland, pp. 5–19. ACM (June 2000)
Serbedzija, N., Reiter, S., Ahrens, M., Velasco, J., Pinciroli, C., Hoch, N., Werther, B.: Requirement Specification and Scenario Description of the ASCENS Case Studies. Deliverable D7.1 (2011), http://www.ascens-ist.eu/deliverables
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Bureš, T., Gerostathopoulos, I., Keznikl, J., Plášil, F., Tůma, P. (2015). Formalization of Invariant Patterns for the Invariant Refinement Method. In: De Nicola, R., Hennicker, R. (eds) Software, Services, and Systems. Lecture Notes in Computer Science, vol 8950. Springer, Cham. https://doi.org/10.1007/978-3-319-15545-6_34
Download citation
DOI: https://doi.org/10.1007/978-3-319-15545-6_34
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15544-9
Online ISBN: 978-3-319-15545-6
eBook Packages: Computer ScienceComputer Science (R0)