A refinement calculus for software components and architectures
Pages 377 - 380
Abstract
The complexity and ubiquity achieved by software in the present world makes it imperative, more than ever, the availability of both technologies and sound methods to drive its development. Programming 'in--the--large', component--based programming and software architecture are popular expressions which embody this concern and correspond to driving forces in current software engineering. In such a context, this paper reports on the research, which constitutes the PhD project of the author, on a formal calculus for reasoning about and transforming component--based architectures.
References
[1]
N. Aguirre and T. Maibaum. A logical basis for the specification of reconfigurable component-based systems. In FASE'03, Proceedings of the Formal Aspects of Software Engineering ETAPS Conference, Warsaw, April 2003. Springer Lect. Notes Comp. Sci (2621).]]
[2]
R. Allen and D. Garlan. A formal basis for architectural connection. ACM TOSEM, 6(3):213--249, 1997.]]
[3]
F. Arbab. Abstract behaviour types: a foundation model for components and their composition. In F. S. de Boer, M. Bonsangue, S. Graf, and W.-P. de Roever, editors, Proc. First International Symposium on Formal Methods for Components and Objects (FMCO'02), pages 33--70. Springer Lect. Notes Comp. Sci. (2852), 2003.]]
[4]
F. Arbab and J. Rutten. A coinductive calculus of component connectors. pages 35--56. Springer Lect. Notes Comp. Sci. (2755), 2003.]]
[5]
R. Backhouse, P. Jansson, J. Jeuring, and L. Meertens. Generic programming --- an introduction. In LNCS, volume 1608, pages 28--115. Springer-Verlag, 1999. Revised version of lecture notes for AFP'98.]]
[6]
R. C. Backhouse and P. F. Hoogendijk. Elements of a relational theory of datatypes. In B. Möller, H. Partsch, and S. Schuman, editors, Formal Program Development, pages 7--42. Springer Lect. Notes Comp. Sci. (755), 1993.]]
[7]
L. S. Barbosa. Components as processes: An exercise in coalgebraic modeling. In S. F. Smith and C. L. Talcott, editors, FMOODS'2000 - Formal Methods for Open Object-Oriented Distributed Systems, pages 397--417. Kluwer Academic Publishers, September 2000.]]
[8]
L. S. Barbosa. Towards a Calculus of State-based Software Components. Journal of Universal Computer Science, 9(8):891--909, August 2003.]]
[9]
L. S. Barbosa and J. N. Oliveira. State-based components made generic. In H. P. Gumm, editor, CMCS'03, Elect. Notes in Theor. Comp. Sci., volume 82.1. Elsevier, 2003.]]
[10]
M. Barbosa and L. Barbosa. A Relational Model for Component Interconnection. Journal of Universal Computer Science, 10(7):808--823, July 2004.]]
[11]
M. A. Barbosa and L. S. Barbosa. Specifying software connectors. In K. Araki and Z. Liu, editors, 1st International Colloquium on Theorectical Aspects of Computing (ICTAC'04), pages 53--68, Guiyang, China, September 2004. Springer Lect. Notes Comp. Sci. (3407).]]
[12]
M. A. Barbosa and L. S. Barbosa. Towards a relational model for component interconnection. In R. Lins, C. Braga, and F. Chalub, editors, Proc. 8th Brazilian Symposium on Programming Languages, pages 17--30, Niteroi, Brasil, May 2004.]]
[13]
R. Bird and O. Moor. The Algebra of Programming. Series in Computer Science. Prentice-Hall International, 1997.]]
[14]
M. Broy. (Inter-)Action Refinement: The Easy Way, volume 118 of Series F: Computer and System Sciences. Springer NATO ASI Series, 1993.]]
[15]
M. Broy. Compositional refinement of interactive systems. J. ACM, 44(6):850--891, 1997.]]
[16]
J. Derrick and E. Boiten. Refinement in Z and Object-Z: Foundations and Advanced Applications. FACIT. Springer-Verlag, 2001.]]
[17]
D. Garlan. Formal modeling and analysis of software architecture: Components, connectors and events. In M. Bernardo and P. Inverardi, editors, Third International Summer School on Formal Methods for the Design of Computer, Communication and Software Systems: Software Architectures (SFM 2003). Springer Lect. Notes Comp. Sci, Tutorial, (2804), Bertinoro, Italy, September 2003.]]
[18]
D. Garlan and M. Shaw. An introduction to software architecture. In V. Ambriola and G. Tortora, editors, Advances in Software Engineering and Knowledge Engineering (volume I). World Scientific Publishing Co., 1993.]]
[19]
J. Goguen. Parametrised programming and software architectures. In Symposium on Software Reusability. IEEE, 1996.]]
[20]
C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271--281, 1972.]]
[21]
B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222--159, 1997.]]
[22]
C. B. Jones. Accommodating interference in the formal design of concurrent object-based programs. Formal Methods in System Design, 8(2):105--122, 1996.]]
[23]
Z. Liu, H. Jifeng, and X. Li. Towards a formal use of uml for software requirement analysis. In Proceedings of PDPTA'2001, USA, 2001.]]
[24]
E. Meijer. Server-side scripting in haskell. Journal of Functional Programming, 2000.]]
[25]
S. Meng and L. S. Barbosa. On refinement of generic software components. In C. Rettray, S. Maharaj, and C. Shankland, editors, 10th Int. Conf. Algebraic Methods and Software Technology (AMAST), pages 506--520, Stirling, 2004. Springer Lect. Notes Comp. Sci. (3116).]]
[26]
A. Mikhajlova and E. Sekerinski. Class refinement and interface refinement in object-oriented program. In Proc. 4th Int. Formal Methods Europe Symposium, pages 82--101. Springer Lect. Notes Comp. Sci. (1313), 1997.]]
[27]
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Technical Report -86, 1989.]]
[28]
M. Moriconi and X. Qian. Correctness and composition of software architectures. In Second Symposium on Foundations of Software Engineering, pages 164--174. ACM Press, 1994.]]
[29]
M. Moriconi, X. Qian, and R. A. Riemenschneider. Correct architecture refinement. IEEE Transactions on Software Engineering, 21(4):356--3, 1995.]]
[30]
G. Papadopoulos and F. Arbab. Coordination models and languages. In Advances in Computers --- The Engineering of Large Systems, volume 46, pages 329--400. 1998.]]
[31]
J. Philipps and B. Rumpe. Refinement of pipe-and-filter architectures. In J. M. Wing, J. Woodcock, and J. Davies, editors, FM'99, Proceedings of the World Congress on Formal Methods in the Development of Computing System, pages 96--115. Springer Lect. Notes Comp. Sci. (1708), 1999.]]
[32]
W.-P. d. Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison, volume 47 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.]]
[33]
J. Rutten. Universal coalgebra: A theory of systems. Theor. Comp. Sci., 249(1):3--80, 2000. (Revised version of CWI Techn. Rep. CS-R9652, 1996).]]
[34]
J. M. Spivey. The Z Notation: A Reference Manual (2nd ed). Series in Computer Science. Prentice-Hall International, 1992.]]
[35]
M. Sun, B. K. Aichernig, L. S. Barbosa, and Z. Naixiao. A coalgebraic semantic framework for component based development in UML. In L. Birkedal, editor, Proc. Int. Conf. on Category Theory and Computer Science (CTCS'04), volume 122, pages 229--245. Elect. Notes in Theor. Comp. Sci., Elsevier, 2005.]]
[36]
M. Sun, Z. Naixiao, and L. S. Barbosa. On semantics and refinement of UML statecharts: A coalgebraic view. In J. Cuellar and Z. Liu, editors, Proc. of 2nd IEEE Int. Conf. on Software Engineering and Formal Methods, pages 164--173, Beijing, China, September 2004. IEEE Computer Society Press.]]
Index Terms
- A refinement calculus for software components and architectures
Recommendations
A refinement calculus for software components and architectures
The complexity and ubiquity achieved by software in the present world makes it imperative, more than ever, the availability of both technologies and sound methods to drive its development. Programming 'in--the--large', component--based programming and ...
A refinement calculus for logic programs
Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming ...
Refinement to Imperative HOL
Many algorithms can be implemented most efficiently with imperative data structures. This paper presents Sepref, a stepwise refinement based tool chain for the verification of imperative algorithms in Isabelle/HOL. As a back end we use imperative HOL, ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2005
402 pages
Copyright © 2005 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 September 2005
Check for updates
Author Tags
Qualifiers
- Article
Conference
ESEC/FSE05: Joint 10th European Software Engineering Conference 2005
September 5 - 9, 2005
Lisbon, Portugal
Acceptance Rates
Overall Acceptance Rate 112 of 543 submissions, 21%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations4Total Citations
- 518Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 28 Feb 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in