Abstract
The end product of architecting is an architectural hierarchy, a collection of architectural descriptions linked by mappings that interpret the more abstract descriptions in the more concrete descriptions. Formalized transformational approaches to architecture refinement and abstraction have been proposed. One argument in favor of formalization is that it can result in architectural implementations that are guaranteed to be correct, relative to the abstract descriptions. If these are correct with respect to one another, conclusions obtained by reasoning from an abstract architectural description will also apply to the implemented architecture. But this correctness guarantee is achieved by requiring that the implementer use only verified transformations, i.e., ones that have been proven to produce correct results when applied. This paper explores an approach that allows the implementer to use transformations that have not been proven to be generally correct, without voiding the correctness guarantee. Checking means determining that application of the transformation produces the desired result. It allows the use of transformations that have not been generally verified, even ones that are known to sometimes produce incorrect results, by showing that they work in the particular case.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35563-4_35
Chapter PDF
References
Abowd, G., Allen, R., and Garlan, D., (1995) Formalizing style to understand descriptions of software architecture. Tech. Rep. CMU-CS-95–111, School of Computer Science, Carnegie Mellon University.
Brinksma, E., Jonsson, B., and Orava, F., (1991), Refining interfaces of communicating systems. Proceedings of TAPSOFT’91, S. Abramsky and T.S.E. Maibaum, Eds., Springer-Verlag, pp. 71–80
Broy, M. (1992), Compositional refinement of interactive systems. Tech. Rep. No. 89, Digital Systems Research Center, Palo Alto.
Enderton, H. B. (1972), A Mathematical Introduction to Logic. Academic Press.
Garlan, D., Allen, R., and Ockerbloom, J. (1994), Exploiting style in architectural design environments. In Proceedings 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering SIGSOFT ‘84, ACM Press, pp. 179–185.
Garlan, D., Monroe, R.–T., and Wile, D. (1997), Acme: An archiectural description interchange language. In Proceedings of CASCON ‘87. Available at http://www.cs.cmu.edu/afs/cs/project/abel/www/acme-web/ v3.0/white-paper-v3.0/white-paper.html.
Hodges, W. (1993), Model Theory. Cambridge University Press.
Lemmon, E. J. (1987), Beginning Logic,second ed. Chapman and Hall.
Luckham, D. C., Augustin, L. M., Kenney, J. J., Vera, J., Bryan, D., and Mann, W. (1995), Specification and analysis of system architecture using Rapide. IEEE Transactions on Software Engineering 21, 4, pp. 314–335.
Mates, B. (1972), Elementary Logic,second ed. Oxford University Press.
Moriconi, M., and Qian, X. (1994), Correctness and composition of software architectures. In Proceedings 2nd ACM Symposium on Foundations of Software Engineering (SIGSOFT ‘84), ACM Press, pp. 164–174.
Moriconi, M., Qian, X., and Riemenschneider, R. A. (1995), Correct architecture refinement. IEEE Transactions on Software Engineering 21, 4, 356 - 372. Available at http://www.csl.sri.com/sadl/tse95.ps.gz.
Moriconi, M., Qian, X., Riemenschneider, R. A., and Gong, L. (1997), Secure software architectures. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, pp. 84 - 93. Available at http://www.csl.sri.com/sadl/sp97.ps.gz.
Moriconi, M., and Riemenschneider, R. A. (1997), Introduction to SADL 1.0: A language for specifying software architecture hierarchies. Tech. Rep. SRI-CSL-97–01, Computer Science Laboratory, SRI International. Available at http://www.cs1.sri.corn/sadl/sadl-intro.ps.gz.
Necula, G. C., and Lee, P. (1998), The design and implementation of a certifying compiler. Submitted to PLDI ‘88. Available at http://www.cs.cmu.edu/-necula/pldi98.ps.gz.
Necula, G. C., and Lee, P. (1996), Proof-carrying code. Tech. Rep. CMU-CS-96–165, School of Computer Science, Carnegie Mellon University. Available at http://www.cs.cmu.edu/-necula/tr96-165.ps.gz.
Necula, G. C., and Lee, P. (1997) Efficient representation and validation of logical proofs. Tech. Rep. CMU-CS-97–172, School of Computer Science, Carnegie Mellon University,. Available at http://www.cs.cmu.edu/-necula/tr97–172.ps.gz.
Owre, S., Rushby, J. M., and Shankar, N. (1992), PVS: A prototype verification system. In 11th International Conference on Automated Deduction (CADE) (Saratoga, NY,), D. Kapur, Ed., vol. 607 of Lecture Notes in Artificial Intelligence, Springer-Verlag, pp. 748–752.
Philipps, J., and Rumpe, B. (1997), Refinement of information flow architectures. In Proceedings of the First IEEE International Conference of Formal Engineering Methods (ICFEM ‘87), pp. 203–212. Available at http://www4.informatik.tumuenchen.de/papers/icfem_rumpe_1997_Publication.html.
Riemenschneider, R. A. (1997), A simplified method for establishing the correctness of architectural refinements. SRI CSL Dependable System Archiecture Group, Working Paper DSA-97–02. Available at http://www.cs1.sri.com/sadl/simplified.ps.gz..
Riemenschneider, R. A. (1998), Correct transformation rules for incremental development of architecture hierarchies. SRI CSL Dependable System Archiecture Group, Working Paper DSA-98–01. Available at http://wwwcs1.sri.com/sadl/incremental.ps.gz.
Shoenfield, J. R. (1967), Mathematical Logic. Addison-Wesley.
X/Open Company. (1993), Distributed Transaction Processing: Reference Model. Apex Plaza, Forbury Road, Reading, Berkshire RG1 lAX, U.K., November 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Riemenschneider, R.A. (1999). Checking the Correctness of Architectural Transformation Steps via Proof-Carrying Architectures. In: Donohoe, P. (eds) Software Architecture. WICSA 1999. IFIP — The International Federation for Information Processing, vol 12. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35563-4_5
Download citation
DOI: https://doi.org/10.1007/978-0-387-35563-4_5
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6536-6
Online ISBN: 978-0-387-35563-4
eBook Packages: Springer Book Archive