add to favorites : reference url back to results : previous : next
 

FORMALIZATION OF INPUT AND OUTPUT IN MODERN OPERATING SYSTEMS: THE HADLEY MODEL
Access this item.
TitleFORMALIZATION OF INPUT AND OUTPUT IN MODERN OPERATING SYSTEMS: THE HADLEY MODEL
AuthorGerber, Matthew
Keywordshadley system
operating systems
software verification
software reliability
device drivers
digital investigation
AbstractWe 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.
AdviserLeeson, John
PublisherUniversity of Central Florida
DegreePh.D.
Degree DisciplineSchool of Computer Science
Degree GrantorEngineering and Computer Science
Degree ProgramComputer Science
Graduation Date2005-05-01
TypeDoctoral dissertation
Access LevelPublic - Allow Worldwide Access
Release Date2005-05-01
RepositoryUniversity Archives
Repository CollectionElectronic Theses and Dissertations
IdentifierCFE0000392
Access Linkhttp://purl.fcla.edu/fcla/etd/CFE0000392

add to favorites : reference url back to results : previous : next
powered by CONTENTdm ® | contact us  ^ to top ^