TMPA-2014: agenda

14 November 2014

Vesti Kostroma about TMPA-2014 (RU)

Moscow Exchange

Current Challenges in the Area of Efficient Parallel Algorithms and Data Structure Development

Vitaly Trifanov, Dmitry Tsitelov, Devexperts LLC, Saint Petersburg

New Exchange Platform NP RTS: Goals, Architecture and Risk Management

Mikhail Vyugin, NP RTS

Introduction into Fault-tolerant Distributed Algorithms and their Modeling (Part 1) (EN)

Josef Widder, Vienna University of Technology (about)

Fault-tolerant distributed algorithms provide a system designer with a mechanism for constructing reliable computing systems. In this talk, we will introduce basic notions such as timing assumptions, fault assumptions, and classic problems in this area. By reviewing classic paper & pencil correctness arguments, we motivate the use of automated verification methods such as model checking.
The first step towards automated verification is adequate modeling. Thus, in the second part of the talk, we explain how to encode the semantics of fault-tolerant distributed algorithms in Promela, the input language of the Spin model checker.

Introduction into Fault-tolerant Distributed Algorithms and their Modeling (Part 2) (EN)

Josef Widder, Vienna University of Technology (about)

A runtime verification system for Software Defined Networks

Victor Altukhov, Eugene Chemeritskiy, Vladislav Podymov and Vladimir Zakharov, Lomonosov Moscow State University, Moscow

We present a software toolset VERMONT (VERifying MONiTor) for runtime checking the consistency of Software Defined Network (SDN) configurations with formally specified invariants of Packet Forwarding Policies (PFPs). One of the main task of network engineering is to provide such a loading of SDN switches with forwarding rules as to guarantee its compliance with the PFP. VERMONT provides some automation to the solution of this task. Being installed in line with the control plane it 1) observes state changes of a network by intercepting the exchange of messages and commands between network switches and SDN controller, 2) builds an adequate formal model of a whole network, and 3) checks every event, such as installation, deletion, or modification of rules, port and switch up and down events, against a set of PFP invariants. Before retransmitting a network updating command to a switch VERMONT anticipates the result of its execution and checks the requirements of PFP. If a violation of some PFP invariant is detected then VERMONT blocks the change, alerts a network administrator, and gives some additional information to elucidate a possible source of an error. In this paper we discuss both mathematical and engineering issues of our toolset. We begin with defining a formal model of SDN and a formal language for PFP specification. After presenting the main algorithms used in VERMONT for SDN model building, model checking, and model modification, we describe the structure of VERMONT and the functionality of its components. Finally, we demonstrate the results of our experiments on the application of VERMONT to a real-life network.

On a Method of Programmatically Configurable Networks Balancing

Michael Nikitinsky, Dmitry Chalyy, Yaroslavl State University, Energia-info LLC, Yaroslavl

A Methodology of Reproducible Research of Simulation Test Models and Communication Protocols Implementations

Dmitry Chalyy, Yaroslavl State University, Yaroslavl

Real Time Systems Profiling

Denis Deryugin, Saint Petersburg State University, Saint Petersburg

On Contemporaneous Application of Model Driven Development and Model Based Checking Methods

Sergey Staroletov, Altai State Technical University, Barnaul

Test Automation of a Backup System

Vadim Zherder and Tatiana Ulyanina Mockow Exchange, National Research Nuclear University MEPhI, Moscow

Testing of a Risk Control System Implementation for High-Load Exchange and Brokerage Systems

Alyona Bulda, Maxim Rudovsky and Alexey Zverev Exactpro Systems, Kostroma, Моscow

Trading Day Logs Replay Limitations and Test Tools Applicability

Pavel Protsenko, Anna-Mariia Lukina, Iosif Itkin, Anna Khristenok, Andrey Alekseenko and Tatiana Pavlyuk, Exactpro Systems, London, Кostroma, Моscow, Оbninsk

This paper is an experience report on replaying full trading day production log files for dynamic verification of securities exchange matching engines. Three types of test automation tools developed in-house are described along with their characteristics. The paper analyzes various approaches to reproduce processes and scenarios observed in the systems during their production usage. The applicability and limitations of these approaches are also considered. The authors point out that for most complex distributed real-time trading systems it is extremely difficult to obtain an identical behavior using production logs replay via external gateways. It might be possible to achieve this by implementing additional instrumentation inside the exchange system’s core. The authors assume however that such an intrusion has limited value and should not be prioritized over other, more appropriate, test design methods for testing such systems.

Integration Test Automation for FIX Protocol Data Exchange Modules

Vsevolod Brekelov, Ilya Barigin, Egor Borisov Devexperts LLC, Saint Petersburg

Modelling of Exchange Trading Participants Behavior Test Scenarios

Elena Gerasimova, Rostislav Yavorsky, Higher School of Economics, Moscow

How We Test Software at Exactpro

Iosif Itkin, Exactpro Systems

On Modelling of Coordinated Behavior of PLC Sensors (RU)

Egor Kuzmin, Dmitriy Ryabukhin and Valery Sokolov, Yaroslavl State University, Yaroslavl

