Software-defined networks (SDN) are a novel paradigm of networking which became an enabler technology for many modern applications such as network virtualization, policy-based access control and many others. Software can provide flexibility and fast-paced innovations in the networking; however, it has a complex nature. In this connection there is an increasing necessity of means for assuring its correctness and security. Abstract models for SDN can tackle these challenges. This paper addresses to confidentiality and some integrity properties of SDNs. These are critical properties for multi-tenant SDN environments, since the network management software must ensure that no confidential data of one tenant are leaked to other tenants in spite of using the same physical infrastructure. We define a notion of end-to-end security in context of software-defined networks and propose a semantic model where the reasoning is possible about confidentiality, and we can check that confidential information flows do not interfere with non-confidential ones. We show that the model can be extended in order to reason about networks with secure and insecure links which can arise, for example, in wireless environments.

The article is published in the authors’ wording.

The article considers the specifics of a model oriented approach to software development based on the usage of Model Driven Architecture (MDA), Model Driven Software Development (MDSD) and Model Driven Development (MDD) technologies. Benefits of this approach usage in the software development industry are described. The main emphasis is put on the system design, automated code generation for large systems, verification, proof of system properties and reduction of bug density. Drawbacks of the approach are also considered. The approach proposed in the article is specific for industrial software systems development. These systems are characterized by different levels of abstraction, which is used on modeling and code development phases. The approach allows to detail the model to the level of the system code, at the same time store the verified model semantics and provide the checking of the whole detailed model. Steps of translating abstract data structures (including transactions, signals and their parameters) into data structures used in detailed system implementation are presented. Also the grammar of a language for specifying rules of abstract model data structures transformation into real system detailed data structures is described. The results of applying the proposed method in the industrial technology are shown.

The article is published in the authors’ wording.

The problem of improving precision of static analysis and verification techniques for C is hard due to simplification assumptions these techniques make about the code model. We present a novel approach to improving precision by executing the code model in a controlled environment that captures program errors and contract violations in a memory and time efficient way. We implemented this approach as an executor module Tassadar as a part of bounded model checker Borealis. We tested Tassadar on two test sets, showing that its impact on performance of Borealis is minimal.

The article is published in the authors’ wording.

The C-program verification is an urgent problem of modern programming. To apply known methods of deductive verification it is necessary to provide loop invariants which might be a challenge in many cases. In this paper we consider the C-light language [18] which is a powerful subset of the ISO C language. To verify C-light programs the two-level approach [19, 20] and the mixed axiomatic semantics method [1, 3, 11] were suggested. At the first stage, we translate [17] the source C-light program into Ckernel one. The C-kernel language [19] is a subset of C-light. The theorem of translation correctness was proved in [10, 11]. The C-kernel has less statements with respect to the C-light, this allows to decrease the number of inference rules of axiomatic semantics during its development. At the second stage of this approach, the verification conditions are generated by applying the rules of mixed axiomatic semantics [10, 11] which could contain several rules for the same program statement. In such cases the inference rules are applied depending on the context. Let us note that application of the mixed axiomatic semantics allows to significantly simplify verification conditions in many cases. This article represents an extension of this approach which includes our verification method for definite iteration over unchangeable data structures without loop exit in C-light programs. The method contains a new inference rule for the deifinite iteration without invariants. This rule was implemented in verification conditions generator. At the proof stage the SMT-solver Z3 [12] is used. An example which illustrates the application of this technique is considered.

he article is published in the authors’ wording.

There is a widespread and rapidly growing interest to the parallel programming nowadays. This interest is based on availability of supercomputers, computer clusters and powerful graphic processors for computational mathematics and simulation. MPI, OpenMP, CUDA and other technologies provide opportunity to write C and FORTRAN code for parallel speed-up of execution without races for resources. Nevertheless concurrency issues (like races) are still very important for parallel systems in general and distributed systems in particular. Due to this reason, there is a need of research, study and teaching of formal models of concurrency and methods of distributed system verification.

The paper presents an individual experience with teaching Formal Models of Concurrency as a graduate elective course for students specializing in high-performance computing. First it sketches course background, objectives, lecture plan and topics. Then the paper presents how to formalize (i.e. specify) a reachability puzzle in semantic, syntactic and logic formal models, namely: in Petri nets, in a dialect of Calculus of Communicating Systems (CCS) and in Computation Tree Logic (CTL). This puzzle is a good educational example to present specifics of different formal notations.

The article is published in the author’s wording.

We discuss the concept of Lax-Darboux scheme and illustrate it on well known examples associated with the Nonlinear Schro¨dinger (NLS) equation. We explore the Darboux links of the NLS hierarchy with the hierarchy of Heisenberg model, principal chiral field model as well as with differential-difference integrable systems (including the Toda lattice and differential-difference Heisenberg chain) and integrable partial difference systems. We show that there exists a transformation which formally diagonalises all elements of the Lax-Darboux scheme simultaneously. It provides us with generating functions of local conservation laws for all integrable systems obtained. We discuss the relations between conservation laws for systems belonging to the Lax-Darboux scheme.

Information systems (IS) produce numerous traces and logs at runtime. In the context of SOA-based (service-oriented architecture) IS, these logs contain details about sequences of process and service calls. Modern application monitoring and error tracking tools provide only rather straightforward log search and filtering functionality. However, “clever” analysis of the logs is highly useful, since it can provide valuable insights into the system architecture, interaction of business domains and services. Here we took runs event logs (trace data) of a big booking system and discovered architectural guidelines violations and common anti-patterns. We applied mature process mining techniques for discovery and analysis of these logs. The aims of process mining are to discover, analyze, and improve processes on the basis of IS behavior recorded as event logs. In several specific examples, we show successful applications of process mining to system runtime analysis and motivate further research in this area.

The article is published in the authors’ wording.

The paper is devoted to the analysis of the body of terms and terminological sources for further automation of constructing the thesaurus of a subject area, which is regarded as poetics in our work. Preliminary systematization of terminology with a linguistic and statistical approach forms the body of semantically related concepts to automate extraction of semantic relationships between terms that define the structure of the thesaurus of the specified field.

Traditional network architecture is inflexible and complicated. This observation has led to a paradigm shift towards software-defined networking (SDN), where network management level is separated from data forwarding level. This change was made possible by control plane transfer from the switching equipment to software modules that run on a dedicated server, called the controller (or network operating system), or network applications, that work with this controller. Methods of representation, storage and communication interfaces with network topology elements are the most important aspects of network operating systems available to SDN user because performance of some key controller modules is heavily dependent on internal representation of the network topology. Notably, firewall and routing modules are examples of such modules. This article describes the methods used for presentation and storage of network topologies, as well as interface to the corresponding Floodlight modules. An alternative algorithm has been suggested and developed for message exchange conveying network topology alterations between the controller and network applications. Proposed algorithm makes implementation of module alerting based on subscription to the relevant events. API for interaction between controller and network applications has been developed. This algorithm and API formed the base for Topology Tracker module capable to inform network applications about the changes that had occurred in the network topology and also stores compact representation of the network to speed up the interaction process.