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 24–27, 2015

Revised Selected Papers

123

Editors

Manuel Mazzara

Innopolis University

Innopolis

Russia

Andrei Voronkov

The University of Manchester

Manchester

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

This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the

material is concerned, speciﬁcally the rights of translation, reprinting, reuse of illustrations, recitation,

broadcasting, reproduction on microﬁlms 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 speciﬁc 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 24–25, 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 scientiﬁc 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 Gurﬁnkel 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