You are here

UCF Digital Collections ยป ETD Collection

FORMALIZATION OF INPUT AND OUTPUT IN MODERN OPERATING SYSTEMS: THE HADLEY MODEL

Download pdf | Full Screen View

Date Issued:
2005
Abstract/Description:
We present the Hadley model, a formal descriptive model of input and output for modern computer operating systems. Our model is intentionally inspired by the Open Systems Interconnection model of networking; I/O as a process is defined as a set of translations between a set of computer-sensible forms, or layers, of information. To illustrate an initial application domain, we discuss the utility of the Hadley model and a potential associated I/O system as a tool for digital forensic investigators. To illustrate practical uses of the Hadley model we present the Hadley Specification Language, an essentially functional language designed to allow the translations that comprise I/O to be written in a concise format allowing for relatively easy verifiability. To further illustrate the utility of the language we present a read/write Microsoft DOS FAT12 and read-only Linux ext2 file system specification written in the new format. We prove the correctness of the read-only side of these descriptions. We present test results from operation of our HSL-driven system both in user mode on stored disk images and as part of a Linux kernel module allowing file systems to be read. We conclude by discussing future directions for the research.
Title: FORMALIZATION OF INPUT AND OUTPUT IN MODERN OPERATING SYSTEMS: THE HADLEY MODEL.
52 views
20 downloads
Name(s): Gerber, Matthew, Author
Leeson, John, Committee Chair
University of Central Florida, Degree Grantor
Type of Resource: text
Date Issued: 2005
Publisher: University of Central Florida
Language(s): English
Abstract/Description: We present the Hadley model, a formal descriptive model of input and output for modern computer operating systems. Our model is intentionally inspired by the Open Systems Interconnection model of networking; I/O as a process is defined as a set of translations between a set of computer-sensible forms, or layers, of information. To illustrate an initial application domain, we discuss the utility of the Hadley model and a potential associated I/O system as a tool for digital forensic investigators. To illustrate practical uses of the Hadley model we present the Hadley Specification Language, an essentially functional language designed to allow the translations that comprise I/O to be written in a concise format allowing for relatively easy verifiability. To further illustrate the utility of the language we present a read/write Microsoft DOS FAT12 and read-only Linux ext2 file system specification written in the new format. We prove the correctness of the read-only side of these descriptions. We present test results from operation of our HSL-driven system both in user mode on stored disk images and as part of a Linux kernel module allowing file systems to be read. We conclude by discussing future directions for the research.
Identifier: CFE0000392 (IID), ucf:46339 (fedora)
Note(s): 2005-05-01
Ph.D.
Engineering and Computer Science, School of Computer Science
Doctorate
This record was generated from author submitted information.
Subject(s): hadley system
operating systems
software verification
software reliability
device drivers
digital investigation
Persistent Link to This Record: http://purl.flvc.org/ucf/fd/CFE0000392
Restrictions on Access: public
Host Institution: UCF

In Collections