×

zbMATH — the first resource for mathematics

Multiple viewpoint contract-based specification and design. (English) Zbl 1209.68120
de Boer, Frank S. (ed.) et al., Formal methods for components and objects. 6th international symposium, FMCO 2007, Amsterdam, The Netherlands, October 24–26, 2007. Revised lectures. Berlin: Springer (ISBN 978-3-540-92187-5/pbk). Lecture Notes in Computer Science 5382, 200-225 (2008).
Summary: 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.
For the entire collection see [Zbl 1155.68012].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Damm, W.: Embedded system development for automotive applications: trends and challenges. In: Proceedings of the 6 th ACM & IEEE International conference on Embedded software (EMSOFT 2006), Seoul, Korea, October 22–25 (2006) · doi:10.1145/1176887.1176888
[2] 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)
[3] Sangiovanni-Vincentelli, A.: Reasoning about the trends and challenges of system level design. Proc. of the IEEE  95(3), 467–506 (2007) · doi:10.1109/JPROC.2006.890107
[4] 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) · doi:10.1109/ACSD.2005.35
[5] Meyer, B.: Applying ”design by contract”. IEEE Computer 25(10), 40–51 (1992) · Zbl 05090679 · doi:10.1109/2.161279
[6] Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8), 453–457 (1975) · Zbl 0308.68017 · doi:10.1145/360933.360975
[7] Lamport, L.: win and sin: Predicate transformers for concurrency. ACM Transactions on Programming Languages and Systems 12(3), 396–428 (1990) · doi:10.1145/78969.78970
[8] Back, R.J., von Wright, J.: Contracts, games, and refinement. Information and communication 156, 25–45 (2000) · Zbl 1046.68571 · doi:10.1006/inco.1999.2820
[9] Back, R.J., von Wright, J.: Refinement Calculus: A systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998) · Zbl 0949.68094 · doi:10.1007/978-1-4612-1674-2
[10] Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press (1989)
[11] Wolf, E.S.: Hierarchical Models of Synchronous Circuits for Formal Verification and Substitution. PhD thesis, Department of Computer Science, Stanford University (October 1995)
[12] 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)
[13] 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) · doi:10.1007/978-3-540-45212-6_9
[14] Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: Proceedings of the 13 th Annual Symposium on Foundations of Software Engineering (FSE 2005), pp. 31–40. ACM Press, New York (2005)
[15] Negulescu, R.: Process spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877. Springer, Heidelberg (2000) · Zbl 0999.68140
[16] Passerone, R.: Semantic Foundations for Heterogeneous Systems. PhD thesis, Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA 94720 (May 2004)
[17] Burch, J., Passerone, R., Sangiovanni-Vincentelli, A.: Overcoming heterophobia: Modeling concurrency in heterogeneous systems. In: Proceedings of the 2 nd International Conference on Application of Concurrency to System Design, Newcastle upon Tyne, UK, June 25–29 (2001) · doi:10.1109/CSD.2001.981761
[18] 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) · Zbl 0628.68025 · doi:10.1145/828.833
[19] Engelfriet, J.: Determinacy (observation equivalence = trace equivalence). Theoretical Computer Science 36, 21–25 (1985) · Zbl 0571.68018 · doi:10.1016/0304-3975(85)90028-3
[20] Brookes, S.D.: On the relationship of CCS and CSP. In: Díaz, J. (ed.) ICALP 1983. LNCS. vol. 154. Springer, Heidelberg (1983) · Zbl 0516.68024
[21] 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) · Zbl 05448730 · doi:10.1109/43.736561
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.