One-Click Formal Methods

被引：18

作者：

Backes, John ^{[1
]}

Bolignano, Pauline ^{[2
]}

Cook, Byron ^{[3
,4
]}

Gacek, Andrew ^{[5
]}

Luckow, Kasper Soe ^{[5
]}

Rungta, Neha ^{[6
]}

Schaef, Martin ^{[7
]}

Schlesinger, Cole ^{[2
]}

Tanash, Rima ^{[8
]}

Varming, Carsten ^{[5
]}

Whalen, Michael ^{[9
]}

机构：

[1] Amazon Web Serv, Amazon Inspector Serv Team, New York, NY 10013 USA

[2] Amazon Web Serv, New York, NY USA

[3] UCL, Comp Sci, London, England

[4] Amazon, Automated Reasoning, New York, NY USA

[5] Amazon Web Serv, Automated Reasoning Grp, New York, NY USA

[6] Amazon Web Serv, Formal Serv Team, New York, NY USA

[7] Amazon Web Serv Secur, New York, NY USA

[8] Amazon Secur Hub Serv Team, New York, NY USA

[9] Amazon Web Serv, Proof Platforms Team, New York, NY USA

来源：

IEEE SOFTWARE | 2019年 / 36卷 / 06期

关键词：

Helicopter control - Industrial automation - Microprocessor designs - Research and development - Security properties;

D O I：

10.1109/MS.2019.2930609

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Formal methods are mathematically based approaches for specifying, building, and reasoning about software. Despite 50 years of research and development, formal methods have had only limited impact in industry. While we have seen success in such domains as microprocessor design and aerospace (e.g., proofs of security properties for helicopter control systems1), we have not seen wide adoption of formal methods for large and complex systems, such as web services, industrial automation, or enterprise support software. © 1984-2012 IEEE.

引用

页码：61 / 65

页数：5

共 4 条

[1]

[Anonymous], 2019, P CAV, DOI DOI 10.1007/978-3-030-25543-5_14

[2]

Backes J, 2018, PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), P206

[3] A Formal Approach to Constructing Secure Air Vehicle Software [J].

Cofer, Darren ;

Gacek, Andrew ;

Backes, John ;

Whalen, Michael W. ;

Pike, Lee ;

Foltzer, Adam ;

Podhradsky, Michal ;

Klein, Gerwin ;

Kuz, Lhor ;

Andronick, June ;

Heiser, Gernot ;

Stuart, Douglas .

COMPUTER, 2018, 51 (11) :14-23

[4] Formal Reasoning About the Security of Amazon Web Services [J].

Cook, Byron .

COMPUTER AIDED VERIFICATION (CAV 2018), PT I, 2018, 10981 :38-47

← 1 →