Mathematical modeling and analysis of an external memory manager

  • William D. Young
  • William R. Bevier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


We have modeled and formally analyzed a simple external memory manager (EMM) system loosely based on the memory management strategies of Mach. The modeling was carried out via a series of refinements from a very abstract model to a simple concrete model. Each successive model is an implementation of the next more abstract level. We have stated theorems that describe formally the relationships among these models; these theorems have been proven for a subset of the functionality of the system. The result is a “stack” of progressively more realistic and complex systems (partially) proven to satisfy an implements relation with a simple high-level design.


Abstract Model Address Space Label State Concrete Syntax Memory Object 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    W.R. Bevier, W.A. Hunt, Jr., J S. Moore, and W.D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411–428, December 1989.Google Scholar
  2. 2.
    J. Boykin, D. Kirschen, A. Langerman, and S. LoVerso. Programming under Mach. Addison Wesley Unix and Open Series System, Reading, Mass., 1993.Google Scholar
  3. 3.
    B. Brock, M. Kaufmann and J Strother Moore. ACL2 theorems about commercial microprocessors, in M. Srivas and A. Camilleri, eds., Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, pp. 275–293, 1996.Google Scholar
  4. 4.
    R.S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988.Google Scholar
  5. 5.
    J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control, in D. Dill, ed., Computer Aided Verification, Lecture Notes in Computer Science 818, Springer Verlag, 1994, page 68–80.Google Scholar
  6. 6.
    M. Kaufmann and J Moore. An industrial strength theorem prover for a logic based on Common Lisp, to appear in IEEE Transactions on Software Engineering, 1997. This is a revised version of “ACL2: An industrial strength version of Nqthm,” which appeared in Proceedings of the Eleventh Annual Conference on Computer Assurance, IEEE Computer Society Press, June, 1996, pp 23–34.Google Scholar
  7. 7.
    W.D. Young and W.R. Bevier. Mathematical modeling and analysis of an external memory manager. CLI Technical Report 105, Computational Logic, Inc., September, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • William D. Young
    • 1
  • William R. Bevier
    • 1
  1. 1.Computational Logic, Inc.AustinUSA

Personalised recommendations