Experience with Applying Formal Methods to Protocol Specification and System Architecture

被引:0
|
作者
Mani Azimi
Ching-Tsun Chou
Akhilesh Kumar
Victor W. Lee
Phamndra K. Mannava
Seungjoon Park
机构
[1] Intel Corporation,
[2] SC12-608,undefined
来源
关键词
formal verification; cache coherence protocols; sliding window protocols; rule-based checking of tables; minimal deadlock-free wormhole routing schemes; fault-tolerant link initialization;
D O I
暂无
中图分类号
学科分类号
摘要
In the last three years or so we at Enterprise Platforms Group at Intel Corporation have been applying formal methods to various problems that arose during the process of defining platform architectures for Intel's processor families. In this paper we give an overview of some of the problems we have worked on, the results we have obtained, and the lessons we have learned. The last topic is addressed mainly from the perspective of platform architects.
引用
收藏
页码:109 / 116
页数:7
相关论文
共 50 条
  • [21] Formal specification and verification of a micropayment protocol
    Gouda, MG
    Liu, AX
    [J]. ICCCN 2004: 13TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS, 2004, : 489 - 494
  • [22] AN INFORMAL OVERVIEW OF FORMAL PROTOCOL SPECIFICATION
    RUDIN, H
    [J]. IEEE COMMUNICATIONS MAGAZINE, 1985, 23 (03) : 46 - 52
  • [23] FORMAL TECHNIQUES FOR PROTOCOL SPECIFICATION AND VERIFICATION
    SUNSHINE, C
    [J]. COMPUTER, 1979, 12 (09) : 20 - 27
  • [24] Formal methods in fieldbus specification
    Zezulka, F
    Hintze, E
    Kucera, P
    [J]. 7TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL VII, PROCEEDINGS, 2003, : 48 - 53
  • [25] Applying formal methods to a certifiably secure software system
    Heitmeyer, Constance L.
    Archer, Myla M.
    Leonard, Elizabeth I.
    McLean, John D.
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2008, 34 (01) : 82 - 98
  • [26] A survey: Applying formal methods to a software intensive system
    de Groot, A
    Hooman, J
    Kordon, F
    Paviot-Adet, E
    Mounier, I
    Lemoine, M
    Gaudiere, G
    Winter, VL
    Kapur, D
    [J]. SIXTH IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING, 2001, : 55 - 64
  • [27] Towards the formal specification of an OPS5 production system architecture
    Gold, David I.
    Plant, R.T.
    [J]. International Journal of Intelligent Systems, 1994, 9 (08): : 739 - 768
  • [28] TOWARDS THE FORMAL SPECIFICATION OF AN OPS5 PRODUCTION SYSTEM ARCHITECTURE
    GOLD, DI
    PLANT, RT
    [J]. INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS, 1994, 9 (08) : 739 - 768
  • [29] Combining formal specification methods and informal specification methods for requirement analysis
    Zhang, LC
    [J]. 1997 IEEE PACIFIC RIM CONFERENCE ON COMMUNICATIONS, COMPUTERS AND SIGNAL PROCESSING, VOLS 1 AND 2: PACRIM 10 YEARS - 1987-1997, 1997, : 444 - 447
  • [30] Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods
    Davide Basile
    Maurice H. ter Beek
    Alessio Ferrari
    Axel Legay
    [J]. International Journal on Software Tools for Technology Transfer, 2022, 24 : 351 - 370