Formal Methods for Message Sequence Charts.

作者: Doron A. Peled

DOI:

关键词:

摘要: The ISO standard for MSC provides a useful tool visualizing communication protocols. MSCs present model concurrency that is different from the of finite state systems, used frequently in automated verification. Thus, poses new and interesting problems related to automatic verification In this paper, some recent results are surveyed.

参考文章(15)
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
Edmund M. Clarke, E. Allen Emerson, DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC 25 Years of Model Checking. ,vol. 131, pp. 196- 215 ,(2008) , 10.1007/978-3-540-69850-0_12
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
Igor Walukiewicz, Difficult Configurations - On the Complexity of LTrL international colloquium on automata languages and programming. pp. 140- 151 ,(1998) , 10.1007/BFB0055048
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
Anca Muscholl, Doron Peled, Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces mathematical foundations of computer science. pp. 81- 91 ,(1999) , 10.1007/3-540-48340-3_8
Anca Muscholl, Doron Peled, Zhendong Su, Deciding Properties for Message Sequence Charts foundations of software science and computation structure. pp. 226- 242 ,(1998) , 10.1007/BFB0053553
Antonio Restivo, Sebastian Seibert, Wolfgang Thomas, Dora Giammarresi, Monadic second-order logic over rectangular pictures and recognizability by tiling systems Information & Computation. ,vol. 125, pp. 32- 45 ,(1996) , 10.1006/INCO.1996.0018
E. Allen Emerson, Edmund M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints international colloquium on automata, languages and programming. pp. 169- 181 ,(1980) , 10.1007/3-540-10003-2_69
Moshe Y Vardi, Pierre Wolper, An Automata-Theoretic Approach to Automatic Program Verification IEEE Computer Society. ,(1986)