Abstract
Designing concurrent or distributed systems with complex architectures while preserving a set of high-level requirements through all design steps is not a trivial task. Building upon a generic notion of contract framework which relies on a component framework and two refinement relations: conformance and refinement under context, we provide a condition under which circular reasoning can be used for checking dominance, i.e. refinement between contracts. We then propose an instantiation of such a contract framework for safety and progress requirements in component systems with data exchange. This allows us to prove non-trivial properties of a protocol for tree-like networks.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Meyer, B.: Applying ”design by contract”. IEEE Computer 25(10), 40–51 (1992)
Quinton, S., Graf, S.: Contract-based verification of hierarchical systems of components. In: Proc. of SEFM 2008, pp. 377–381. IEEE Computer Society, Los Alamitos (2008)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Specification, vol. 1. Springer, Heidelberg (1991)
Sifakis, J.: A framework for component-based construction. In: Proc. of SEFM 2005, pp. 293–300. IEEE Computer Society, Los Alamitos (2005)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proc. of ESEC/SIGSOFT FSE 2001, pp. 109–120. ACM Press, New York (2001)
Bidinger, P., Stefani, J.B.: The Kell calculus: operational semantics and type systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 109–123. Springer, Heidelberg (2003)
Arbab, F.: Reo: a channel-based coordination model for component composition. Mathematical Strucutres in Computer Science 14(3) (2004)
Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Proc. of SEFM 2006, pp. 3–12. IEEE Computer Society, Los Alamitos (2006)
Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200–225. Springer, Heidelberg (2008)
Ben-Hafaiedh, I., Graf, S., Quinton, S.: A contract framework for reasoning about safety and progress. Technical Report TR-2010-11, Verimag (2010)
Stadler, Z., Grumberg, O.: Network grammars, communication behaviours and automatic verification. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1990)
Bliudze, S., Sifakis, J.: The algebra of connectors: structuring interaction in BIP. In: Proc. of EMSOFT 2007, pp. 11–20. ACM Press, New York (2007)
Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for performance optimization in BIP. In: Proc. of SIES 2009, pp. 152–160 (2009)
Datta, A.K., Devismes, S., Horn, F., Larmore, L.L.: Self-stabilizing k-out-of-l exclusion on tree network. CoRR abs/0812.1093 (2008)
de Roever, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods, vol. 54. Cambridge University Press, Cambridge (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ben-Hafaiedh, I., Graf, S., Quinton, S. (2010). Reasoning about Safety and Progress Using Contracts. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-16901-4_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16900-7
Online ISBN: 978-3-642-16901-4
eBook Packages: Computer ScienceComputer Science (R0)