Manuel Mazzara
Andrei Voronkov
(Eds.)
123
LNCS 9609
10th International Andrei Ershov Informatics Conference, PSI 2015
in Memory of Helmut Veith
Kazan and Innopolis, Russia, August 24–27, 2015
Revised Selected Papers
Perspectives of
System Informatics
Lecture Notes in Computer Science 9609
Commenced Publication in 1973
Founding and Former Series Editors:
Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen
Editorial Board
David Hutchison
Lancaster University, Lancaster, UK
Takeo Kanade
Carnegie Mellon University, Pittsburgh, PA, USA
Josef Kittler
University of Surrey, Guildford, UK
Jon M. Kleinberg
Cornell University, Ithaca, NY, USA
Friedemann Mattern
ETH Zurich, Zürich, Switzerland
John C. Mitchell
Stanford University, Stanford, CA, USA
Moni Naor
Weizmann Institute of Science, Rehovot, Israel
C. Pandu Rangan
Indian Institute of Technology, Madras, India
Bernhard Steffen
TU Dor tmund University, Dortmund, Germany
Demetri Terzopoulos
University of California, Los Angeles, CA, USA
Doug Tygar
University of California, Berkeley, CA, USA
Gerhard Weikum
Max Planck Institute for Informatics, Saarbrücken, Germany
More information about this series at http://www.springer.com/series/7407
Manuel Mazzara
Andrei Voronkov (Eds.)
Perspectives of
System Informatics
10th International Andrei Ershov Informatics Conference, PSI 2015
in Memory of Helmut Veith
Kazan and Innopolis, Russia, August 2427, 2015
Revised Selected Papers
123
Editors
Manuel Mazzara
Innopolis University
Innopolis
Russia
Andrei Voronkov
The University of Manchester
Manchester
UK
ISSN 0302-9743 ISSN 1611-3349 (electronic)
Lecture Notes in Computer Science
ISBN 978-3-319-41578-9 ISBN 978-3-319-41579-6 (eBook)
DOI 10.1007/978-3-319-41579-6
Library of Congress Control Number: 2016942778
LNCS Sublibrary: SL1 Theoretical Computer Science and General Issues
© Springer International Publishing Switzerland 2016
This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the
material is concerned, specically the rights of translation, reprinting, reuse of illustrations, recitation,
broadcasting, reproduction on microlms or in any other physical way, and transmission or information
storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now
known or hereafter developed.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication
does not imply, even in the absence of a specic statement, that such names are exempt from the relevant
protective laws and regulations and therefore free for general use.
The publisher, the authors and the editors are safe to assume that the advice and information in this book are
believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors
give a warranty, express or implied, with respect to the material contained herein or for any errors or
omissions that may have been made.
Printed on acid-free paper
This Springer imprint is published by Springer Nature
The registered company is Springer International Publishing AG Switzerland
Preface
To the memory of Helmut Veith
The Ershov Informatics Conference (the PSI Conferenc e Series) is the premier
international forum in Russia for research and applications in computer, software, and
information sciences. The conference brings together academic and industrial
researchers, developers, and users to discuss the most recent topics in the eld. PSI
provides an ideal venue for setting up research collaborations between the rapidly
growing Russian informatics community and its international counterparts, as well as
between established scientists and younger researchers.
The 1 0th edition of the conference was held during August 2425, 2015, in Kazan
and Innopolis City, in Tatarstan (Russian Federation). In particular, the rst and last
day of the conference were hosted in the new ultramodern complex of Innopolis City
(http://www.innopolis.com/main/) while the core days were held at the Korston Con-
ference Center, in downtown Kazan.
This volume contains a selection of papers presented at PSI 2015. It includes two
invited papers and 23 papers selected out of 56 submissions. We wish to thank all those
involved in the organization as well as the Program Committee members and the
anonymous reviewers. Without them and all their hard work, the realization of such an
ambitious project would not have been possible.
During the preparation of this volume, a dramatic event stunned us and the members
of the international scientic community, in Austria and worldwide. Helmut Veith,
whose invited paper is published in this volume, died tragically on March 12, 2016.
This volume is dedicated to the memory of a bright colleague and dear friend.
April 2016 Manuel Mazzara
Andrei Voronkov
Organization
Program Committee
Farhad Arbab CWI and Leiden University, The Netherlands
David Aspinall University of Edinburgh, UK
Marcello M. Bersani Politecnico di Milano, Italy
Eike Best Universität Oldenburg, Germany
Nikolaj Bjørner Microsoft Research, USA
Nail Bukharaev Kazan Federal University, Russia
Andrea Calì University of London, Birkbeck College, UK
Mauro Caporuscio Politecnico di Milano, Italy
Néstor Cataño Madeira Interactive Technologies Institute, Portugal
Gabriel Ciobanu Romanian Academy, Iasi, Rom ania
Volker Diekert University of Stuttgart, Germany
Salvatore Distefano University of Mess ina, Italy
Nicola Dragoni Technical University of Denmark, Denmark
Schahram Dustdar TU Wien, Austria
Dieter Fensel University of Innsbruck, Austria
Carlo A. Furia ETH Zurich, Switzerland
Carlo Ghezzi Politecnico di Milano, Italy
Sergei Gorlatch University of Münster, Germany
Jan Fr iso Groote Eindhoven University of Technology, The Netherlands
Arie Gurnkel Carnegie Mellon University, USA
Cliff Jones Newcastle University, UK
Joost-Pieter Katoen RWTH Aachen University, Germany
Konstantin Korovin The University of Manchester, UK
Maciej Koutny Newcastle University, UK
Laura Kovacs Chalmers University of Technology, Sweden
Gregory Kucherov CNRS/LIGM, France
Johan Lilius A bo Akademi University, Finland
Anthony Widjaja Lin Yale-NUS College, USA
Zhiming Liu Birmingham City University, UK
Jan Madse n Technical University of Denmark
Rupak Majumdar MPI-SWS, Germany
Manuel Mazzara Innopolis University, Russia
Klaus Meer TU Cottbu s, Germany
Hernan Melgratti Universidad de Buenos Aires, Argentina
Bertrand Meyer ETH Zurich, Switzerland
Torben Mogensen DIKU, Denmark
Peter Mosses Swansea University, UK
Martin Nordio ETH Zurich, Switzerland
Jose R. Parama University of A Coruna, Spain
Wojciech Penczek ICS PAS and Siedlce University, Poland
Peter Pepper Technische Universität Berlin, Germany
Alexander K. Petrenko Russian Academy of Sciences, Russia
Paul Pettersson Mälardalen University, Sweden
Nadia Polikarpova ETH Zürich, Switzerland
Qiang Qu Innopolis University, Russia
Wolfgang Reisig Humboldt-Universitä t zu Berlin, Germany
Andrey Rybalchenko Microsoft Research, UK
Davide Sangiorgi University of Bologna, Italy
Klaus-Dieter Schewe Software Competence Center Hagenberg, Germany
Natalia Sidorova Technische Universiteit Eindhoven, The Netherlands
Giancarlo Succi Free University of Bozen-Bolzano, Italy
Max Talanov Kazan Federal University, Russsia
Alexander Tormasov Innopolis University, Russia
Mark Trakhtenbrot Holon Institute of Technology, Israel
Kishor Trivedi Duke University, USA
Andrei Voronkov The University of Manchester, Chalmers University of
Technology, and EasyChair, UK/Sweden
Domagoj Vrgoc Center for Semantic Web Research, Chile
Sergey Zykov Higher School of Economics, Russia
Additional Reviewers
Akbar, Zaenal
Barylska, Kamila
Dan, Li
Enoiu, Eduard Paul
Fensel, Anna
Fleischhack, Hans
Freitas, Leo
Haidl, Michael
Kahsai, Temesghen
Keshishzadeh, Sarmen
Lorenzen, Florian
Marinescu, Raluca
Mezzetti, Nicola
Moelle, Andre
Noll, Thomas
Penabad, Miguel R.
Prüfer, Robert
Rasch, Ari
Seghir, Mohamed Nassim
Steggles, Jason
Szreter, Maciej
Veselov, Alexander
VIII Organization
Contents
Quantitative Analysis of Collective Adaptive Systems . . . . . . . . . . . . . . . . . 1
Jane Hillston
What You Always Wanted to Know About Model Checking
of Fault-Tolerant Distributed Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . 6
Igor Konnov, Helmut Veith, and Josef Widder
Applying MDA to Generate Hadoop Based Scientific
Computing Applications. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
Darkhan Akhmed-Zaki, Madina Mansurova, Bazargul Matkerim,
Ekateryna Dadykina, and Bolatzhan Kumalakov
Site-Level Web Template Extraction Based on DOM Analysis . . . . . . . . . . . 36
Julián Alarte, David Insa, Josep Silva, and Salvador Tamarit
Verification Support for a State-Transition-DSL Defined with Xtext . . . . . . . 50
Thomas Baar
Towards Using Exact Real Arithmetic for Initial Value Problems . . . . . . . . . 61
Franz Brauße, Marga rita Korovina, and Norbert Th. Mü ller
Constraint Solving for Verifying Modal Specifications of Workflow
Nets with Data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
Hadrien Bride, Olga Kouchnaren ko, and Fabien Peureux
Behavioural Analysis of Sessions Using the Calculus of Structures . . . . . . . . 91
Gabriel Ciobanu and Ross Horne
Using Refinement in Formal Development of OS Security Model . . . . . . . . . 107
Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin,
Alexander K. Petrenko, and Ilya V. Shchepetkov
Conflict Resolution in Multi-agent Systems with Typed Connections
for Ontology Population. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116
Natalia Garanina, Elena Sidorova, and Stepan Anokhin
Maximally-Polyvariant Partial Evaluation in Polynomial Time . . . . . . . . . . . 130
Robert Glück
Dynamics Security Policies and Process Opacity for Timed
Process Algebras. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149
Damas P. Gruska
Estimating Development Effort for Software Architectural Tactics. . . . . . . . . 158
Mohamad Kassab and Giuseppe Destefanis
Clone Detection in Reuse of Software Technical Documentation. . . . . . . . . . 170
Dmitrij Koznov, Dmitry Luciv, Hamid Abdul Basit, Ouh Eng Lieh,
and Mikhail Smirnov
Modeling Actor Systems Using Dynamic I/O Automata. . . . . . . . . . . . . . . . 186
Ilham W. Kurnia and Arnd Poetzsch-Heffter
RSSA: A Reversible SSA Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203
Torben Ægidius Mogensen
Checking Several Requirements at once by CEGAR . . . . . . . . . . . . . . . . . . 218
Vitaly Mordan and Vadim Mutilin
Unifying Requirements and Code: An Example . . . . . . . . . . . . . . . . . . . . . 233
Alexandr Naumchev, Bertrand Meyer, and Victor Rivera
Program Schemata Technique to Solve Propositional Program
Logics Revised . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245
Nikolay Shilov
Automated Two-Phase Composition of Timed Web Services . . . . . . . . . . . . 260
Maciej Szreter
Equivalence of Finite-Valued Symbolic Finite Transducers. . . . . . . . . . . . . . 276
Margus Veanes and Nikolaj Bjørner
Relaxed Parsing of Regular Approximations of String-Embedded
Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 291
Ekaterina Verbitskaia, Semyon Grigorev, and Dmitry Avdyukhin
Branching Processes of Timed Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . 303
Irina Virbitskaite, Victor Borovlyov, and Louchka Popova-Zeugmann
Implementation and Evaluation of Contextual Natural Deduction
for Minimal Logic. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 314
Bruno Woltzenlogel Paleo
Hybrid Lustre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 325
Zhenghen Yuan, Tingliang Zhou, Jing Liu, Juan Luo, Yi Zhang,
and Xiaohong Chen
Author Index ............................................ 341
X Contents