People/Web Search Calendar Emergency Info A-Z Index UVA Email University of Virginia

Computer Science Colloquia

Tuesday, September 8, 2015
Jian Xiang
Adviser: John Knight
Attending Faculty: Jack Davidson (Chair), Kevin Sullivan, Hongning Wang, and Houston Wood

10:00 AM in Rice 404

Ph.D. Proposal Presentation
Real-World Types and Their Applications

Software systems, especially cyber-physical systems and embedded systems, interact with the real world in order to sense and affect it. For these systems to function correctly, such software should obey rules inherited from the real world that it senses, models, and affects, as well as from the machine world in which the software executes. Frequently, however, important characteristics of real-world entities are often undocumented, or are documented incompletely, informally, and implicitly in source code. As a result, real-world attributes, such as units and dimensions, and associated real-world constraints, such as not mixing units, are stated and enforced either in ad-hoc ways or not at all. In addition, crucial relationships between machine-world representations and real-world entities, such as accuracy of sensed values, remain under-specified. The result is that programs tend to treat machine-world representations as if they were the real-world entities themselves. This practice leads to the introduction of faults into systems due to unrecognized discrepancies, and executions end up violating rules inherited from the real world. The results are software and system failures and adverse downstream consequences.

This thesis proposes the notion of real-world types to document relevant characteristics of real-world entities for use in programs and to document relationships between real-world types and machine-level representations. By using real-world types, programmers are able to enforce real-world constraints on programs in a systematic way, thereby enabling a new class of software fault detection. This research will examine the principles and practices necessary to (1) comprehensively document real-world entities and (2) leverage such documentations to systematically enforce real-world constraints. This proposal provides an overview of real-world types along with key research questions, a research plan to answer these research questions, and preliminary results.