Abstract
We survey compositionality results for three classes of system properties: invariance/safety properties and liveness properties (based on work by Abadi and Lamport), and confidentiality properties (based on work by Mantel). We then analyse the difficulties which occur when trying to apply the compositionality results of these classes of properties simultaneously.
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
Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
Birolini, A.: Reliability Engineering: Theory and Practice, 3rd edn. Springer, Heidelberg (1999)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Charpentier, M., Chandy, K.M.: Theorems about composition. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 167–186. Springer, Heidelberg (2000)
Crnković, I., Larsson, M., Preiss, O.: Concerning predictability in dependable component-based systems: Classification of quality attributes. In: de Lemos, R., Gacek, C., Romanovsky, A. (eds.) Architecting Dependable Systems III. LNCS, vol. 3549, pp. 257–278. Springer, Heidelberg (2005)
Johnson, D.M., Thayer, F.J.: Security and the composition of machines. In: Proc. IEEE Computer Security Foundations Workshop, pp. 72–89 (1988)
Kindler, E.: Safety and liveness properties: A survey. EATCS-Bulletin 53 (June 1994)
Lyu, M.R. (ed.): Handbook of Software Reliability Engineering. McGraw-Hill and IEEE Computer Society (1996)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: Specification. Springer, Heidelberg (1991)
Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, Heidelberg (1995)
Mantel, H.: Possibilistic definitions of security - An assembly kit. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000). IEEE Computer Society Press, Cambridge (2000)
Mantel, H.: A Uniform Framework for the Formal Specification and Verification of Information Flow Security. PhD thesis, Universität des Saarlandes (2003)
McLean, J.: A general theroy of composition for trace sets closed under selective interleaving functions. In: Proc. IEEE Symposium on Research in Security and Privacy, pp. 73–93 (1994)
McLean, J.: A general theory of composition for a class of “possibilistic” properties. IEEE Transactions on Software Engineering 22(1), 53–67 (1996); Special Section—Best Papers of the IEEE Symposium on Security and Privacy (1994)
Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object- Oriented Programming, 2nd edn. ACM Press and Addison-Wesley, New York (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Freiling, F.C., Santen, T. (2006). On the Composition of Compositional Reasoning. In: Reussner, R.H., Stafford, J.A., Szyperski, C.A. (eds) Architecting Systems with Trustworthy Components. Lecture Notes in Computer Science, vol 3938. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11786160_8
Download citation
DOI: https://doi.org/10.1007/11786160_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35800-8
Online ISBN: 978-3-540-35833-6
eBook Packages: Computer ScienceComputer Science (R0)