Abstract
We present the mathematical foundations and the design methodology of the contract-based model developed in the framework of the SPEEDS project. SPEEDS aims at developing methods and tools to support “speculative design”, a design methodology in which distributed designers develop different aspects of the overall system, in a concurrent but controlled way. Our generic mathematical model of contract supports this style of development. This is achieved by focusing on behaviors, by supporting the notion of “rich component” where diverse (functional and non-functional) aspects of the system can be considered and combined, by representing rich components via their set of associated contracts, and by formalizing the whole process of component composition.
This research has been developed in the framework of the European IP-SPEEDS project number 033471.
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.
Similar content being viewed by others
References
Damm, W.: Embedded system development for automotive applications: trends and challenges. In: Proceedings of the 6th ACM & IEEE International conference on Embedded software (EMSOFT 2006), Seoul, Korea, October 22–25 (2006)
Butz, H.: The Airbus approach to open Integrated Modular Avionics (IMA): technology, functions, industrial processes and future development road map. In: International Workshop on Aircraft System Technologies, Hamburg (March 2007)
Sangiovanni-Vincentelli, A.: Reasoning about the trends and challenges of system level design. Proc. of the IEEE 95(3), 467–506 (2007)
Damm, W.: Controlling speculative design processes using rich component models. In: Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), St. Malo, France, June 6–9, pp. 118–119 (2005)
Meyer, B.: Applying ”design by contract”. IEEE Computer 25(10), 40–51 (1992)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8), 453–457 (1975)
Lamport, L.: win and sin: Predicate transformers for concurrency. ACM Transactions on Programming Languages and Systems 12(3), 396–428 (1990)
Back, R.J., von Wright, J.: Contracts, games, and refinement. Information and communication 156, 25–45 (2000)
Back, R.J., von Wright, J.: Refinement Calculus: A systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)
Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press (1989)
Wolf, E.S.: Hierarchical Models of Synchronous Circuits for Formal Verification and Substitution. PhD thesis, Department of Computer Science, Stanford University (October 1995)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering, pp. 109–120. ACM Press, New York (2001)
Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117–133. Springer, Heidelberg (2003)
Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: Proceedings of the 13th Annual Symposium on Foundations of Software Engineering (FSE 2005), pp. 31–40. ACM Press, New York (2005)
Negulescu, R.: Process spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877. Springer, Heidelberg (2000)
Passerone, R.: Semantic Foundations for Heterogeneous Systems. PhD thesis, Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA 94720 (May 2004)
Burch, J., Passerone, R., Sangiovanni-Vincentelli, A.: Overcoming heterophobia: Modeling concurrency in heterogeneous systems. In: Proceedings of the 2nd International Conference on Application of Concurrency to System Design, Newcastle upon Tyne, UK, June 25–29 (2001)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the Association for Computing Machinery 31(3), 560–599 (1984)
Engelfriet, J.: Determinacy → (observation equivalence = trace equivalence). Theoretical Computer Science 36, 21–25 (1985)
Brookes, S.D.: On the relationship of CCS and CSP. In: Díaz, J. (ed.) ICALP 1983. LNCS. vol. 154. Springer, Heidelberg (1983)
Lee, E.A., Sangiovanni-Vincentelli, A.L.: A framework for comparing models of computation. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems 17(12), 1217–1229 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C. (2008). Multiple Viewpoint Contract-Based Specification and Design . In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2007. Lecture Notes in Computer Science, vol 5382. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92188-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-92188-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-92187-5
Online ISBN: 978-3-540-92188-2
eBook Packages: Computer ScienceComputer Science (R0)