A formal approach to AADL model-based software engineering

被引：9
|
作者：
Mkaouar, Hana [1 ]
Zalila, Bechir [1 ]
Hugues, Jerome [2 ]
Jmaiel, Mohamed [1 ,3 ]
机构：
[1] Univ Sfax, Natl Sch Engn Sfax, ReDCAD Lab, BP 1173, Sfax 3038, Tunisia
[2] Univ Toulouse, ISAE, SUPAERO, F-31055 Toulouse 4, France
[3] Digital Res Ctr Sfax, BP 275, Sfax 3021, Tunisia
来源：
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER | 2020年 / 22卷 / 02期
关键词：
Safety-critical software engineering; Real-time systems; Ravenscar profile; AADL; Formal specification; Model-checking; CADP; VERIFICATION; TIME; SEMANTICS; ARCHITECTURES; LANGUAGES; CHECKING; SAFETY;
D O I：
10.1007/s10009-019-00513-7
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Formal methods have become a recommended practice in safety-critical software engineering. To be formally verified, a system should be specified with a specific formalism such as Petri nets, automata and process algebras, which requires a formal expertise and may become complex especially with large systems. In this paper, we report our experience in the formal verification of safety-critical real-time systems. We propose a formal mapping for a real-time task model using the LNT language, and we describe how it is used for the integration of a formal verification phase in an AADL model-based development process. We focus on real-time systems with event-driven tasks, asynchronous communication and preemptive fixed-priority scheduling. We provide a complete tool-chain for the automatic model transformation and formal verification of AADL models. Experimentation illustrates our results with the Flight control system and Line follower robot case studies.
引用
收藏
页码：219 / 247
页数：29
相关论文
共 50 条
  • [31] The formal economic model of software engineering
    Wang, Yingxu
    Yuan, Yuyu
    2006 CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1-5, 2006, : 1972 - +
  • [32] A formal approach to component-based software engineering: Education and evaluation
    Sitaraman, M
    Long, TJ
    Weide, BW
    Harner, EJ
    Wang, LQ
    PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2001, : 601 - 609
  • [33] ADVANCED MODEL-BASED SOFTWARE ENGINEERING TECHNOLOGIES FOR SOFTWARE DEFINED RADIO CONFIGURATION
    Liu, William C.
    McNeill, Kevin M.
    Cook, Michael
    Krikeles, Basil
    MILITARY COMMUNICATIONS CONFERENCE, 2010 (MILCOM 2010), 2010, : 1147 - 1150
  • [34] Return on Investment in Model-Based Systems Engineering Software Tools
    Duffy, James B.
    Feng, Jingyao
    Combs, Robert
    Richardson, James P.
    INCOSE International Symposium, 2021, 31 (01) : 791 - 805
  • [35] Seamless Method-and Model-based Software and Systems Engineering
    Broy, Manfred
    FUTURE OF SOFTWARE ENGINEERING, 2011, : 33 - 47
  • [36] MODEL-BASED SOFTWARE ENGINEERING IN LARGER SCALE PROJECT COURSES
    BRUEGGE, B
    COYNE, RF
    SOFTWARE ENGINEERING EDUCATION, 1993, 40 : 273 - 287
  • [37] On the Needs and Challenges of Model-Based Engineering for Spaceflight Software Systems
    Pettit, Robert G.
    Mezcciani, Navneet
    Fant, Julie
    2014 IEEE 17TH INTERNATIONAL SYMPOSIUM ON OBJECT/COMPONENT/SERVICE-ORIENTED REAL-TIME DISTRIBUTED COMPUTING (ISORC), 2014, : 25 - 31
  • [38] Engineering Model-Based Software Testing of WIMP Interactive Applications
    Canny A.
    Martinie C.
    Navarre D.
    Palanque P.
    Barboni E.
    Gris C.
    Proceedings of the ACM on Human-Computer Interaction, 2021, 5 (EICS)
  • [39] Model-Based Software Engineering and Certification: Some Open Issues
    Russo, Stefano
    Scippacercola, Fabio
    2016 IEEE 27TH INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING WORKSHOPS (ISSREW), 2016, : 237 - 240
  • [40] Ontology Evolution in the Context of Model-Based Secure Software Engineering
    Buerger, Jens
    Kehrer, Timo
    Juerjens, Jan
    RESEARCH CHALLENGES IN INFORMATION SCIENCE (RCIS 2020), 2020, 385 : 437 - 454
12345