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.

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.



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.