Formal verification of globally-iterated and locally-non-iterated finite state machines

被引：0
|
作者：
Ivanov, L [1 ]
Nunna, R [1 ]
机构：
[1] Stevens Inst Technol, Dept Comp Sci, Hoboken, NJ 07030 USA
来源：
42ND MIDWEST SYMPOSIUM ON CIRCUITS AND SYSTEMS, PROCEEDINGS, VOLS 1 AND 2 | 1999年
关键词：
D O I：
暂无
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
Formal Verification of hardware has significantly gained in popularity as an alternative to testing and simulation in hardware design. Recently we introduced a new methodology for verification of non-iterated systems. The technique is based on the inductively defined notion of a series-parallel poser. In this paper we extend the notion of series-parallel posers to allow the modeling of systems involving global iteration. For this class of systems we present a verification algorithm, and discuss its foundation.
引用
收藏
页码：202 / 205
页数：4
相关论文
共 50 条
  • [41] Formal Verification of IEC61499 Function Blocks with Abstract State Machines and SMV - Modelling
    Patil, Sandeep
    Dubinin, Victor
    Vyatkin, Valeriy
    2015 IEEE TRUSTCOM/BIGDATASE/ISPA, VOL 3, 2015, : 313 - 320
  • [42] FINITE-STATE MACHINES AND FORMAL GRAMMARS AS MEANS OF HARDWARE DESCRIPTION FOR COMPUTER ARCHITECTURES
    DITTMANN, J
    SIEMENS FORSCHUNGS-UND ENTWICKLUNGSBERICHTE-SIEMENS RESEARCH AND DEVELOPMENT REPORTS, 1980, 9 (05): : 294 - 297
  • [43] Formal Change Impact Analyses of Extended Finite State Machines using a Theorem Prover
    Guo, Bo
    Subramaniam, Mahadevan
    SEFM 2008: Sixth IEEE International Conference on Software Engineering and Formal Methods, Proceedings, 2008, : 335 - 344
  • [44] Design of decentralized critical observers for networks of finite state machines: A formal method approach
    Pola, Giordano
    De Santis, Elena
    Di Benedetto, Maria Domenica
    Pezzuti, Davide
    AUTOMATICA, 2017, 86 : 174 - 182
  • [45] An effective iterated greedy algorithm for scheduling unrelated parallel batch machines with non-identical capacities and unequal ready times
    Arroyo, Jose Elias C.
    Leung, Joseph Y. -T.
    COMPUTERS & INDUSTRIAL ENGINEERING, 2017, 105 : 84 - 100
  • [46] Distinguing Non-deterministic Timed Finite State Machines
    Gromov, Maxim
    El-Fakih, Khaled
    Shabaldina, Natalia
    Yevtushenko, Nina
    FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 137 - +
  • [47] Learning Abstracted Non-deterministic Finite State Machines
    Pferscher, Andrea
    Aichernig, Bernhard K.
    TESTING SOFTWARE AND SYSTEMS, ICTSS 2020, 2020, 12543 : 52 - 69
  • [48] Non-linear Error Detection for Finite State Machines
    Akdemir, Kahraman D.
    Hammouri, Ghaith
    Sunar, Berk
    INFORMATION SECURITY APPLICATIONS, 2009, 5932 : 226 - 238
  • [49] Formal Verification of Controller Synthesis Based on Incompletely Specified Finite State Machine Model
    Li, Wei
    Liu, Zhengyi
    Lu, Ying
    Wu, Ranguo
    2008 INTERNATIONAL SYMPOSIUM ON INTELLIGENT INFORMATION TECHNOLOGY APPLICATION, VOL III, PROCEEDINGS, 2008, : 593 - +
  • [50] Free subgroups of inverse limits of iterated wreath products of non-abelian finite simple groups in primitive actions
    Leinen, Felix
    Puglisi, Orazio
    JOURNAL OF GROUP THEORY, 2017, 20 (04) : 749 - 761
12345