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 条

[1] Verification of Contract-based Communicating Systems
Salauen, Gwen
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (138):
[2] Contract-Based Verification of Hierarchical Systems of Components
Quinton, Sophie
Graf, Susanne
SEFM 2008: SIXTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2008, : 377 - 381
[3] Contract-Based Verification of Simulink Models
Bostrom, Pontus
FORMAL METHODS AND SOFTWARE ENGINEERING, 2011, 6991 : 291 - 306
[4] Towards contract-based verification for autonomous vessels
Torben, Tobias Rye
Smogeli, Oyvind
Glomsrud, Jon Arne
Utne, Ingrid B.
Sorensen, Asgeir J.
OCEAN ENGINEERING, 2023, 270
[5] Application of Contract-based verification techniques for Hybrid Automata to Surgical Robotic Systems
Schreiter, Luzie
Bresolin, Davide
Capiluppi, Marta
Raczkowsky, Joerg
Fiorini, Paolo
Woern, Heinz
2014 EUROPEAN CONTROL CONFERENCE (ECC), 2014, : 2310 - 2315
[6] Proof-Carrying Apps: Contract-Based Deployment-Time Verification
Holthusen, Soenke
Nieke, Michael
Thuem, Thomas
Schaefer, Ina
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I, 2016, 9952 : 839 - 855
[7] Towards Smart Contract-Based Verification of Anonymous Credentials
Muth, Robert
Galal, Tarek
Heiss, Jonathan
Tschorsch, Florian
FINANCIAL CRYPTOGRAPHY AND DATA SECURITY. FC 2022 INTERNATIONAL WORKSHOPS, 2023, 13412 : 481 - 498
[8] VCC: Contract-based Modular Verification of Concurrent C
Dahlweid, Markus
Moskal, Michal
Santen, Thomas
Tobies, Stephan
Schulte, Wolfram
2009 31ST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, COMPANION VOLUME, 2009, : 429 - +
[9] Towards Design and Verification of Evolving Cyber Physical Systems Using Contract-Based Methodology
Guissouma, Houssem
Leiner, Simon
Sax, Eric
2019 5TH IEEE INTERNATIONAL SYMPOSIUM ON SYSTEMS ENGINEERING (IEEE ISSE 2019), 2019,
[10] Contract-based verification of discrete-time multi-rate Simulink models
Pontus Boström
Jonatan Wiik
Software & Systems Modeling, 2016, 15 : 1141 - 1161

← 1 2 3 4 5 →