Requirements Analysis of a Quad-Redundant Flight Control System

被引：22

作者：

Backes, John ^{[1
]}

Cofer, Darren ^{[1
]}

Miller, Steven ^{[1
]}

Whalen, Michael W. ^{[2
]}

机构：

[1] Rockwell Collins, Bloomington, MN 55438 USA

[2] Univ Minnesota, Minneapolis, MN 55455 USA

来源：

NASA FORMAL METHODS (NFM 2015) | 2015年 / 9058卷

关键词：

D O I：

10.1007/978-3-319-17524-9_7

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In this paper we detail our effort to formalize and prove requirements for the Quad-redundant Flight Control System (QFCS) within NASA's Transport Class Model (TCM). We use a compositional approach with assume-guarantee contracts that correspond to the requirements for software components embedded in an AADL system architecture model. This approach is designed to exploit the verification effort and artifacts that are already part of typical software verification processes in the avionics domain. Our approach is supported by an AADL annex that allows specification of contracts along with a tool, called AGREE, for performing compositional verification. The goal of this paper is to show the benefits of a compositional verification approach applied to a realistic avionics system and to demonstrate the effectiveness of the AGREE tool in performing this analysis.

引用

页码：82 / 96

页数：15

共 14 条

[1] [Anonymous], 2006, YICES SMT SOLVER
[2] [Anonymous], 2013, JKIND JAVA IMPLEMENT
[3] Brat G., 2015, VERIFYING SAFTETY FL
[4] Caspi P., 2001, INT C COMP SAF REL S
[5] Cofer Darren, 2012, NASA Formal Methods. Proceedings of the 4th International Symposium, NFM 2012, P126, DOI 10.1007/978-3-642-28891-3_13
[6] Cooper GE., 1969, USE PILOT RATING EVA
[7] Crum V., 2004, P AER C 2004 IEEE
[8] Feiler PH., 2012, Model-based engineering with AADL: an introduction to the SAE architecture analysis & design language
[9] Gacek A., 2015, NASA FORM METH S
[10] Gacek A., 2014, AGREE USERS GUIDE

← 1 2 →