Experiences using lightweight formal methods for requirements modeling

被引:66
作者
Easterbrook, S
Lutz, R
Covington, R
Kelly, J
Ampo, Y
Hamilton, D
机构
[1] NASA, IV&V Facil, Fairmont, WV 26554 USA
[2] NASA, Jet Prop Lab, Pasadena, CA 91109 USA
[3] NEC Corp Ltd, Tokyo, Japan
[4] Hewlett Packard Corp, San Diego, CA 92127 USA
基金
美国国家航空航天局;
关键词
software requirements; formal methods; verification and validation; fault protection software; NASA;
D O I
10.1109/32.663994
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies differ from previously reported applications of formal methods in that formal methods were applied very early in the requirements engineering process, to validate the evolving requirements. The results were fed back into the projects, to improve the informal specifications. For each case study, we describe what methods were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, formal methods enhanced the existing verification and validation processes, by testing key properties of the evolving requirements, and helping to identify weaknesses. We conclude that the benefits gained from early modeling of unstable requirements more than outweigh the effort needed to maintain multiple representations.
引用
收藏
页码:4 / 14
页数:11
相关论文
共 27 条
[1]  
AMPO Y, 1995, P FDN SOFTW ENG 95
[2]  
[Anonymous], 1996, ARIANE 5 FLIGHT 501
[3]  
Boehm B. W., 1981, SOFTWARE ENG EC
[4]  
BUTLER RW, 1995, P 10 ANN C COMP ASS
[5]   FORMAL METHODS REALITY CHECK - INDUSTRIAL USAGE [J].
CRAIGEN, D ;
GERHART, S ;
RALSTON, T .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1995, 21 (02) :90-98
[6]  
CROW J, 1996, WORKSH FORM METH SOF
[7]  
CROW J, 1995, SRICSL9517 SRI INT
[8]  
DIVITO BL, 1996, P FORMAL METHODS EUR
[9]  
EASTERBROOK S, 1996, P IEEE 5 WORKSH EN T
[10]  
EASTERBROOK S, 1997, P 3 IEEE S REQ ENG R