Computer Science Colloquia
Thursday, May 1, 2014
Advisor: Kevin Sullivan
Attending Faculty: David Evans
1:30 PM, Rice Hall, Rm. 242
Master's Project Presentation
Synthesizing REST Web Services to Advance a Useful Science of Non-Functional System Properties and Tradeoffs
Today, software and systems engineers operate without the ability to effectively characterize, specify, reason about, verify, and make trade-offs among many important non-functional system properties (often called ilities). Definitions of ilities such as evolvability and security are far too vague and informal to be useful in high-consequence software and systems engineering projects. Common terms are often used in inconsistent ways, and different terms are often used to refer to the same underlying concepts. In some cases, the underlying concepts themselves remain very poorly defined and understood. As a consequence, many large projects go awry.
Our research is intended to advance a science of ilities and trade-offs. Our approach is to develop, validate, and promulgate formal definitions and models of important ilities. However, formal models can be hard for practitioners to understand and use, cutting off a key source of feedback needed to validate and evolve such models.
To address this problem, I present an approach to make such models easier for practitioners to understand and use by exposing their essential data and functional abstractions as REST web services. My main technical contribution is an approach to implementing such web services largely through synthesis of executable code from formal ility models expressed in the constructive logic of the Coq proof assistant. I present a case study and demonstration prototype involving our formalization and extension of an informal theory of change-related ilities by our colleagues, Ross, et al.: researchers in MIT's Engineering Systems Department.