Abstract
Complexity of software development has to be dealt with by dividing the different aspects and different views of the system and separating different concerns in the design. This implies the need of different modelling notations and tools to support more and more phases of the entire development process. To ensure the correctness of the models produced, the tools therefore need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensure high quality of such add-ins is to base them on sound formal foundations. This paper reports our experience in the work on the Common Component Modelling Example (CoCoME) and shows where such add-ins will fit. In particular, we show how the formal techniques developed in rCOS can be integrated into a component-based development process, and where it can be integrated in and provide extension to an existing successful commercial tool for adding formally supported checking, transformation and generation modules.
This work is partially supported by the projects HighQSoftD and HTTS funded by Macao Science and Technology Development Fund, NSFC-60673114 and 863 of China 2006AA01Z165.
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
Apache tuscany project, http://incubator.apache.org/tuscany/
The concurrency workbench, http://homepages.inf.ed.ac.uk/perdita/cwb/
Service component architecture, http://www.osoa.org/display/Main/Home
Back, R.J.R., von Eright, J.: Refinement Calculus: A Systematic Introduction. In: Graduate Texts in Computer Science, Springer, Heidelberg (1998)
Chandy, K., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Chen, X., He, J., Liu, Z., Zhan, N.: A model of component-based programing. In: Biryukov, A. (ed.) FSE 2007. LNCS, vol. 4593, Springer, Heidelberg (2007)
Chen, X., Liu, Z., Mencl, V.: Separation of Concerns and Consistent Integration in Requirements Modelling. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Plášil, F. (eds.) SOFSEM 2007. LNCS, vol. 4362, Springer, Heidelberg (2007)
Chen, Z., Hannousse, A.H., Van Hung, D., Knoll, I., Li, X., Liu, Y., Liu, Z., Nan, Q., Okika, J., Ravn, A.P., Stolz, V., Yang, L., Zhan, N.: The common component modelling example in rCOS. In: CoCoME—The Common Component Modelling Example. LNCS, Springer, Heidelberg (2007)
Chen, Z., Liu, Z., Stolz, V., Yang, L., Ravn, A.P.: A Refinement Driven Component-Based Design. In: Proc. of 12th IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2007), IEEE Computer Society Press, Los Alamitos (2007)
de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P.: Formal Methods for Components and Objects. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, Springer, Heidelberg (2004)
Flanagan, C., et al.: Extended Static Checking for Java. In: Pro. PLDI’ 2002 (2002)
Fowler, M., et al.: Refactoring: Improving the Design of Existing Code. Addison-Wesley, Reading (1999)
He, J., Li, X., Liu, Z.: Component-Based Software Engineering. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, Springer, Heidelberg (2005)
He, J., Li, X., Liu, Z.: rCOS: A refinement calculus for object systems. Theoretical Computer Science 365(1-2), 109–142 (2006)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)
Kruchten, P.: The Rational Unified Process—An Introduction. Addison-Wesley, Reading (2000)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Larman, C.: Applying UML and Patterns. Prentice-Hall, Englewood Cliffs (2001)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1-2), 134–152 (1997)
Leavens, J.L.: JML’s rich, inherited specification for behavioural subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, Springer, Heidelberg (2006)
Liu, X., Liu, Z., Zhao, L.: Object-oriented structure refinement—a graph transformational approach (Extended version submitted for journal publication). In: Intl. Workshop on Refinement (REFINE 2006). ENTCS (2006)
Liu, Z.: A continuous algebraic semantics of CSP. Journal of Computer Science and Technology 4(4), 304–314 (1989)
Liu, Z., He, J. (eds.): Mathematical Frameworks for Component software: Models for Analysis and Synthesis. In: Liu, Z., He, J. (eds.) Series on Component-Based Software Development, vol. 2, World Scientific, Singapore (2006)
Liu, Z., Ravn, A., Li, X.: Unifying proof methodologies of duration calculus and timed linear temporal logic. Formal Aspects of Computing 16(2), 140–154 (2004)
Martin, R.C.: Agile Software Development: Principles, Patterns, and Practices. Prentice-Hall, Englewood Cliffs (2003)
Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1992)
Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)
Tata Consultancy Services. MasterCraft, http://www.tata-mastercraft.com/
Zhou, C.C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Chen, Z., Li, X., Liu, Z., Stolz, V., Yang, L. (2007). Harnessing rCOS for Tool Support —The CoCoME Experience. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science, vol 4700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75221-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-75221-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75220-2
Online ISBN: 978-3-540-75221-9
eBook Packages: Computer ScienceComputer Science (R0)