Write a Blog >>
Thu 12 Nov 2020 08:03 - 08:04 at Virtual room 1 - Analysis 3

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 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change

08:00 - 08:02
Talk
Research Papers
Profir-Petru PârțachiUniversity College London, UK, Santanu Kumar DashUniversity of Surrey, UK, Miltiadis AllamanisMicrosoft Research, UK, Earl T. BarrUniversity College London, UK
DOI Pre-print Media Attached File Attached
08:03 - 08:04
Talk
Industry Papers
Jincao FengEast China Normal University, Weikai MiaoEast China Normal University, China, Hanyue ZhengEast China Normal University, Yihao HuangEast China Normal University, Jianwen LiEast China Normal University, China, Zheng WangBeijing Sunwise Information Technology, China, Ting SuEast China Normal University, China, Bin GuBeijing Institute of Control Engineering, China, Geguang PuShanghai Trusted Industrial Control Platform, China, Mengfei YangChina Academy of Space Technology, China, Jifeng HeShanghai Key Lab of Trustworthy Computing, China
DOI
08:05 - 08:06
Talk
Research Papers
Khouloud GaaloulUniversity of Luxembourg, Luxembourg, Claudio MenghiUniversity of Luxembourg, Luxembourg, Shiva NejatiUniversity of Ottawa, Canada / University of Luxembourg, Luxembourg, Lionel BriandUniversity of Ottawa, Canada / University of Luxembourg, Luxembourg, David WolfeQRA, Canada
DOI
08:07 - 08:08
Talk
Research Papers
Rahul GopinathCISPA, Germany, Björn MathisCISPA, Germany, Andreas ZellerCISPA, Germany
DOI
08:09 - 08:10
Talk
Research Papers
Michael PradelUniversity of Stuttgart, Germany, Georgios GousiosFacebook, USA, Jason LiuFacebook, USA, Satish ChandraFacebook, USA
DOI Pre-print Media Attached
08:11 - 08:30
Talk
Paper Presentations
Khouloud GaaloulUniversity of Luxembourg, Luxembourg, Michael PradelUniversity of Stuttgart, Germany, Profir-Petru PârțachiUniversity College London, UK, Rahul GopinathCISPA, Germany, M: Dan HaoPeking University, China