One of the most serious problems when doing program analyses is dealing with function calls. While function inlining is the traditional approach to this problem, it nonetheless suffers from the increase in analysis complexity due to the state space explosion. Craig interpolation has been successfully used in recent years in the context of bounded model checking to do function summarization which allows one to replace the complete function body with its succinct summary and, therefore, reduce the complexity. Unfortunately this technique can be applied only to a pair of unsatisfiable formulae.

In this work-in-progress paper we present an approach to function summarization based on Craig interpolation that overcomes its limitation by using random model sampling. It captures interesting input/output relations, strengthening satisfiable formulae into unsatisfiable ones and thus allowing the use of Craig interpolation. Preliminary experiments show the applicability of this approach; in our future work we plan to do a full evaluation on real-world examples.

We study the verification of the soundness property for workflow nets extended with resources. A workflow is sound if it terminates properly (no deadlocks and livelocks are possible). A class of resource-constrained workflow nets (RCWF-nets) is considered, where resources can be used by a process instance, but cannot be created or spent. Two sound RCWF-nets using the same set of resources can be put in parallel. This parallel composition may in some cases produce additional deadlocks. A problem of deadlock avoidance in parallel workflows is studied, some methods of deadlock search and control are presented.

The paper presents an approach to formal verification of multi-agent data analysis algorithms for ontology population. The system agents correspond to information items of the input data and the rule of ontology population and data processing. They determine values of information objects obtained at the preliminary phase of the analysis. The agents working in parallel check the syntactic and semantic consistency of tuples of information items. Since the agents operate in parallel, it is necessary to verify some important properties of the system related to it, such as the property that the controller agent correctly determines the system termination. In our approach, the model checking tool SPIN is used. The protocols of agents are written in Promela language (the input language of the tool) and the properties of the multi-agent data analysis system are expressed in the liner time logic LTL. We carried out several experiments to check this model in various modes of the tool and various numbers of agents.

The paper presents two approaches to debugging the application model behavior scenarios: semi-automatic and automatic. The first approach allows a user to automatize the process of finding the place in a concrete behavioral scenario that is suspicious of being a cause of an error. The second approach allows, in a single cycle of the analysis, to automatically identify not only the place, but also possible causes of errors in a given set of generated behavioral symbolic scenarios.

The designing of network update algorithms is urgent for the development of SDN control software. A particular case of Network Update Problem is that of restoring seamlessly a given network configuration after some packet forwarding rules have been disabled (say, at the expiry of their time-outs). We study this problem in the framework of a formal model of SDN, develop correct and safe network recovering algorithms, and show that in general case there is no way to restore network configuration seamlessly without referring to priorities of packet forwarding rules.

As opposed to traditional testing, the deductive verification represents a formal way to examine the program correctness. But what about the correctness of the verification system itself? The theoretical foundations of Hoare’s logic were examined in classical works, and some soundness/completeness theorems are well-known. However, we practically are not aware of implementations of those theoretical methods which were subjected to anything more than testing. In other words, our ultimate goal is a verification system which can be self-applicable (at least partially). In our recent studies we addressed ourselves to the metageneration approach in order to make such a task more feasible.

The automated test generation has received a lot of attention in the last decades as it is one of possible solutions to software testing inherent problems: the need to write tests and providing test coverage in presence of human factor. The most promising technique of generating a test automatically is the dynamic symbolic execution assisted by an automated constraint solver, e. g., an SMT-solver. This process is very similar to the bounded model checking, which also has to deal with generating models from a source code, asserting logic properties in it and process the returned model. This paper describes a prototype unit test generator for C based on a working bounded model checker called Borealis and shows that these two techniques are very similar and can be easily implemented by using the same basic components. The prototype test generator was sampled on a number of examples and showed good results in terms of test coverage and test excessiveness.

The standard language of message sequence charts MSC is intended to describe scenarios of object interaction. Due to their expressiveness and simplicity MSC diagrams are widely used in practice at all stages of system design and development. In particular, the MSC language is used for describing communication behavior in distributed systems and communication protocols. In this paper the method for analysis and verification of MSC and HMSC diagrams is considered. The method is based on the translation of (H)MSC into coloured Petri nets. The translation algorithms cover most standard elements of the MSC including data concepts. Size estimates of the CPN which is the result of the translation are given. Properties of the resulting CPN are analyzed and verified by using the known system CPN Tools and the CPN verifier based on the known tool SPIN. The translation method has been demonstrated by the example.

