Abstract
The formal methods, fault-tolerance, and cyber-security research communities explore models that differ from each other. The differences frustrate efforts at cross-community collaboration. Moreover, ignorance about these differences means the status quo is likely to persist. This paper discusses two of the key differences: (i) the trace-based semantic foundation for formal methods and (ii) the implicit notions of independence.
Supported in part by National Science Foundation grants 0430161, 0964409, and CCF-0424422 (TRUST), ONR grants N00014-01-1-0968 and N00014-09-1-0652, and a grant from Microsoft. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of these organizations or the U.S. Government.
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
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Computing 2(3), 117–126 (1987)
Clarkson, M., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18(6), 1157–1210 (2010)
Forrest, S., Somayaji, A., Ackley, D.H.: Building diverse computer systems. In: Proc. 6th Workshop on Hot Topics in Operating Systems, pp. 67–72. IEEE Computer Science Press, Los Alamitos (1997)
Knight, J.C., Leveson, N.G.: An experimental evaluation of the assumption of independence in multiversion programming. IEEE Transactions on Software. Engineering 12(1), 96–109 (1986)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)
Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Transactions on Programming Languages 4(3), 382–401 (1982)
Randell, B.: On failures and faults. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 18–39. Springer, Heidelberg (2003)
Roeder, T., Schneider, F.B.: Proactive obfuscation. ACM Transactions on Computing Systems 28(2) (2010)
Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys 22(4), 299–319 (1990)
Xu, J., Kalbarczyk, Z., Iyer, R.K.: Transparent runtime randomization for security. In: Proc. 22nd International Symposium on Reliable Distributed Systems, pp. 260–269. IEEE Computer Science Press, Los Alamitos (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schneider, F.B. (2011). Beyond Traces and Independence. In: Jones, C.B., Lloyd, J.L. (eds) Dependable and Historic Computing. Lecture Notes in Computer Science, vol 6875. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24541-1_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-24541-1_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24540-4
Online ISBN: 978-3-642-24541-1
eBook Packages: Computer ScienceComputer Science (R0)