R. S. Fabry
Abstract
Dynamic verification of a decision implies that every time the decision is made there is a consistency check performed on the decision using independent hardware and software. The dynamic verification of operating system decisions is used on the PRIME system being designed and constructed at the University of California, Berkeley. PRIME is an experimental time-sharing system which is to have the properties of continuous availability, data privacy, and cost effectiveness. The technique of dynamic verification allows the construction of an operating system which does not make certain decisions improperly even in the presence of a single hardware or software fault. Furthermore, multiple faults lead to unreliable operation only if the faults happen to reinforce each other. On PRIME, dynamic verification is used to ensure that one user's information cannot become available to another user gratuitously even in the presence of a single hardware or software fault. The amount of additional hardware and software required for dynamic verification can be modest.
- 1 Baskin, H. B., Borgerson, B. R., and Roberts, R. PRIME- a modular architecture for terminal-oriented systems. Proc. AFIPS 1972 SJCC, AFIPS Press, Montvale, N.J., pp. 431-437.Google Scholar
- 2 Borgerson, B. R. A fail-softly system for time-sharing use. Digest of the 1972 lnternat. Symp. on Fault Tolerant Computing, June 1972, pp. 89-93.Google Scholar
- 3 Quatse, J. T., Gaulene, P., and Dodge, D. The external access network of a modular computer system. Proc. AFIPS 1972 SJCC, AFIPS Press, Montvale, N.J., pp. 783-790.Google Scholar
- 4 Borgerson, B. R. Spontaneous reconfiguration in a faiLsoftly computer utility. Proc. Datafair 73, British Computer Society, London, pp. 326-333.Google Scholar
- 5 Lampson, B. W. Protection. Proc. 5th Princeton Conf. on lnformat. Sciences and Systems, 1971, pp. 437-443.Google Scholar
- 6 Amdahl, G. M. The structure of SYSTEM/360, Part 3- Processing unit design considerations. IBM Systems J. 3, 2 & 3 (196Zl), 144-164.Google Scholar
- 7 Weissman, C. Security controls in the ADEPT-50 timesharing system. Proc. AFIPS 1969 FJCC, AFIPS Press, Montvale, N.J., pp. 119-133.Google Scholar
- 8 Carter, W. C., and Bouricius, W.G. A survey of fault tolerant computer architecture and its evaluation. Computer (Jan. 1971), 10-15.Google Scholar
- 9 Dijkstra, E. W. The structure of THE multiprogramming system. Comm. ACM 11, 5 (May 1968), 341-346. Google ScholarDigital Library
- 10 Elspas, B., et al. An assessment of techniques for proving program correctness. Computing Surveys 4, 2 (June 1972), 97-147. Google ScholarDigital Library
Recommendations
An empirical exploratory study on operating system reliability
SAC '14: Proceedings of the 29th Annual ACM Symposium on Applied ComputingHigh-reliability applications run on top of commodity operating systems, which hence must provide high reliable services. In this paper, we conduct an empirical exploratory study on OS reliability. We analyze more than 30,000 real OS failure data ...
Survey of the Formal Verification of Operating Systems in Power Monitoring System
PRIS '23: Proceedings of the 2023 5th International Conference on Pattern Recognition and Intelligent SystemsThe formal verification of the operating systems in power monitoring system is an important means to ensure the security of the operating system in power monitoring system. This paper introduces the verification principles and framework of formal ...
Model Checking Dynamic Memory Allocation in Operating Systems
Most system software, including operating systems, contains dynamic data structures whose shape and contents should satisfy design requirements during execution. Model checking technology, a powerful tool for automatic verification based on state ...
Comments