Approaches to the Fragmentation of a Paravirtualization System (RU)

Vasily Sartakov, Nikolay Golikov, ksys labs, Odintsovo

Automated Testing of Engineering Applications by Using AutoIt (RU)

Alyona Kiselyva, ICAD RAS, Moscow

The Analysis of Test Scenario Coverage for a UCM-Model (RU)

Igor Nikiforov, Pavel Drobintsev, Vsevolod Kotlyarov, Nikita Voinov, Saint Petersburg State Polytechnic University, Saint Petersburg

Test Set Generation Based on a Management Stream Model (RU)

Pavel Drobintsev, Vsevolod Kotlyarov, Igor Nikiforov, Nikita Voinov, Saint Petersburg State Polytechnic University, Saint Petersburg

15 November 2014

Generalized Tabular LL-Analysis (RU)

Anastasiia Ragozina, Semyon Grigorev, Saint Petersburg State University, JetBrains, Saint Petersburg

Extended High-Level C-Compatible Memory Model with Limited Low-Level Pointer Cast Support for Jessie Intermediate Language (RU)

Mikhail Mandrykin and Alexey Khoroshilov, ISP RAS, Moscow

The paper presents an intermediate language which is intended to serve as a target analyzable language for verificationof real-world production GNU C programs (Linux kernel modules). The language represents an extension of the existing intermediate language used by the JESSIE plugin for the FRAMA-C static analysis framework. It is compatible with the C semantics of arrays, initially supports hierarchical (prefix) pointer casts and discriminated unions, and extended with limited support for low-level pointer casts. The approaches to translation of the original C code into the intermediate language and translation of the intermediate language into the input language of the Why3 deductive verification platform are explained by examples. The examples illustrate the expressive power of the extended intermediate language and efficiency of the resulting axiomatic representation

Alias Calculus for a Simple Imperative Language with Decidable Pointer Arithmetic (RU)

Nikolay Shilov, Alexander Vorontsov, Aizhan Satekbayeva, Nazarbayev University, Kazakhstan

"Alias calculus was proposed by Bertrand Meyer in 2011 for a toy programming language with single data type for abstract pointers. The original calculus is set-based formalism insensitive to control flow; it is a set of syntax-driven rules to compute an upper approximation aft(S,P) for aliasing after execution of a program P for a given initial aliasing S; this calculus guarantees partial correctness of the assertion {S}P{aft(S,P)}. The primary purpose of our paper is to present a variant of alias calculus for more realistic programming language with static and dynamic memory, with types for regular data as well as for decidable pointer arithmetic. Our variant is insensitive to control flow (as the original calculus by B. Meyer), but is calculus is equation-based (in contrast to the original calculus)."

A Method of Building Extended Finite State Machines According to HDL-Description Based on Static Code Analysis (RU)

Sergey Smolov, Alexander Kamkin, ISP RAS, Moscow

AADL Module Analysis by means of Graphical Representation (RU)

Alexander Strakh, ISP RAS, Moscow

Lightweight Static Analysis for Data Race Detection in Operating System Kernels (RU)

Pavel Andrianov, Alexey Khoroshilov, Vadim Mutilin, ISP RAS, Moscow

The paper presents an approach to lightweight static data race detection. It takes into account the specifics of operating system kernels, such as complex parallelism and kernel specifics synchronization mechanisms. The method is based on the Lockset one, but it implements two heuristics that are aimed to reduce amount of false alarms: a memory model and a model of parallelism. The main target of our research and evaluation is operating system kernels but the approach can be applied to the other programs as well.

Static Analysis of Transactions Management in Applications for Java EE Platform (RU)

Ivan Grachev, Andrey Solovev, Vladimir State University, Vladimir

Parametrized Model Checking of Fault-tolerant Distributed Algorithms by Abstraction (Part 1) (RU)

Igor Konnov, Vienna University of Technology

We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assumed maximum number of faults. At the center of our technique is a parametric interval abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters. Using PIA for both data abstraction and a new form of counter abstraction, we reduce the parameterized problem to finite-state model checking. We demonstrate the practical feasibility of our method by verifying safety and liveness of several fault-tolerant broadcasting algorithms, and finding counter examples in the case where there are more faults than the FTDA was designed for. Further, we show how bounded model checking can be used as a complete verification method for reachability properties, which can handle more involved FTDAs.

Parametrized Model Checking of Fault-tolerant Distributed Algorithms by Abstraction (Part 2) (RU)

Igor Konnov, Vienna University of Technology

The Agile-Tester: a Professional or a Craftsman? (RU)

Andrey Konushin, RSTQB, Vladimir

Automated Software Development and Verification Technologies in the Aerospace Industry (RU)

Andrey Tyugashev, SSAU, Samara

A Method of Reducing Computational Complexity in Verification of Programming Probability Models (RU)

Andrew Mironov, Sergei Frenkel, IPI RAS, Moscow

Verification of 800 Automata-Based Programs Built by means of Genetic Programming (RU)

Michael Lukin, Maxim Buzdalov and Anatoly Shalyto Saint Petersburg State University of Information Technologies, Mechanics and Optics, Saint Petersburg