Formal verification of abstract system and protocol specifications

被引：0
|
作者：
Schneider, Axel [1 ]
Bluhm, Thomas [1 ]
Renner, Tobias [1 ]
Heinkel, Ulrich [1 ]
Knaeblein, Joachim [1 ]
Zavala, Reynaldo [1 ]
机构：
[1] Lucent Technol Network Syst GmbH, Nurnberg, Germany
来源：
30TH ANNUAL IEEE/NASA SOFTWARE ENGINEERING WORKSHOP, PROCEEDINGS | 2006年
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Formal methods such as automated model checking are used commercially for digital circuit design verification. These techniques find errors early in the product cycle, which improves development time and cost. By contrast, the current practice in complex system design is to specify system functions and protocol details in natural language. Some errors are found early by manual inspections, but others are only revealed during implementation testing or by costly field failures. We describe our application of formal specification and model checking to real telecom product development, and enumerate the classes of specification errors that these formal techniques revealed at an early stage of the development cycle.
引用
收藏
页码：207 / +
页数：2
相关论文
共 50 条
  • [1] Formal Specifications and Verification of a Secure Communication Protocol Model
    Xia Yang 1
    2. Research Center for Information Network Security
    [J]. Journal of Systems Engineering and Electronics, 2003, (02) : 90 - 97
  • [2] ARE CONSTRUCTIVE FORMAL SPECIFICATIONS LESS ABSTRACT
    VANHOREBEEK, I
    LEWI, J
    [J]. SIGPLAN NOTICES, 1990, 25 (05): : 60 - 68
  • [3] A formal abstract semantics for data specifications
    Piessens, F
    Steegmans, E
    [J]. 15TH INTERNATIONAL CONGRESS ON CYBERNETICS, PROCEEDINGS, 1999, : 983 - 988
  • [4] An Innovative Teaching Tool for the Verification of Abstract Data Type Implementations from Formal Algebraic Specifications
    del Vado Virseda, Rafael
    Perez Morente, Fernando
    [J]. PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE, ICCS 2012, 2012, 9 : 1743 - 1752
  • [5] A Software Testing Tool for the Verification of Abstract Data Type Implementations from Formal Algebraic Specifications
    del Vado Virseda, Rafael
    [J]. 2012 IEEE 25TH CONFERENCE ON SOFTWARE ENGINEERING EDUCATION AND TRAINING (CSEE&T), 2012, : 100 - 104
  • [6] Formal abstract architecture for use case specifications
    Rysavy, O
    Bures, F
    [J]. 11TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOP ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 2004, : 203 - 210
  • [7] Formal verification and validation of interactive systems specifications -: From informal specifications to formal validation
    Aït-Ameur, Y
    Breholée, B
    Girard, P
    Guittet, L
    Jambon, F
    [J]. HUMAN ERROR, SAFETY AND SYSTEMS DEVELOPMENT, 2004, 152 : 61 - 76
  • [8] Formal verification of safety protocol in train control system
    ZHANG Yan1
    2 Railway Technologies Research Centre
    [J]. Science China Technological Sciences, 2011, (11) : 3078 - 3090
  • [9] Formal verification of safety protocol in train control system
    Zhang Yan
    Tang Tao
    Li KePing
    Mera, Jose Manuel
    Zhu Li
    Zhao Lin
    Xu TianHua
    [J]. SCIENCE CHINA-TECHNOLOGICAL SCIENCES, 2011, 54 (11) : 3078 - 3090
  • [10] Formal Verification of Cryptographic Protocol for Secure RFID System
    Kim, Hyun-Seok
    Oh, Jung-Hyun
    Kim, Ju-Bae
    Jeong, Yeon-Oh
    Choi, Jin-Young
    [J]. NCM 2008: 4TH INTERNATIONAL CONFERENCE ON NETWORKED COMPUTING AND ADVANCED INFORMATION MANAGEMENT, VOL 2, PROCEEDINGS, 2008, : 470 - 477
12345