PSI 2014: Papers with Abstracts

Abstract. With adoption of the UML and other graphical languages by software industry,
graphical models became a cornerstone in today's software development practice.
As other artefacts such as program source code, graphical models evolve over
time and are, thus, put regularily under version control.

In order to deeply understand the role an artefact plays within a project, it is
sometimes helpful to review the history of this artefact. While there are
numerous tools available that make it easy for a user to grasp the evolution of
textual files (or even portions of it), an adequate support for graphical files
has remained to be an area of niche products.

In this paper, we argue that a better support for reviewing the version history
of graphical files can facilitate the work with graphical models. In order to
support this claim, we implemented a prototypcical tool that can extract and
display the version history of any graphical file stored in a GitHub-repository.
In addition, users can annotate each version of a file with comments, what
turns our tool into a review tool for software projects. Recently, we started to
use the tool is a software engineering course to give students better feedback
on complex UML models they have to develop iteratively.

Abstract. The article deals with the problem of proving observational equivalence for the class of computational processes called processes with message passing. These processes can execute actions of the following forms: sending or receiving of messages, checking logical conditions and updating values of internal variables of processes. Our main result is a theorem that reduces the problem of proving observational equivalence of a pair of processes with message passing to the problem of finding formulas associated with pairs of states of these processes, satisfying certain conditions that are associated with transitions of these processes. This reduction is a generalization of Floyd's method of flowchart verification, which reduces the problem of verification of flowcharts to the problem of finding formulas (called intermediate assertions) associated with points in the flowcharts and satisfying conditions, corresponding to transitions in the flowcharts. The above method of proving observational equivalence of processes with message passing is illustrated by a sliding window protocol verification

Abstract. The paper studies the subsequence relation through a notion of an intransitive binary relation on words in traces generated by prefix-rewriting systems. The relation was introduced in 1988 by V.F. Turchin for loop approximation in supercompilation. We study properties of this relation and introduce some refinements of the subsequence relation that inherit the useful features of Turchin's relation.

Abstract. The multiple trip vehicle routing problem involves several sequences of routes. Working shift of single vehicle can be scheduled in multiple trips. It is suitable for urban areas where the vehicle has very limited size and capacity over short travel distances. The size and capacity limit also requires the vehicle should be vacated frequently. As a result, the vehicle could be used in different trips as long as the total time or distance is not exceeded. Various approaches are developed to solve the vehicle routing problem (VRP). Except for the simplest cases, VRP is always a computationally complex issue in order to optimize the objective function in terms or both time and expense. Ant colony optimization (ACO) has been introduced to solve the vehicle routing problem. The multiple ant colony system is proposed to search for alternative trails between the source and destination so as to minimize (fuel consumption, distance, time) among numerous geographically scattered routes. The objective is to design adaptive routing so as to balance loads among congesting city networks and to be adaptable to connection failures. As the route number increases, each route becomes less densely packed. It can be viewed as the vehicle scheduling problem with capacity constraints. The proposed scheme is applied to typical cases of vehicle routing problems with a single depot and flexible trip numbers. Results show feasibility and effectiveness of the approach.