FREPA: An Automated and Formal Approach to Requirement Modeling and Analysis in Aircraft Control Domain
Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects.
Thu 12 NovDisplayed time zone: (UTC) Coordinated Universal Time change
08:00 - 08:30 | |||
08:00 2mTalk | Flexeme: Untangling Commits Using Lexical Flows Research Papers Profir-Petru Pârțachi University College London, UK, Santanu Dash University of Surrey, UK, Miltiadis Allamanis Microsoft Research, UK, Earl T. Barr University College London, UK DOI Pre-print Media Attached File Attached | ||
08:03 1mTalk | FREPA: An Automated and Formal Approach to Requirement Modeling and Analysis in Aircraft Control Domain Industry Papers Jincao Feng East China Normal University, Weikai Miao East China Normal University, China, Hanyue Zheng East China Normal University, Yihao Huang East China Normal University, Jianwen Li East China Normal University, China, Zheng Wang Beijing Sunwise Information Technology, China, Ting Su East China Normal University, China, Bin Gu Beijing Institute of Control Engineering, China, Geguang Pu Shanghai Trusted Industrial Control Platform, China, Mengfei Yang China Academy of Space Technology, China, Jifeng He Shanghai Key Lab of Trustworthy Computing, China DOI | ||
08:05 1mTalk | Mining Assumptions for Software Components using Machine Learning Research Papers Khouloud Gaaloul University of Luxembourg, Luxembourg, Claudio Menghi University of Luxembourg, Luxembourg, Shiva Nejati University of Ottawa, Canada / University of Luxembourg, Luxembourg, Lionel Briand University of Ottawa, Canada / University of Luxembourg, Luxembourg, David Wolfe QRA, Canada DOI | ||
08:07 1mTalk | Mining Input Grammars from Dynamic Control Flow Research Papers DOI | ||
08:09 1mTalk | TypeWriter: Neural Type Prediction with Search-Based Validation Research Papers Michael Pradel University of Stuttgart, Germany, Georgios Gousios Facebook & Delft University of Technology, Jason Liu Facebook, USA, Satish Chandra Facebook, USA DOI Pre-print Media Attached | ||
08:11 19mTalk | Conversations on Analysis 3 Paper Presentations Khouloud Gaaloul University of Luxembourg, Luxembourg, Michael Pradel University of Stuttgart, Germany, Profir-Petru Pârțachi University College London, UK, Rahul Gopinath CISPA, Germany, M: Dan Hao Peking University, China | ||