Like other software artefacts, DSMLs evolve in time. When a DSML changes, instance models might no longer conform to the new DSML metamodel and hence cannot be manipulated with a modelling tool. Therefore, a need for models migration to a new version of metamodel arises. Today, various approaches to this problem exist - from entirely manual to mostly automated. This paper describes a hybrid approach to model migration implemented in DSM platform QReal, which is being developed by the research group of Software Engineering Chair of St. Petersburg State University. That DSM platform implies some specific requirements, such as the support of metamodel interpretation and metamodeling “on the fly” modes. The presented approach realizes model migration when using one of those specific features. 

The algorithm of pattern mining from sequences of system calls is described. Patterns are used for process identification or establishing the fact that some sequence of system calls was produced by the process which was used in pattern extraction. Existing algorithms are computationaly more complex or reveals high false positive runs in experiments in comparision with an automaton building algorithm. Our algorithm is less complex and more precise in comparision with the classical N-gram algorithm. Performance tests reveal that our kernel monitor does not significatly slow down the processing of the operating system. After 20 minutes of learning the algorithm is able to identify any thread of any process with 85% precision. Program identification based on behavior is used for anomaly detection of malicious activities in system.

Complex information systems are often implemented by using more than one programming language. Sometimes this variety takes a form of one host and one or few string-embedded languages. Textual representation of clauses in a string-embedded language is built at run time by a host program and then analyzed, compiled or interpreted by a dedicated runtime component (database, web browser etc.) Most general-purpose programming languages may play the role of the host; one of the most evident examples of the string-embedded language is the dynamic SQL which was specified in ISO SQL standard and is supported by the majority of DBMS. Standard IDE functionality such as code completion or syntax highlighting can really helps the developers who use this technique. There are several tools providing this functionality, but they all process only one concrete string-embedded language and cannot be easily extended for supporting another language. We present a platform which allows to easily create tools for string-embedded language processing.

The paper presents an approach to effort reduction in developing test suites for industrial software products based on the incremental technology. The main problems to be solved by the incremental technology are full automation design of test scenarios and significant reducing of test explosion. The proposed approach provides solutions to the mentioned problems through joint co-working of a designer and a customer, through the integration of symbolic verification with the automatic generation of test suites; through the usage of an efficient technology with the toolset VRS/TAT.

This paper describes the software for graph storage, analysis and visualization. The article presents a comparative analysis of existing software for analysis and visualization of graphs, describes the overall architecture of application and basic principles of construction and operation of the main modules. Furthermore, a description of the developed graph storage oriented to storage and processing of large-scale graphs is presented. The developed algorithm for finding communities and implemented algorithms of autolayouts of graphs are the main functionality of the product. The main advantage of the developed software is high speed processing of large size networks (up to millions of nodes and links). Moreover, the proposed graph storage architecture is unique and has no analogues. The developed approaches and algorithms are optimized for operating with big graphs and have high productivity.

The report presents a new system focused on the creation of specialized databases and database management systems. Based on the analysis of various NoSQL solutions there have been formulated some principles of such a system. The main features of the approach are: a) the infrastructure provides a flexible system of type definitions which allow to create data structures based on different paradigms; b) different forms of structured data support and mapping to the file system are used in the infrastructure. Experiments were provided with the implementation of RDF graphs, relational tables, name tables, object-relational mappings. The approach allows to solve some problems of technologies creation for work with Big Data.

The workshop of the Nonlinear Dynamics scientific-educational center continued its work in 2014, focusing on methods of the dynamical system analysis and studies of their behavior. More than 30 talks in the field of scientific-educational center research have been made this year. The talk topics included numerical analysis of traveling waves in the Fisher–KPP equation with delay and simulations of the twophase heat distribution problem using heterogeneous computing architectures. In a number of talks normal and quasi-normal forms of differential equations with several delays were derived and studied, also one talk considered a problem of optimal control of a telescopic manipulator. The selected talk abstracts are presented in this issue of the journal.