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

共 50 条

[21] Contract-based verification of MATLAB-style matrix programs
Wiik, Jonatan
Bostrom, Pontus
FORMAL ASPECTS OF COMPUTING, 2016, 28 (01) : 79 - 107
[22] A contract-based component model for embedded systems
Li, SY
Wu, J
Hu, ZG
QSIC 2004: PROCEEDINGS OF THE FOURTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, 2004, : 232 - 239
[23] A Formal Contract-based Model for Component-based Real-time Systems
Trinh-Dong Nguyen
Dang Van Hung
Anh-Hoang Truong
2017 4TH NAFOSTED CONFERENCE ON INFORMATION AND COMPUTER SCIENCE (NICS), 2017, : 230 - 235
[24] MODELING AND VERIFICATION OF TIME-DEPENDENT SYSTEMS USING TIME PETRI NETS
BERTHOMIEU, B
DIAZ, M
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1991, 17 (03) : 259 - 273
[25] Contract-based modeling and verification of timed safety requirements within SysML
Iulia Dragomir
Iulian Ober
Christian Percebois
Software & Systems Modeling, 2017, 16 : 587 - 624
[26] Contract-based modeling and verification of timed safety requirements within SysML
Dragomir, Iulia
Ober, Iulian
Percebois, Christian
SOFTWARE AND SYSTEMS MODELING, 2017, 16 (02): : 587 - 624
[27] Contract-Based Resource Verification for Higher-Order Functions with Memoization
Madhavan, Ravichandhran
Kulal, Sumith
Kuncak, Viktor
ACM SIGPLAN NOTICES, 2017, 52 (01) : 330 - 343
[28] Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code
Wiik, Jonatan
Bostrom, Pontus
FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2014, 2014, 8829 : 396 - 412
[29] Contract-Based Incentive Mechanism for Cooperative NOMA Systems
Tang, Rui
Cheng, Julian
Cao, Zhaoxin
IEEE COMMUNICATIONS LETTERS, 2019, 23 (01) : 172 - 175
[30] Contract-based formal specification of safety critical systems
Dong, W
Wang, J
Proceedings of the 29th Annual International Computer Software and Applications Conference, Workshops and Fast Abstracts, 2005, : 7 - 8

← 1 2 3 4 5 →