Computer Science, № 20, 2004

A new language of finite state machines called USL is proposed. The language is intended for rapid development of formal verification-oriented operational semantics of modern programming languages. Formal operational semantics of the USL language is defined. The USL-based approach to programming language semantics design is illustrated by the example of...

In this paper, we try to decide a problem of recognising timed testing equivalences for timed event structures with dense internal actions. For this purpose, we construct a formula that characterizes a timed event structure up to the timed must-preorder. So, to understand if two timed event structures are...

We study the model checking problem for fixpoint logics in well- structured multiaction transition systems. P.A. Abdulla et al. (1996) and Finkel & Schnoebelen (2001) examined the decidability problem for liveness (reachability) and progress (eventuality) properties in well-structured single action transition systems. Our main result is as follows: the model...

A new three-level approach to sequential object-oriented program verification is presented. It is applied to a significant С# subset called C#-light that includes all principal sequential С# constructs. At the first stage, C#-light is translated into an intermediate language C#-kernel that allows us to simplify axiomatic semantics. At the second...

This work considers a model of a multilevel information system that integrates heterogeneous classes of objects of different configuration and complexity range. The architectural solution is suggested that allows dynamical extension of a working system by connecting objects both of existing classes and new classes as well. The use of...

Stochastic Petri nets (SPNs) is a well-known model for quantitative analysis. We consider the class called DTWSPNs that is a modification of discrete time SPNs (DTSPNs) by transition labeling and weights. Transitions of DTWSPNs are labeled by actions that represent elementary activities and can be visible or invisible for an...

It is shown in the paper that state-based algebraic semantics of an imperative program can be regarded as a compiler abstract model and can serve as a good assistant of the compiler designer.