|
Research
| | My research interests are
in the areas of Software Engineering, Human-Computer Interfaces, and
software support for Medical Safety. Specifically, my thesis is in
Requirements Engineering and is focused on a new approach to help make
formal property specifications more accessible. I am currently doing
case studies to evaluate this new approach: these case studies involve
requirements for various medical processes (e.g., blood transfusion,
chemotherapy).
The Problem
Property specifications are often used in requirements engineering to
precisely describe important behavioral properties of a system. These
specifications can then be used as the basis for automated analyses,
such as formal verification, that check that the behavior of a system
is consistent with its specified properties. Ideally, property
specifications should be precise enough to support automated analyses
and accessible enough to be readily understood by system developers.
Automated analyzers typically accept property specifications
represented in mathematical formalisms, such as temporal logic or
finite-state automata, but such formalisms are often difficult for
system developers to understand. In practice, developers instead tend
to write properties in a natural language, such as English. While
natural language may offer accessibility, properties written with such
informality are often ambiguous. To be used effectively in requirements
engineering, property specifications need to be represented in a way
that is both accessible and mathematically precise.
Our Approach
The new property specification approach that we have developed aims to guide users
through the process of creating property specifications that have both
qualities. To provide this guidance, the approach focuses on helping
users to elucidate subtle, but important, property details that need to
be considered but are often overlooked. These property details are
represented using templates that explicitly indicate possible
variations. The approach provides three alternative representations of
these templates, each of which offer user guidance for how to make
decisions about the same property details. The three representations
are:
- graphical finite-state automata, which offer precision;
- "disciplined" English sentences, which offer accessibility; and
- an
interactive question tree format, which offers accessibility and
additional user guidance.
To provide support for evaluation of this
approach, a prototype tool, called PROPEL, for "PROPerty ELucidation",
is under development. This tool allows users to work with one or
more of these representations as they develop their properties. This
property specification approach is being evaluated by using PROPEL to
specify properties in several small, but realistic, case studies.
|
Publications
Elizabeth A. Henneman, George S. Avrunin, Lori A. Clarke, Leon
J. Osterweil, Chester Andrzejewski, Jr., Karen Merrigan, Rachel
L. Cobleigh, Kim Frederick, Ethan Katz-Bassett, and Philip
L. Henneman. Increasing patient safety and efficiency in transfusion
therapy using formal process definitions. Transfusion Medicine
Reviews, 21(1):49-57. January 2007. Accepted for publication May
2006.
Download this paper: PDF
Download this paper:
HTML
Rachel L. Cobleigh, George S. Avrunin, Lori A. Clarke, User
guidance for creating precise and accessible property
specifications, Proceedings of the Fourteenth ACM SIGSOFT
Symposium on the Foundations of Software Engineering (FSE 2006),
Portland, OR, pp. 208-218, November 2006.
Download this paper: PDF
Lori A. Clarke, Yao Chen, George S. Avrunin, Bin Chen, Rachel
L. Cobleigh, Kim Frederick, Elizabeth A. Henneman, and Leon J.
Osterweil, Process Programming to Support Medical Safety: A Case
Study on Blood Transfusion, Proceedings of the Software Process
Workshop, Beijing, China, May 2005.
Download this paper: PDF
Rachel L. Smith*, George S. Avrunin, Lori A. Clarke, From Natural
Language Requirements to Rigorous Property Specifications,
Proceedings of the Monterey Workshop 2003 (Workshop on Software
Engineering for Embedded Systems (SEES 2003) From Requirements to
Implementation), Chicago, IL, pp. 40-46, September 2003.
Download this paper:
PDF
Rachel L. Smith*, George S. Avrunin, Lori A. Clarke, Leon
J. Osterweil, PROPEL: An Approach Supporting Property
Elucidation, Proceedings of the 24th International Conference on
Software Engineering (ICSE 2002), Orlando, FL, pp. 11-21, May 2002.
Download this paper:
PDF
* Maiden name.
Other Interests
|
