Preprints of IIS SB RAS, 2013
Preprint 171
V.A. Nepomniaschy, S.A. Chernenok
Analysis of message sequence charts of distributed systems using colored Petri nets

Message Sequence Charts (MSCs) is a graphical description language for interaction scenarios standardized by the International Telecommunication Union (ITU). In particular, it is used for describing communication behaviors in real-time and telecommunication systems.

This paper presents a translation method from MSC and High-level MSC (HMSC) into Coloured Petri Nets and its implementation. Transformation rules for MSC elements cover the entire MSC standard, except data and time concepts. A software system that implements these algorithms is presented. Illustrated examples of translation are analyzed in the known CPNTools system.

Download the text in PDF (In Russian)
Preprint 170
I.S. Anureev
Conceptual basis of three-level method of C# program verification
In this paper a conceptual basis of the improved three-level method of C# program veri cation is described. The C#-light language is expanded upon unsafe code. Formal operational semantics of the languages C#-light and C#-kernel, based on domain-speci c transition systems, is de ned. The approach to veri cation conditions generation, based on safety logic of C#- kernel, is suggested. A new conception of the C#-kernel language considers it as a union of the C#-light language with the selected elements of the Atoment language. Translation of a C#-light program into C#-kernel is reduced to transformation of the program state based on the attributive annotation method and precomputation of C# constant expressions.

Download the text in PDF (In Russian)



You are reporting a typo in the following text:
Simply click the "Send typo report" button to complete the report. You can also include a comment.