Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems

被引：2

作者：

Bhatt, Devesh ^{[1
]}

Chattopadhyay, Arunabh ^{[1
]}

Li, Wenchao ^{[2
]}

Oglesby, David ^{[1
]}

Owre, Sam ^{[2
]}

Shankar, Natarajan ^{[2
]}

机构：

[1] Honeywell Aerosp Labs, Golden Valley, MN 55422 USA

[2] SRI Int, Silicon Valley, CA USA

来源：

NASA FORMAL METHODS, NFM 2016 | 2016年 / 9690卷

关键词：

D O I：

10.1007/978-3-319-40648-0_3

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Avionic systems involve complex time-dependent behaviors across interacting components. This paper presents a contract-based approach for formally verifying these behaviors in a compositional manner. A unique feature of our contract-based tool is the support of architectural specification for multi-rate platforms. An abstraction technique has also been developed for properties related to variable time bounds. Preliminary results on applying this approach to the verification of an aircraft cabin pressure control system are promising.

引用

页码：34 / 40

页数：7

共 7 条

[1] [Anonymous], 1992, TEMPORAL LOGIC REACT, DOI DOI 10.1007/978-1-4612-0931-7
[2] Requirements Analysis of a Quad-Redundant Flight Control System
Backes, John
Cofer, Darren
Miller, Steven
Whalen, Michael W.
[J]. NASA FORMAL METHODS (NFM 2015), 2015, 9058 : 82 - 96
[3] Barnat J, 2012, LECT NOTES COMPUT SC, V7437, P78, DOI 10.1007/978-3-642-32469-7_6
[4] Formal Design and Safety Analysis of AIR6110 Wheel Brake System
Bozzano, M.
Cimatti, A.
Pires, A. Fernandes
Jones, D.
Kimberly, G.
Petri, T.
Robinson, R.
Tonetta, S.
[J]. COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 : 518 - 535
[5] Verifying the Safety of a Flight-Critical System
Brat, Guillaume
Bushnell, David
Davies, Misty
Giannakopoulou, Dimitra
Howar, Falk
Kahsai, Temesghen
[J]. FM 2015: FORMAL METHODS, 2015, 9109 : 308 - 324
[6] Dwyer M. B., 1999, Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), P411, DOI 10.1109/ICSE.1999.841031
[7] Li W., 2015, ACM IEEE INT C FORM

← 1 →