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 条
  • [41] Formal verification of concurrent programs using the Larch prover
    Chetali, B
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (01) : 46 - 62
  • [42] Towards Embedded Systems Formal Verification Translation from SysML into Petri Nets
    Szmuc, Wojciech
    Szmuc, Tomasz
    PROCEEDINGS OF THE 25TH INTERNATIONAL CONFERENCE MIXED DESIGN OF INTEGRATED CIRCUITS AND SYSTEM (MIXDES 2018), 2018, : 420 - 423
  • [43] Formal verification of simulation traces using computation slicing
    Sen, Alper
    Garg, Vijay K.
    IEEE TRANSACTIONS ON COMPUTERS, 2007, 56 (04) : 511 - 527
  • [44] Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
    Zhao, Xingyu
    Osborne, Matt
    Lantair, Jenny
    Robu, Valentin
    Flynn, David
    Huang, Xiaowei
    Fisher, Michael
    Papacchini, Fabio
    Ferrando, Angelo
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2019), 2019, 11724 : 105 - 124
  • [45] Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control
    Schiffl, Jonas
    Grundmann, Matthias
    Leinweber, Marc
    Stengele, Oliver
    Friebe, Sebastian
    Beckert, Bernhard
    PROCEEDINGS OF THE 26TH ACM SYMPOSIUM ON ACCESS CONTROL MODELS AND TECHNOLOGIES, SACMAT 2021, 2021, : 125 - 130
  • [46] Towards Formal Verification of Plans for Cognition-enabled Autonomous Robotic Agents
    Meywerk, Tim
    Walter, Marcel
    Herdt, Vladimir
    Grosse, Daniel
    Drechsler, Rolf
    2019 22ND EUROMICRO CONFERENCE ON DIGITAL SYSTEM DESIGN (DSD), 2019, : 129 - 136
  • [47] Towards Trustworthy RISC-V Designs: Formal Verification of the MFENCE Instruction
    Ponugoti, Kushal K.
    Karlapalem, Nikhila
    4TH INTERDISCIPLINARY CONFERENCE ON ELECTRICS AND COMPUTER, INTCEC 2024, 2024,
  • [48] Formal Verification of Analog and Mixed Signal Designs Using SPICE Circuit Simulation Traces
    Lata, Kusum
    Roy, Subir K.
    JOURNAL OF ELECTRONIC TESTING-THEORY AND APPLICATIONS, 2013, 29 (05): : 715 - 740
  • [49] Formal Verification of Analog and Mixed Signal Designs Using SPICE Circuit Simulation Traces
    Kusum Lata
    Subir K. Roy
    Journal of Electronic Testing, 2013, 29 : 715 - 740
  • [50] Formal Verification of Full-Wave Rectifier using SPICE Circuit Simulation Traces
    Lata, Kusum
    Jamadagni, H. S.
    PROCEEDINGS OF THE ELEVENTH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN (ISQED 2010), 2010, : 264 - 270