Formalization of storage considerations in software design
Lakshminarasimha Reddy Ankireddipally · 1999
One of the technical impediments for the widespread adoption of the formal methods is an inability to address storage-related concerns such as "out of memory" errors. The focus of this dissertation is on formal specification and modular reasoning of storage-related aspects of practical components and systems. In particular, this thesis tries to address the following fundamental storage-related questions for practical component-based software development (1) Is it possible to reason statically and in a modular fashion that the system would not run "out of memory"? (2) Is it possible for the reasoning system to be modular, yet sufficiently precise with respect to storage constraints? (3) Is it possible to have a formally specified storage management mechanism that is predictable and efficient, yet allows effective storage utilization?;The main contribution of this research work is a formal and modular framework for storage specification and reasoning. A memory management mechanism that is predictable and efficient is also a part of this dissertation.