Specification and verification of a real-time field bus with formal description languages

被引:0
|
作者
Marino, P [1 ]
Poza, F
Dominguez, M
Nogueira, J
机构
[1] Univ Vigo, Elect Technol Dept, Vigo, Spain
[2] Univ Vigo, Appl Elect Inst, Vigo, Spain
[3] ETS Ingn Ind, Vigo, Spain
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In this work the real-time field bus PROFIBUS for industrial communication networks, is specified with the formal specification language LOTOS and its associated tools. The paper introduces the general characteristics of LOTOS and its related tools, and the main features of PROFIBUS particularly the related with its data link layer. The methodology and data types implemented are explained, with an instance of developed performance tests for the specification. Results and new guidelines of this work are explained in last paragraph devoted to conclusions and future works. With LOTOS specification of PROFIBUS protocol comes up the possibility and benefit of using formal descriptions techniques for designs in the field of industrial communications.
引用
收藏
页码:415 / 429
页数:15
相关论文
共 50 条
  • [31] Extending Object-Z formal specification with Real-Time
    Wen, Zhicheng
    Chen, Zhigang
    INFORMATION TECHNOLOGY APPLICATIONS IN INDUSTRY, PTS 1-4, 2013, 263-266 : 1642 - 1646
  • [32] Aspect-Oriented Formal Specification for Real-Time Systems
    Zhang, Lichen
    ADVANCES IN COMPUTATIONAL SCIENCE AND ENGINEERING, 2009, 28 : 13 - 32
  • [33] AUTOMATED SUPPORT FOR THE FORMAL SPECIFICATION AND DESIGN OF REAL-TIME SYSTEMS
    HOSTUART, C
    ZEDAN, H
    FANG, M
    MICROPROCESSING AND MICROPROGRAMMING, 1993, 38 (1-5): : 79 - 86
  • [34] A formal specification method for building real-time distributed software
    Kim, TY
    Hong, SB
    Lee, YK
    INTERNATIONAL SOCIETY FOR COMPUTERS AND THEIR APPLICATIONS 13TH INTERNATIONAL CONFERENCE ON COMPUTERS AND THEIR APPLICATIONS, 1998, : 46 - 49
  • [35] Specification and automated verification of atomic concurrent real-time transactions
    Cai, Simin
    Gallina, Barbara
    Nystrom, Dag
    Seceleanu, Cristina
    SOFTWARE AND SYSTEMS MODELING, 2021, 20 (02): : 557 - 589
  • [36] A Framework for Specification and Verification of Timeout Models of Real-Time Systems
    Misra, Janardan
    CONTEMPORARY COMPUTING, 2011, 168 : 146 - 157
  • [38] PARAGON: A paradigm for the specification, verification and testing of real-time systems
    BenAbdallah, H
    Clarke, D
    Lee, I
    Sokolsky, O
    1997 IEEE AEROSPACE CONFERENCE PROCEEDINGS, VOL 2, 1997, : 469 - 488
  • [39] Specification and automated verification of real-time behaviour - a case study
    Kristensen, C.H.
    Andersen, J.H.
    Skou, A.
    Annual Reviews in Control, 1996, 20 : 55 - 70
  • [40] Incremental verification of architecture specification language for real-time systems
    Tsai, JJP
    Sistla, AP
    Paul, R
    THIRD INTERNATIONAL WORKSHOP ON OBJECT-ORIENTED REAL-TIME DEPENDABLE SYSTEMS, PROCEEDINGS, 1997, : 215 - 222