Verification of Scenario-based Specifications using Templates
作者： Girish Keshav Palshikar , Purandar Bhaduri
DOI: 10.1016/J.ENTCS.2004.12.017
关键词:
摘要: Specifying dynamic behaviour of a system by listing scenarios its interactions has become popular practice. Message sequence chart (MSC) is rigorous and widely used notation for specifying such behaviour. High-level MSCs (HMSC) provide hierarchical modular composition facilities constructing complex from basic MSCs. Although the general problem formal verification properties HMSCs intractable, we propose framework restricted verification. We present simple templates commonly types discuss efficient algorithms verifying them.
core.ac.uk
elsevier.com
iitg.ac.in 
sci-hub.se 参考文章(26)
David K. Huber, Garry D. Coleman, Advancing the Standard Mechanical Engineering. ,vol. 121, pp. 78- 80 ,(1999) , 10.1115/1.1999-OCT-7
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
Blaise Genest, Anca Muscholl, Helmut Seidl, Marc Zeitoun, Infinite-State High-Level MSCs: Model-Checking and Realizability international colloquium on automata languages and programming. pp. 657- 668 ,(2002) , 10.1007/3-540-45465-9_56
Doron Peled, Specification and Verification of Message Sequence Charts IFIP Advances in Information and Communication Technology. pp. 139- 154 ,(2000) , 10.1007/978-0-387-35533-7_9
Wil Janssen, Radu Mateescu, Sjouke Mauw, Peter Fennema, Petra van der Stappen, Model Checking for Managers international workshop on model checking software. pp. 92- 107 ,(1999) , 10.1007/3-540-48234-2_7
Vladimir Levin, Doron Peled, Verification of Message Sequence Charts via Template Matching colloquium on trees in algebra and programming. pp. 652- 666 ,(1997) , 10.1007/BFB0030632
Rajeev Alur, Mihalis Yannakakis, Model Checking of Message Sequence Charts CONCUR’99 Concurrency Theory. pp. 114- 129 ,(1999) , 10.1007/3-540-48320-9_10
Werner Damm, David Harel, LSCs: Breathing Life into Message Sequence Charts formal methods. ,vol. 19, pp. 45- 80 ,(2001) , 10.1023/A:1011227529550
Thomas Gehrke, Michaela Huhn, Arend Rensink, Heike Wehrheim, An Algebraic Semantics for Message Sequence Chart Documents formal techniques for (networked and) distributed systems. pp. 3- 18 ,(1998) , 10.1007/978-0-387-35394-4_1
Peter Graubmann, Ekkart Rudolph, HyperMSCs and sequence diagrams for use case modelling and testing Lecture Notes in Computer Science. pp. 32- 46 ,(2000) , 10.5555/1765175.1765179