Verification of Message Sequence Charts via Template Matching
作者： Vladimir Levin , Doron Peled
DOI: 10.1007/BFB0030632
关键词: Sequence 、 Template 、 Matching (statistics) 、 Design tool 、 Transitive closure 、 Communications system 、 Theoretical computer science 、 Computer science 、 Template matching 、 Chart
摘要: Message sequence charts are becoming a popular low-level design tool for communication systems. When applied to systems of non-trivial size, organizing and manipulating them become challenge. We present methodology specifying verifying message charts. Specification is given using templates, namely with only partial information about the participating events their interrelated order. Verification done by search whose aim match templates against The result such either reports that no matching chart exists, or returns examples satisfy constraints appear in template. describe algorithm an implementation.
springer.com
sci-hub.se 参考文章(11)
Rajeev Alur, Gerard J. Holzmann, Doron Peled, An analyzer for message sequence charts tools and algorithms for construction and analysis of systems. pp. 35- 48 ,(1996) , 10.1007/3-540-61042-1_37
Stephen Cole Kleene, Representation of Events in Nerve Nets and Finite Automata Princeton University Press. pp. 3- 42 ,(1951) , 10.1515/9781400882618-002
Wil Janssen, Job Zwiers, Protocol Design by Layered Decomposition: A Compositional Approach Proceedings of the Second International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. pp. 307- 326 ,(1992) , 10.1007/3-540-55092-5_17
Walter J. Savitch, Relationships between nondeterministic and deterministic tape complexities Journal of Computer and System Sciences. ,vol. 4, pp. 177- 192 ,(1970) , 10.1016/S0022-0000(70)80006-X
Mogens Nielsen, Gordon Plotkin, Glynn Winskel, Petri nets, event structures and domains, part I Theoretical Computer Science. ,vol. 13, pp. 85- 108 ,(1981) , 10.1016/0304-3975(81)90112-2
Eike Best, Raymond Devillers, Sequential and concurrent behaviour in Petri net theory Theoretical Computer Science. ,vol. 55, pp. 87- 136 ,(1987) , 10.1016/0304-3975(87)90090-9
Tzilla Elrad, Nissim Francez, Decomposition of distributed programs into communication-closed layers Science of Computer Programming. ,vol. 2, pp. 155- 173 ,(1982) , 10.1016/0167-6423(83)90013-8
Gerard J. Holzmann, Early Fault Detection Tools tools and algorithms for construction and analysis of systems. pp. 1- 13 ,(1996) , 10.1007/3-540-61042-1_34
Mogens Nielsen, Gordon Plotkin, Glynn Winskel, Petri Nets, Event Structures and Domains Proceedings of the International Sympoisum on Semantics of Concurrent Computation. pp. 266- 284 ,(1979) , 10.1007/BFB0022474
Vaughan Pratt, Modeling concurrency with partial orders International Journal of Parallel Programming. ,vol. 15, pp. 33- 71 ,(1986) , 10.1007/BF01379149