Mathematical modeling and analysis of an external memory manager
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.
KeywordsAbstract Model Address Space Label State Concrete Syntax Memory Object
Unable to display preview. Download preview PDF.
- 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.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.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.R.S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988.Google Scholar
- 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.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.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