Formal verification of FIRE: A case study

被引：0
|
作者：
Jang, JY
Qadeer, S
Kaufmann, M
Pixley, C
机构：
来源：
DESIGN AUTOMATION CONFERENCE - PROCEEDINGS 1997 | 1997年
关键词：
D O I：
10.1109/DAC.1997.597139
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We present our experiences with the formal verification of an automotive chip used to control the safety features in a car, We used a BDD based model checker in our work. We describe our verification methodology for verifying a very complicated property on a relatively large design. We also describe the bugs that were found and present our views on how to make model checking an effective integrated part of the design flow for complex hardware systems.
引用
收藏
页码：173 / 177
页数：3
相关论文
共 50 条
  • [31] Polynomial Formal Verification of a Processor: A RISC-V Case Study
    Weingarten, Lennart
    Mahzoon, Alireza
    Goli, Mehran
    Drechsler, Rolf
    2023 24TH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN, ISQED, 2023, : 41 - 47
  • [32] Formal Verification of Translation Validators A Case Study on Instruction Scheduling Optimizations
    Tristan, Jean-Baptiste
    Leroy, Xavier
    POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, : 17 - 27
  • [33] Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods
    Srivas, MK
    Miller, SP
    FORMAL METHODS IN SYSTEM DESIGN, 1996, 8 (02) : 153 - 188
  • [34] Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study
    Webster, Matt
    Dixon, Clare
    Fisher, Michael
    Salem, Maha
    Saunders, Joe
    Koay, Kheng Lee
    Dautenhahn, Kerstin
    Saez-Pons, Joan
    IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS, 2016, 46 (02) : 186 - 196
  • [35] Process mining approach to formal business process modelling and verification: a case study
    Ito, Sohei
    Vymetal, Dominik
    Sperka, Roman
    JOURNAL OF MODELLING IN MANAGEMENT, 2021, 16 (02) : 602 - 622
  • [36] Towards Formal Verification for Cyber-physically Agnostic Software: a Case Study
    Drozdov, Dmitrii
    Patil, Sandeep
    Dubinin, Victor
    Vyatkin, Valeriy
    IECON 2017 - 43RD ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2017, : 5509 - 5514
  • [37] SPIN vs. VIS: A case study on the formal verification of the ATMR protocol
    Peng, H
    Tahar, S
    Khendek, F
    ICFEM 2000: THIRD INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 2000, : 79 - 87
  • [38] Formal Verification With Frama-C: A Case Study in the Space Software Domain
    Busquim e Silva, Rovedy Aparecida
    Arai, Nanci Naomi
    Burgareli, Luciana Akemi
    Parente de Oliveira, Jose Maria
    Pinto, Jorge Sousa
    IEEE TRANSACTIONS ON RELIABILITY, 2016, 65 (03) : 1163 - 1179
  • [39] A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System
    Iftikhar, M. Usman
    Weyns, Danny
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (91): : 45 - 62
  • [40] Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA
    Gouglidis, Antonios
    Grompanopoulos, Christos
    Mavridou, Anastasia
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (272): : 52 - 64
12345