Modeling and verification of the SDL-specified communication protocols using high-level Petri nets

被引：0
作者：
V. A. Nepomniaschy
V. S. Argirov
D. M. Beloglazov
A. V. Bystrov
E. A. Chetvertakov
T. G. Churina
机构：
[1] Russian Academy of Sciences,Ershov Institute of Information Systems, Siberian Branch
[2] Novosibirsk State University,undefined
来源：
Programming and Computer Software | 2008年 / 34卷
关键词：
Process Instance; Input Place; Service Place; Output Place; Model Check Method;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
To simplify modeling and verification of communication protocols presented in the SDL language, the so-called hierarchical typed timed Petri nets (HTT nets), which are substantial modifications of colored Petri nets, are introduced. A method of translation of the SDL language into HTT nets is described. A program complex SPV (SDL Protocol Verifier), which includes a translator from SDL into HTT nets and means for editing, simulation, visualization, and verification of these net models, is presented. For the verification, a model checking method for properties presented by μ-calculus formulas is used. Experiments on application of the SPV complex for modeling and verifying two ring protocols (RE and ATMR protocols), an optimized version of the sliding window protocol (i-protocol), and a dynamic version of the InRes protocol are described
引用
收藏
页码：330 / 340
页数：10
相关论文
共 43 条
[1]  
Kristensen L.M.(1998)The Practitioner’s Guide to Coloured Petri Nets Int. J. Software Tools Technology Transfer 2 98-132
[2]  
Christensen S.(2003)CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets Lecture Notes in Computer Science (Proc. of ICATPN 2003) 2679 450-462
[3]  
Jensen K.(1998)A Compositional Net Semantics for SDL Lecture Notes in Computer Science 1420 144-164
[4]  
Ratzer A.V.(2003)Automatic Formal Model Generation and Analysis of SDL Lecture Notes in Computer Science 2708 285-299
[5]  
Wells L.(1998)Combining Finite Automata. Parallel Programs and SDL Using Petri Nets Lecture Notes in Computer Science 1384 102-117
[6]  
Lassen H.M.(1999)Emma: Developing an Industrial Reachability Anallyser for SDL Lecture Notes in Computer Science (Proc. of Int. Congress on Formal Methods) 1708 642-661
[7]  
Laursen A.M.(2007)Application of Modified Coloured Petri Nets to Modeling and Verification of SDL Specified Communication Protocols Lecture Notes in Computer Science (Proc. of CSR 2007) 4649 303-314
[8]  
Qvortrup J.F.(1991)Modelling and Verification of Time Dependant Systems Using Time Petri Nets IEEE Trans. Software Eng. 17 259-273
[9]  
Stissing M.S.(2003)The Petri Net Markup Language, Petri Net Technology for Communication Based Systems Lecture Notes in Computer Science 2472 124-144
[10]  
Westergaard M.(1991)An Efficient Reliable Ring Protocol IEEE Trans. Commun. 39 1616-1624
12345