TMPA-2013: agenda
10 October 2013
About TMPA-2013 (RU)
Report
TMPA-2013: Opening (RU)
Verification
Verification of Parallel Programs – Current Stage and Perspectives (RU)
Yuri G. Karpov, Professor, Head of Department of Distributed Computing and Networking of the St. Petersburg State Polytechnic University Technical Cybernetics School (about)
Dynamic Verification of Hybrid Systems (RU)
Pakulin, N., Institute for System Programming, ISP RAS
In the recent decade we face aggressive replacement of analog control loops with digital ones. Even for critical systems there are ongoing projects for digital control: “Smart Grids” in power industry, “Integrated Modular Avionics” in aerospace, “Smart Fabrics” in manufacturing, etc. Introduction of large scale digital control channels raises the risks of faults that might result in heavy losses. Those risks call for new methods of analysis and verification, including modeling hybrid systems and model-based verification. The paper overviews a number of existing approaches to verification of hybrid systems and introduces architecture of a test bed for dynamic verification of models of hybrid systems.
UPPAAL-based software-defined network verification (RU)
Podymov, V., Popesko, U., Moscow State University
A lot of efforts were made in the last few years in the area of software-defined networks (SDN) - a special kind of computer networks in which the switching device control is fully centralized. This paper investigates the problems of formal description and verification of SDN as a real-time system. We provide a UML-based description of SDN, using the UML diagram editor Dia. To verify real-time properties of SDN, we use a well-known model-checking tool UPPAAL. The main result of the research is an approach for SDN verification, based on translation of SDN description into network of timed automata. Translation correctness is formalized and proved. A number of experiments were done to show that the approach can be used to verify real-time properties of SDN specified as TCTL formulae.
Construction and verification of PLC programs by LTL specification (RU)
Kuzmin, Е., Ryabukhin, D., Shipov, А Yaroslavl State University
The article proposes an approach to construction and verification of PLC ST-programs for discrete problems. The linear-time temporal logic LTL is used for the specification of the program behavior. Programming is carried out in the ST (Structured Text) language, according to the LTL-specification. The correctness analysis of the LTL-specification is performed by Cadence SMV, a symbolic model checking tool. A new approach to programming and verification of PLC ST-programs is illustrated. For each discrete problem, we propose creating an ST-program, its LTL-specification, and an SMV-model.
On the Road to Technology of Developing the Means of Deductive Program Verification (RU)
Anureyev, I., A.P.Ershov Institute of Informatics Systems
Verification of Distributed Automated Programs Using the Spin Tool (RU)
Lukin, M., Shalyto, А. , St. Petersburg National Research University of Information Technologies, Mechanics and Optics
The Efficient Universal Sleptsov Net (RU)
Zaitsev D., Professor, International Humanitarian University, Odessa, Ukraine
Hardware track
Correctness checking of HDL-model behavior based on runtime trace matching (RU)
Ivannikov, V.P., Kamkin, A.S., Chupilko, M.M., Institute for System Programming, ISP RAS
Correctness checking of HDL-model behavior is an integral part of runtime verification of hardware. As a rule, it is based on comparing of HDL-model behavior and reference model behavior, developed in high-level programming languages. Being verified, both models are stimulated with the same input sequence; their output traces are caught and matched. Due to the abstractness of the reference model, the matching is not a trivial task as event sequences can be different and some events of one trace may miss in the other one. A methodology of runtime trace matching for hardware models of different abstraction levels is suggested in this paper. The methodology has been successfully applied to a number of industrial projects of unit-level microprocessor verification.
The Usage of Check Points for SystemC Program Verification (RU)
Shipin, А.А., Sokolov, V.А., Chaliy, D.U., Yaroslavl State University
Unified High Level Model of Software and Hardware System for Verifying Functional Reliability (RU)
Frenkel, S.L., Zakharov, V.N., Ushakov, V.G., Institute of Informatics Problems, RAS; Moscow State University
The Specifics of Developing Software for Linux Controllers (RU)
Smirnov, М., Olonichev, V., Staroverov, B. , Kostroma State Technological University
11 October 2013
Testing
Technical Solutions and Non-Technical Challenges of Test Automation (RU)
Alexander K. Petrenko, Professor, Head of Programming Technologies Department, Institute for System Programming ISP RAS
On improving the statistical method used to access the completeness of tests for software systems and discrete devices (RU)
Basok, B., Grechin, A., Moscow State Technical University of Radioengineering, Electronics and Automation
This paper describes a statistical method for test completeness verification. The method is based on analyzing programs and mathematical models of discrete devices with introduced defects. It is proposed in the paper that the method allows largely reducing the time it takes to evaluate the tests by introducing multiple defects on the one hand, and, by using the results of the analysis of tests performed against the object under test and its individual components, on the other hand. The paper provides experimental data confirming the effectiveness of the proposed approaches.
The Analysis of Performance of Genode Micro-core Environment Network Subsystem (RU)
Sartakov, V., Tarasikov, Aksys labs
An Approach to Verification of Correctness of Data Migration between DBMS Using Cryptographic Hash Functions (RU)
Zhuravlev, М., Polozov, V. , St. Petersburg State University
Automation of Conformance Testing of TLS Transport Layer Security Protocol (RU)
Nikeshin, А., Pakulin, N., Shnitman, V., Institute for System Programming, ISP RAS
Applying OLAP and MapReduce Technologies for Performance Testing Results Processing (RU)
Senov, А , Kostroma State Technological University
Trading systems
Special features of testing tools applicable for use in trading systems production (RU)
Matveeva, А., Antonov, N., Itkin, I, Innovative Trading Systems, LLC, Kostroma State Technological University, Exactpro Systems, LLC
The paper examines basic requirements for tools developed for verification of correct work of electronic trading systems by applying High Volume Automated Testing (HiVAT) methods and analyzes the applicability of such tools during production operation of trading systems.
Compatibility testing of clients' protocol connectivity to exchange and broker systems (RU)
Alexeenko, А., Protsenko, P., Matveeva, А., Itkin, I., Sharov D., Innovative Trading Systems, LLC, Exactpro Systems LLC
The software development life cycle for exchanges and brokers, in addition to verification of functional and technical system characteristics, includes a mandatory Integration Testing stage with the Client Certification part. The goal of this stage is to ensure the compatibility of automated trading systems connected to an exchange or broker via financial industry protocols (such as FIX/FAST, ITCH or specialized binary access interfaces). This paper presents a unique tool developed for verifying the compatibility of trading systems. One distinctive feature of the tool is a unified means of supporting multiple protocols. The case study provides examples of the tool usage by trading participants for self-certification and during large migrations of trading platforms.
Usage of exchange simulators and test exchanges as tools for Ticker Plant systems testing (RU)
Buyanova, О., Zverev, А., Bulda, А., Innovative Trading Systems, LLC, Kostroma State Technological University, Exactpro Systems, LLC
Ticker Plant systems are widely used in modern day trading. They allow collecting in real-time quotes from several markets, present the data in a unified format, and disseminate it electronically depending on requests and goals of external clients, traders. This paper presents a view on the possibility of using market simulators for testing such systems. A set of main functional and non-functional test scenarios required to control the quality of quote dissemination has been identified. A comparison of market simulators and real test markets has been presented.
High performance load generator for automated trading systems testing (RU)
Guriev, D., Gai, M., Itkin, I., Terentiev, A., Innovative Trading Systems, LLC
The growing volume of orders generated by HFT (high-frequency trading) systems has posed a challenge of conducting exchange and brokerage systems testing in production-like environments. Specialized testing tools are used to ensure quality of high load trading systems with high availability. The main requirement for such tools is that they should be capable of creating realistic, high loads using limited hardware infrastructure. This article describes a load injection tool developed for testing automated trading systems and an approach that ensures high performance.
Model Based Testing Approach for Verification of Exchange Surveillance Systems (RU)
Pryadkina N., Kryukov, A , Kostroma State Technological University
Testing of Graphical Interface of Trading Terminals in High Frequency Trading Conditions (RU)
Bobrov, I., Zverev, A, Innovative Trading Systems, LLC
Electronic Trading Platforms: Unconventional Methods of Software Testing (RU)
Panel discussion
12 October 2013
Analysis of programs
Mathematical Aspects of Program Obfuscation (RU)
Vladimir A. Zakharov, Associate Professor of Mathematical Cybernetics Department, Head of Laboratory of Mathematical Problems of Computer Security, Faculty of Computational Mathematics and Cybernetics, Moscow State University (MSU) (about)
Dynamic data race detection in Java-programs using synchronization contracts (RU)
Tsytelov, D., Trifanov, V., Devexperts LLC, St. Petersburg State University
Data race occurs in a multi-threaded program when several threads simultaneously access the same memory location and at least one of them is a write access. Data races can damage global data structures and it's hard to detect them manually, so research in the area of automatic race detection methods has been carried out for more than 20 years. This article covers aspects of performance and precision of dynamic race detection in Java programs and proposes the idea of lowering the overheads of dynamic analysis using synchronization contracts. Synchronization contracts are mainly based on specifying pairs of methods, that being called from different threads provide synchronization between these threads. Contracts serve for exclusion of application's code parts that are not interesting from race detection perspective, for example - external libraries. In this paper we describe contracts specification language and some implementation details and discuss advantages and restrictions of our approach.
Detection of incorrect pointer dereferences for C/C++ programs using static code analysis and logical inference (RU)
Vert, Т., Krikun, Т., Glukhih, М., St. Petersburg State Polytechnic University, Clausthal Technical University
This article considers a method for an increase of static code analysis precision. The method extends classic code analysis algorithm with dependency analysis. For this purpose, during abstract interpretation information about statically known values should be extracted as well as dependencies between unknown values. Dependencies can be represented with first-order logic predicates. Such a method allows using of external logical inference tools to prove truth or falsehood of branch conditions and of error occurrence conditions. The main focus is oriented to pointer analysis logic and incorrect dereference detection rules. A prototype is implemented and results of efficiency evaluation are provided. The prototype uses Microsoft Z3 Solver as a logical inference tool. A significant precision increase is shown, ways for performance boosting are suggested.
Generating unit tests using static analysis and contracts (RU)
Andrianova, А., Itsykson, V., St. Petersburg State Polytechnic University
Software Quality Assurance is one of the main challenges of software engineering. One of the ways to improve software quality is automated synthesis of unit tests. This paper describes a technology of automated unit tests creation combining the “white” and “black” box approaches. This allows using information extracted from the source code of the program and using partial specifications in the form of contracts to create test oracles and distribute the test parameters across the domain of definition to ensure the test coverage of program paths. The developed approach was implemented as a tool that analyzes Java-based programs and generates test cases for class methods in JUnit format, using CoFoJa to specify the contracts. Testing of the designed tool performed on a number of test objects has proven that the approach is efficient.
OOP Class Diagrams: Formation and Analysis (RU)
Bui, D., Kompan, S., Taras Shevchenko National University of Kyiv
