Heather M. Conboy, George S. Avrunin, and Lori A. Clarke. Modal abstraction view of requirements for medical devices used in healthcare processes. In SEHC '13: Proceedings of the 2013 ICSE Workshop on Software Engineering in Health Care, pages 24–27, San Francisco, May 2013. [ .pdf ]
Medical device requirements often depend on the healthcare processes in which the device is to be used. Since such processes may be complex, critical requirements may be specified inaccurately, or even missed altogether. We are investigating an automated requirement derivation approach that takes as input a model of the healthcare process along with a model of the device and tries to derive the requirements for that device. Our initial experience with this approach has shown that when the process and device involve complex behaviors, the derived requirements are also often complex and difficult to understand. In this paper, we describe an approach for creating a modal abstraction view of the derived requirements that decomposes each requirement based on it.
Heather M. Conboy, George S. Avrunin, and Lori A. Clarke. Process-based derivation of requirements for medical devices. In 1st ACM International Health Informatics Symposium, pages 656–665, Arlington, VA, November 2010. [ DOI | .pdf ]
One goal of medical device certification is to show that a given medical device satisfies its requirements. But the requirements that should be met by such a device depend on the clinical processes in which the device is to be used, and such processes are increasingly large and complex. Critical requirements may thus be specified inaccurately or incompletely, or even missed altogether, and the use of the devices may lead to harm. Thus, we investigated a process-based requirement derivation approach that inputs a model that captures a particular medical process and a requirement that should be satisfied by that process, and outputs a derived requirement of the medical device that is sufficient to prevent any violations of the process requirement. Our approach combines an approach for generating assumptions for assume-guarantee reasoning with one for interface synthesis to automate the derivation of the medical device requirements. The proposed approach iteratively performs the requirement derivation by employing a model checker and a learning algorithm. We implemented this approach and evaluated our approach by applying it to two small case studies. Our experiences showed that the proposed approach could be successfully applied to abstract models of portions of real medical processes and that the derived requirements of the medical devices appeared useful and understandable.
Huong Phan, George S. Avrunin, and Lori A. Clarke. Considering the exceptional: Incorporating exceptions into property specifications. Technical Report UM-CS-2008-32, Department of Computer Science, University of Massachusetts, September 2008. [ .pdf ]
Property specifications concisely describe aspects of what a system is supposed to do. It is important that these specifications be correct, describing all the desired behavior and ruling out undesired behavior. Our experience shows that properties are sometimes specified incorrectly because specifiers fail to take into account some exceptional behaviors of the system. In previous work we presented Propel, a tool that guides specifiers through the process of creating understandable yet precise property specifications. Here we describe extensions to Propel that allow specifiers of a property to indicate what exceptions should be considered and what impact those exceptions should have on the acceptability of system behavior. Although the description is given in terms of the framework provided by Propel, the issues specifiers must consider would apply to other specification formalisms.
Rachel L. Cobleigh, George S. Avrunin, and Lori A. Clarke. User guidance for creating precise and accessible property specifications. In Proceedings of the 14th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 208–218, Portland, OR, November 2006. [ DOI | .pdf ]
Property specifications concisely describe what a system is supposed to do. No matter what notation is used to describe them, however, it is difficult to represent these properties correctly, since there are often subtle, but important, details that need to be considered. Propel aims to guide users through the process of creating properties that are both accessible and mathematically precise, by providing templates for commonly-occurring property patterns. These templates explicitly represent these subtle details as options. In this paper, we present a new representation of these templates, a Question Tree notation that asks users a hierarchical sequence of questions about their intended properties. The Question Tree notation is particularly useful for helping to select the appropriate template, but it also complements the finite-state automaton and disciplined natural language representations provided by Propel. We also report on some case studies that are using Propel and on an experimental evaluation of the understandability of the disciplined natural language representation
Richard M. Chang, George S. Avrunin, and Lori A. Clarke. Property inference from program executions. Technical report, Department of Computer Science, University of Massachusetts, 2006. [ .pdf ]
Software verification techniques require properties that define the intended behavior of a system be specified. Generating such properties is often very difficult and serves as an impediment to the adoption of verification techniques. Techniques that leverage program executions to infer these properties are a promising avenue for automatically generating these properties. In this paper, we propose a property inference approach that leverages event traces derived from program executions to efficiently infer properties that are subtle variations of commonly occurring properties. We define inference templates that represent sets of these properties and describe our inference algorithm that refines these templates based on event traces.
Rachel L. Smith, George S. Avrunin, and Lori A. Clarke. From natural language requirements to rigorous property specifications. In Workshop on Software Engineering for Embedded Systems (SEES 2003): From Requirements to Implementation, pages 40–46, Chicago, IL, September 2003. [ .pdf ]
Property specifications concisely describe selected aspects of what a software system is supposed to do. It is surprisingly difficult to write these properties correctly. Although there are rigorous mathematical formalisms for representing properties, these are often difficult to use. No matter what notation is used, however, there are often subtle, but important, details that need to be considered. The Propel tool aims to make the job of writing and understanding properties easier by providing templates that explicitly capture these details as options for commonly-occurring property patterns. These templates are represented using “disciplined” natural language, decision trees, and finite-state automata, allowing the developer to easily move between these representations.
Rachel L. Smith, George S. Avrunin, Lori A. Clarke, and Leon J. Osterweil. Propel: An approach supporting property elucidation. In Proceedings of the Twenty-Fourth International Conference on Software Engineering, pages 11–21, Orlando, FL, May 2002. [ DOI | .pdf ]
Property specifications concisely describe what a software system is supposed to do. It is surprisingly difficult to write these properties correctly. There are rigorous mathematical formalisms for representing properties, but these are often difficult to use. No matter what notation is used, however, there are often subtle, but important, details that need to be considered. Propel aims to make the job of writing and understanding properties easier by providing templates that explicitly capture these details as options for commonly-occurring property patterns. These templates are represented using both "disciplined" natural language and finite-state automata, allowing the specifier to easily move between these two representations.
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the Twenty-First International Conference on Software Engineering, pages 411–420, Los Angeles, May 1999. [ DOI | .pdf ]
Model checkers and other finite-state verification tools allow developers to detect certain kinds of errors automatically. Nevertheless, the transition of this technology from research to practice has been slow. While there are a number of potential causes for reluctance to adopt such formal methods, we believe that a primary cause is that practitioners are unfamiliar with specification processes, notations, and strategies. In a recent paper, we proposed a pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification. Since then, we have carried out a survey of available specifications, collecting over 500 examples of property specifications. We found that most are instances of our proposed patterns. Furthermore, we have updated our pattern system to accommodate new patterns and variations of existing patterns encountered in this survey. This paper reports the results of the survey and the current status of our pattern system.
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Mark Ardis, editor, Proceedings of FMSP '98, the Second Workshop on Formal Methods in Software Practice, pages 7–15, Clearwater Beach, FL, March 1998. [ DOI | .pdf ]
Finite-state verification (e.g., model checking) provides a powerful means to detect errors that are often subtle and difficult to reproduce. Nevertheless, the transition of this technology from research to practice has been slow. While there are a number of potential causes for reluctance in adopting such formal methods in practice, we believe that a primary cause rests with the fact that practitioners are unfamiliar with specification processes, notations, and strategies. Recent years have seen growing success in leveraging experience with design and coding patterns. We propose a pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification.
This file was generated by bibtex2html 1.99.
![[Back]](/icons/back.gif){kind=icon}
Back to George Avrunin's home page