Simplifying Requirements Formalization for Resource-Constrained Mission-Critical Software

被引：1

作者：

de Ferro, Carlos Mao ^{[1
]}

Mavridou, Anastasia ^{[2
]}

Dille, Michael ^{[2
]}

Martins, Francisco ^{[3
]}

机构：

[1] Univ Lisbon, Fac Ciencias, LASIGE, Lisbon, Portugal

[2] NASA, Ames Res Ctr, KBR Inc, Washington, DC 20546 USA

[3] Univ Acores, Ponta Delgada, Portugal

来源：

2023 53RD ANNUAL IEEE/IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS WORKSHOPS, DSN-W | 2023年

关键词：

requirements; verification; mission-critical code; VERIFICATION;

D O I：

10.1109/DSN-W58399.2023.00066

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Developing critical software requires adherence to rigorous software development practices, such as formal requirement specification and verification. Despite their importance, such practices are often considered as complex and challenging tasks that require a strong formal methods background. In this paper, we present our work on simplifying the formal requirements specification experience for resource-constrained mission critical software through the use of structured natural language. To this end, we connect NASA's FRET, a formal requirement elicitation and authoring tool with the Shelley model checking framework for MicroPython code. We report our experience on using these tools to specify requirements and analyze code from the NASA Ames PHALANX exploration concept.

引用

页码：263 / 266

页数：4

共 50 条

[21] Fuzzy Self-Adaptation of Mission-Critical Software Under Uncertainty
杨启亮
吕建
陶先平
马晓星
邢建春
宋巍
Journal of Computer Science & Technology, 2013, 28 (01) : 165 - 187
[22] Evaluation of the resource-constrained critical path method algorithms
Kim, K
de la Garza, JM
JOURNAL OF CONSTRUCTION ENGINEERING AND MANAGEMENT, 2005, 131 (05) : 522 - 532
[23] Strong valid inequalities for the resource-constrained scheduling problem with uniform resource requirements
Hardin, Jill R.
Nernhauser, George L.
Savelsbergh, Martin W. P.
DISCRETE OPTIMIZATION, 2008, 5 (01) : 19 - 35
[24] Formalization and assessment of regulatory requirements for safety-critical software
Vilkomir, Sergiy A.
Bowen, Jonathan P.
Ghose, Aditya K.
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2006, 2 (3-4) : 165 - 178
[25] Critical Sequences and Resource Links Optimization in Resource-Constrained Project Scheduling
Cui, Wan-An
ASIA-PACIFIC JOURNAL OF OPERATIONAL RESEARCH, 2018, 35 (05)
[26] Fuzzy Self-Adaptation of Mission-Critical Software Under Uncertainty
Yang, Qi-Liang
Lv, Jian
Tao, Xian-Ping
Ma, Xiao-Xing
Xing, Jian-Chun
Song, Wei
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2013, 28 (01) : 165 - 187
[27] An Evolutionary Algorithm for Online, Resource-Constrained, Multivehicle Sensing Mission Planning
Tsiogkas, Nikolaos
Lane, David M.
IEEE ROBOTICS AND AUTOMATION LETTERS, 2018, 3 (02): : 1199 - 1206
[28] A contract-based approach of resource-constrained software deployment
Le Sommer, N
Guidec, F
COMPONENT DEPLOYMENT, 2002, 2370 : 15 - 30
[29] A framework for resource-constrained rate-optimal software pipelining
Govindarajan, R
Altman, ER
Gao, GR
IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 1996, 7 (11) : 1133 - 1149
[30] Dynamic software update of resource-constrained distributed embedded systems
Felser, Meik
Kapitza, Rüdiger
Kleinöder, Jürgen
Schröder-Preikschat, Wolfgang
IFIP Advances in Information and Communication Technology, 2015, 231 : 387 - 400

← 1 2 3 4 5 →