TMPA-2015: agenda
12 November 2015
Conference Оpening
Software Engineering Education: The Messir Approach
Nicolas Guelfi, University of Luxembourg
Mastering the development of software having the required quality level is a complex task. Since 1968, the software engineering discipline has grown in order to offer theories, methods and tools to software engineers to tackle this complex task. The role of software engineering educators is to help the learners to acquire competencies in those theories, methods and tools to better master the production of quality products.
This talk will present the outcomes of an individual experience of 25 years of teaching software engineering and modeling in computer science programs at bachelor and master levels. A concrete educational software engineering method (Messir) and its environment (Excalibur) will be presented as one of the means to better educate our engineers to our discipline and be prepared for facing their future professional challenges.
Dr. Nicolas Guelfi is full professor at University of Luxembourg, LU since 1999. He obtained his PhD from the University of Paris XI (Orsay) on high level object-oriented specification formalisms for concurrent systems. Since 1994 he has been teaching software engineering at any academic level in universities (Paris XI (FR), Paris XII (FR), University of Luxembourg (LU), Polytechnic Schools (EPFL-Lausanne (CH)), or engineering schools (EPITA, ESI (FR)). He founded the Lassy laboratory (Laboratory for Advanced Software Systems) at University of Luxembourg which he directed for more than 10 years.
He has been involved in many research projects both at national, European or International level over the last 15 years and he managed more than 60 staff members at any qualification level on research and development projects. He has been member of the ERCIM (European Research Consortium in Mathematics and Informatics - http://www. ercim.eu) executive committee and he founded the ERCIM Working Group on Rapid Integration of Software Engineering Techniques (RISE) and the ERCIM Working Group on Software Engineering for Resilient Systems (SERENE). He is acting as expert for the courthouse concerning trials on conformance questions. The lawsuits involve projects whose budget range from thousands of euros to hundred of millions of euros. He has contributed to the field of software engineering as a researcher by publishing articles, editing books, acting as program chair or reviewing committee member. His research contribution has mainly focused on: requirements definition and specification using formal, semi-formal or informal methods; and system dependability and resiliency.
Static and dynamic program analysis
The dynamic analysis of executable code in ELF format based on static binary instrumentation (RU)
Mikhail Yermakov, ISP RAS
The application of static analysis to optimize the dynamic detection of race conditions (RU)
Yakov Roskoshnyy, Dmitry Tsitelov, Vitaly Trifanov, Roman Elizarov, Saint Petersburg State University of Information Technologies, Mechanics and Optics, Saint Petersburg
Lexical analysis of dynamically formed string expressions (RU)
Marina Polubelova, Semyon Grigorev, Saint Petersburg State University, Saint Petersburg
The application of parameterized hierarchy templates for automated program code defect-fixing (RU)
Artyom Aleksyuk, Vladimir Itsykson, Peter The Great Saint Petersburg Polytechnic University, Saint Petersburg
Automated testing of multi-thread data structures solutions linerializability (RU)
Anton Evdokimov, Dmitry Tsitelov, Roman Elizarov, Vitaly Trifanov, Saint Petersburg State University of Information Technologies, Mechanics and Optics, Saint Petersburg
Kotlin: from null dereference to smart casts (RU)
Mihael Glukhikh, JetBrains
Kotlin is a new open-source programming language developed by JetBrains. The main design goal was to create a completely Java compatible language that compiles as fast as Java but is safer and more concise. This presentation considers two language aspects which implementation uses static code analysis. It is the nullability analysis algorithm to protect from null dereference at runtime which improves safety, and the smart cast application algorithm based on type inference which improves conciousness.
Mikhail Glukhikh was born in 3 June 1978 in Leningrad. He was graduated from Ioffe Physical Technical School in 1995 and from Saint Petersburg State Polytechnical University in 2001 with master degree in informational technologies. He defended PhD thesis in 2007. Since 2002, Mikhail was a lead developer in Digitek Labs at computer system and software engineering department. From 2007 he is an associate professor at the same department. In 2013 he worked in Clausthal University of Technology as an invited researcher. In 2014, he worked at SPb office of Intel corporation, since March 2015, he participates in Kotlin language development at JetBrains company.
Trading systems
FPGA-based low latency sponsored access (RU)
Valery Florov, Pavel Garin, Pavel Smirnov, Maxim Metelkov, Exactpro
Reference test harness for algorithmic trading platforms (RU)
Victoria Leonchik, Alexey Sukhov, Eugene Ushakov, Iosif Itkin, Anna-Maria Lukina, Exactpro
The safety and stability of algorithmic trading software is an ongoing concern for exchanges, market participants and the society in general. Financial regulators worldwide are trying to create effective rules to prevent selfenforced market volatility and technology crashes caused by computer-aided trading. Specifying relevant requirements for dynamic software verification of algorithmic trading platforms remains is an on-going task. Yet, there has been little progress to date in locating efficient and commonly accepted approaches. This paper introduces a reference test harness implementation for algo trading platforms created by the authors.
Dynamic verification of input and output data streams for market data aggregation and quote dissemination systems (Ticker Plant) (RU)
Alyona Bulda, Maria Orlova, Exactpro
Market data aggregation and quote dissemination systems (Ticker Plants) are widely used across the electronic trading industry. A Ticker Plant is responsible for distributing information about multiple execution venues over a normalized protocol. This paper presents a dynamic verification approach for such systems. Based on a set of programs developed by the authors, it allows processing large data sets, including those collected during non-functional testing of trading platforms and using them in real-live production. The paper also outlines benefits and shortcomings of the selected approach for real-time and historical transactions analysis.
ClearTH: a tool for automated testing of post trade systems (RU)
Anna Toropova, Ekaterina Dimova, Iosif Itkin, Exactpro
Automated process of creating test scenarios for financial protocols and connectivity testing (RU)
Automated process of creating test scenarios for financial protocols and connectivity testing
13 November 2015
There are many theories of programming; this one seek to describe programs, programming languages and programming in a simple mathematical framework, based on a small set of high-school-level concepts of elementary set theory (sets and binary relations). It uses only three starting operations (union, restriction and composition) and covers the core concepts of programming as well as concurrency, non-determinism, control structures, correctness. From the theory’s definitions it is possible to deduce, as theorems, the axioms of classic theories such as those of Hoare and Kahn.
Bertrand Meyer is an academic, author, project manager and consultant in software engineering. He is Professor of Software Engineering at ETH Zurich and Innopolis University, and Chief Architect at Eiffel Software.
Verification
Implementing the MetaVCG approach in the C-light system (RU)
Alexei Promsky, Dmitry Kondtratyev, A.P. Ershov Institute of Informatics Systems, Novosibirsk
Among the problems that can confront a verification system developer, the addition of new axiomatic rules is of great interest. Not only theoretical properties of a Hoare logic (first of all, soundness and completeness) can be endangered by such activity, but also the recoding of verification condition generator (VCG) is required in practice. The error-prone process of manual reprogramming can compromise the very idea of verification system. Can we trust a program verified by (possibly) faulty system? While the self-verified system is still a challenge (though some steps towards it are already taken), as for its VCGpart, there is a method providing a greater level of reliability. In 1980, Moriconi and Schwartz represented the MetaVCG approach, regretfully abandoned. In this article, we would like to describe our efforts to implement this approach in the C-light system.
Expanding the meta-generation of correctness conditions by means of semantic markup (RU)
Dmitry Kondratyev, A.P. Ershov Institute of Informatics Systems, Novosibirsk
A Need To Specify and Verify Standard Functions (RU)
Nikolay Shilov, A.P. Ershov Institute of Informatics Systems, Novosibirsk
The problem of validation of standard mathematical functions and libraries is well-recognized by industrial and academic professional community but still is poorly understood by freshmen and inexperienced developers. The paper gives two examples (from author's pedagogical experience) when formal specification and verification of standard functions do help and are needed.
Formal methods in robotics (RU)
Dmitry Mordvinov, Yury Litvinov, Saint Petersburg State University, Saint Petersburg
The verification of functional programs by applying statechart diagrams construction method (RU)
Andrew Mironov, ISP RAS, Moscow
Towards a usable defect prediction tool: crossbreeding machine learning and heuristics (RU)
Vladimir Kovalenko, Galina Alperovich, JetBrains
A traditional supervised learning approach to defect prediction has been evaluated in numerous research papers. The biggest drawback of plain machine learning prediction models is their demand for labeled data. It sets a high restriction on applicability of defect prediction tools based on such models, and requires considerable time and resources to train the algorithms.
Building a defect prediction tool that can be used in realworld applications requires a simpler model that does not require as much human effort to train. The issue is confronted by heuristic approaches, such as the Google Bug Prediction Score, however studies show that the accuracy of heuristic models is often too low to justify their implementation.
We introduce a combined approach: by using a set of simple heuristics to identify bug fixes in version control and generating training instances based on bugfix data and language independent features, our combined algorithm performs significantly better than Google’s heuristic, while still remaining fully automated and language independent. As traditional classification quality metrics are not applicable in our case due to lack of precise labeling, we use an empirical method to compare relative prediction quality based on issue tracker activity
Building a defect prediction tool that can be used in realworld applications requires a simpler model that does not require as much human effort to train. The issue is confronted by heuristic approaches, such as the Google Bug Prediction Score, however studies show that the accuracy of heuristic models is often too low to justify their implementation.
We introduce a combined approach: by using a set of simple heuristics to identify bug fixes in version control and generating training instances based on bugfix data and language independent features, our combined algorithm performs significantly better than Google’s heuristic, while still remaining fully automated and language independent. As traditional classification quality metrics are not applicable in our case due to lack of precise labeling, we use an empirical method to compare relative prediction quality based on issue tracker activity
Standards and standartization in program engineering. Why would you care? (RU)
Nikolay Pakulin, ISP RAS, Moscow
14 November 2015
Automated testing: yesterday, today, tomorrow – the vectors of development
Anton Semyonchenko, DPI Solutions
Automation yesterday, today and tomorrow – are three independent engineering field of study, different on essence from each other.
Automation yesterday – first of all is using highly-specialized and very expensive so-called “record-play” UI tools. Nowadays automation engineer is a mixture of a developer, testing engineer and DevOps-specialists at once. So what’s the difference between today and tomorrow automation?
Testing and debugging tools
Multi-platform approach to reverse debugging of virtual machines (RU)
Pavel Dovgalyuk, Maria Klimushenkova, Denis Dmitriev and Vladimir Makarov, Novgorod State University
Multi-module application tracing in z/OS environment (RU)
Rostislav Efremov, Saint Petersburg State University, Saint Petersburg
Testing of a robot-programming environment (RU)
Dmitry Mordvinov, Yury Litvinov, Saint Petersburg State University, Saint Petersburg
Generation of Test Scenarios for Non Deterministic and Concurrent Telecommunication Applications (RU)
Pavel Drobintsev, Vsevolod Kotlyarov, Nikita Voinov, Peter The Great Saint Petersburg Polytechnic University, Saint Petersburg
The paper presents an approach to tests generation for industrial software systems with non deterministic and concurrent behavior. A brief overview of modern model driven test technologies is presented; benefits and problems of these approaches are highlighted. Specifics of concurrent and non deterministic behavior are analyzed to identify issues with such behavior testing. As result of the issues analysis usage of non-linear symbolic test scenarios for reducing test suite size is suggested and presented in examples. Based on the suggestion an approach for construction of non linear tests from linear ones is described with an example of industrial project. Results with description of main benefits for suggested approach are presented.
Information support system for autonomous spacecraft control macro-programming (RU)
Andrew Tyugashev, Anton Nasekin, Saint Petersburg State University of Information Technologies, Mechanics and Optics, Saint Petersburg
Conference closing remarks (RU)
TMPA-2015: Tools and Methods of Program Analysis Conference (RU)
About TMPA-2015. POLITECH (RU)