Towards Formal Verification of Adaptive Cruise Controller using SpaceEx

被引：0
|
作者：
Mishra, Ambuj [1 ]
Roy, Subir K. [1 ]
机构：
[1] IIIT Bangalore, Bangalore, Karnataka, India
来源：
2016 INTERNATIONAL CONFERENCE ON VLSI SYSTEMS, ARCHITECTURES, TECHNOLOGY AND APPLICATIONS (VLSI-SATA) | 2016年
关键词：
Hybrid Systems; Formal Verification; Hybrid Automata;
D O I：
暂无
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
A formal mathematical model of an Adaptive Cruise Controller (ACC) in SpaceEx is presented with a view to formally verify it to ensure its safety critical behavior. SpaceEx (an academic open source tool) is a hybrid systems modeling and verification platform which employs efficient implementation of reachability and safety verification algorithms which are scalable under certain assumptions, to circumvent the difficult problem of formal verification of hybrid systems. In this paper, application of SpaceEx in the comprehensive verification of an Adaptive Cruise Controller for automobiles is presented.
引用
收藏
页数：6
相关论文
共 50 条
  • [31] A Solidity-to-CPN Approach Towards Formal Verification of Smart Contracts
    Garfatta, Ikram
    Klai, Kais
    Graiet, Mohamed
    Gaaloul, Walid
    2021 IEEE 30TH INTERNATIONAL CONFERENCE ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE 2021), 2021, : 69 - 74
  • [32] Towards a general methodology for formal verification on spiking neural P systems
    Perez-Jimenez, Mario J.
    Valencia-Cabrera, Luis
    Orellana-Martin, David
    Ramirez-de-Arellano, Antonio
    THEORETICAL COMPUTER SCIENCE, 2024, 1011
  • [33] Towards Formal Verification of Node RED-Based IoT Applications
    Garfatta, Ikram
    Souid, Nour Elhouda
    Klai, Kais
    VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS, VECOS 2023, 2024, 14368 : 90 - 104
  • [34] Formal Verification Problems in a Big Data World: Towards a Mighty Synergy
    Camilli, Matteo
    36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE COMPANION 2014), 2014, : 638 - 641
  • [35] Formal Verification of Business Processes using Model Checking
    Stoica, Florin
    INNOVATION MANAGEMENT AND EDUCATION EXCELLENCE VISION 2020: FROM REGIONAL DEVELOPMENT SUSTAINABILITY TO GLOBAL ECONOMIC GROWTH, VOLS I - VI, 2016, : 2563 - 2575
  • [36] Formal Verification of Database Applications Using Predicate Abstraction
    Alam M.I.
    Halder R.
    SN Computer Science, 2021, 2 (3)
  • [37] Verification of a cruise control system using counterexample-guided search
    Stursberg, O
    Fehnker, A
    Han, Z
    Krogh, BH
    CONTROL ENGINEERING PRACTICE, 2004, 12 (10) : 1269 - 1278
  • [38] Formal Verification of the Pastry Protocol Using TLA+
    Lu, Tianxiang
    DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015, 2015, 9409 : 284 - 299
  • [39] FORMAL VERIFICATION OF CONTRACTUAL SOFTWARE ARCHITECTURES USING SPIN
    Ozkaya, Mert
    MALAYSIAN JOURNAL OF COMPUTER SCIENCE, 2015, 28 (04) : 318 - 337
  • [40] Formal Verification of Graph Grammars using Mathematical Induction
    da Costa, Simone Andre
    Ribeiro, Leila
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 240 : 43 - 60
12345