Formal specification of software using abstract state machines.

Abstract

As software systems grow in size and sophistication, it becomes harder for humans to understand them and anticipate their behavior. Formal specification techniques aim to foster understanding and increase reliability by providing a mathematical foundation to software documentation. But by and large, applications of these techniques to real-world software problems have been small in number and scope. In this thesis, we explore several real-world software domains through formal specification, using Abstract State Machines (ASMs). ASMs require minimal mathematical overhead and are flexible enough to provide descriptions at various levels of abstraction. In each domain, we construct specifications at appropriate levels of abstraction. Each specification serves as a precise yet fully abstract standard, an executable tool for learning and design, and a basis for verification. Moreover, the rigor imposed by the specification process brings to light interesting issues. Each software domain that we examine presents unique challenges, in terms of specification, refinement or verification. First, we take a formal approach to the notoriously complicated area of database recovery. Starting with a high-level view of the recovery problem, we add implementation details in a clear, methodical way through a series of refinements. Second, we present a specification of the Java programming language that covers the broad spectrum of the language's features in a modular fashion. We use a semi-graphical format that unifies the static and dynamic semantics of the language. Third, we investigate the Java concurrency model in depth from a formal perspective. The abstract operational view afforded by our ASM models highlights subtleties of the model. Finally, we formally specify the Windows Card Runtime Environment, currently being developed at Microsoft. This specification is used to verify certain critical safety properties.