ICTERI 2013 Ermolayev, V., Mayr, H. C., Nikitchenko, M., Spivakovskiy, A., Zholtkevych, G., Zavileysky, M., Kravtsov, H., Kobets, V. and Peschanenko, V. (Eds.): ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer. Proc. 9th Int. Conf. ICTERI 2013, Kherson, Ukraine, June 19-22, 2013, CEUR-WS.org, online
This volume constitutes the refereed proceedings of the 9th International Conference on ICT in Education, Research, and Industrial Applications, held in Kherson, Ukraine, in June 2013.
The 49 papers were carefully reviewed and selected from 124 submissions. The volume opens with the contributions of the invited speakers. Further, the part of the volume containing the papers of the main ICTERI conference is structured in four topical parts: ICT infrastructures, Integration and Interoperability; Machine Intelligence, Knowledge Engineering and Management for ICT; Model-based software system development; and Methodological and Didactical Aspects of Teaching ICT and Using ICT in Education. This part of the volume is concluded by the two papers describing the tutorials presented at the conference. The final part of the volume comprises the selected contributions of the three workshops co-located with ICTERI 2013, namely: the 1st International Workshop on Methods and Resources of Distance Learning (MRDL 2013); the 2nd International Workshop on Information Technologies in Economic Research (ITER 2013); and the 2nd International Workshop on Algebraic, Logical, and Algorithmic Methods of System Modeling, Specification and Verification (SMSV 2013).
Copyright © 2013 for the individual papers by the papers’ authors. Copying permitted only for private and academic purposes. This volume is published and copyrighted by its editors. It is our pleasure to present you the proceedings of ICTERI 2013, the ninth edition of the International Conference on Information and Communication Technologies in Education, Research, and Industrial Applications: Integration, Harmonization, and Knowledge Transfer, held at Kherson, Ukraine on June 19-22, 2013. ICTERI is concerned with interrelated topics from information and communication technology (ICT) infrastructures to teaching these technologies or using those in education or industry. Those aspects of ICT research, development, technology transfer, and use in real world cases are vibrant for both the academic and industrial communities.
The conference scope was outlined as a constellation of the following themes: ICT infrastructures, integration and interoperability Machine Intelligence, knowledge engineering, and knowledge management for ICT Cooperation between academia and industry in ICT Model-based software system development Methodological and didactical aspects of teaching ICT and using ICT in education
A visit to Google Analytics proves the broad and continuously increasing interest in the ICTERI themes. Indeed, between November 15, 2012 and May 15, 2013 we have received circa 4 400 visits to the conference web site, http://icteri.org/, from 110 countries (568 cities). These numbers are 1.5 – 2 times higher than those observed in the similar period for ICTERI 2012.
ICTERI 2013 continues the tradition of hosting co-located focused events under its umbrella. In the complement to the main conference this year, the program offered the three co-located workshops, two tutorials, and IT talks panel. The main conference program has been composed of the top-rated submissions evenly covering all the themes of ICTERI scope.
The workshops formed the corolla around the main ICTERI conference by focusing on particular sub-fields relevant to the conference theme. In particular: The 1st International Workshop on Methods and Resources of Distance Learning (MRDL 2013) dealt mainly with the methodological and didactical aspects of teaching ICT and using ICT in education The scope of the 2nd International Workshop on Information Technologies in Economic Research (ITER 2013) was more within the topic of cooperation between academia and industry 2nd International Workshop on Algebraic, Logical, and Algorithmic Methods of System Modeling, Specification and Verification (SMSV 2013) focused on modelbased software system development
The IT Talks panel was the venue for the invited industrial speakers who wish to present their cutting edge ICT achievements.
This year we were also accepted the two focused short tutorials to the program: on ontology alignment and the industrial applications of this technology; and on the time model and Clock Constraint Specification Language for the UML profile used in modeling and analysis of real-time and embedded systems.
Overall ICTERI attracted a substantial number of submissions – a total of 124 comprising the main conference and workshops. Out of the 60 paper submissions to the main conference we have accepted 22 high quality and most interesting papers to be presented at the conference and published in our proceedings. The acceptance rate was therefore 36.7 percent. Our three workshops received overall 64 submissions, from which 27 were accepted by their organizers and included in the second part of this volume. Those selected publications are preceded by the contributions of our invited speakers. The talk by our keynote speaker Wolf-Ekkehard Matzke expressed his industrial views on the knowledge-based bio-economy and the “Green TripleHelix” of biotechnology, synthetic biology, and ICT. The invited talk by Gary L. Pratt was focused on a movement of higher education institutions to forming consortiums for creating a position of strength facing contemporary economic challenges. The invited talk by Alexander A. Letichevsky presented a general theory of interaction and cognitive architectures based on this theory.
The conference would not have been possible without the support of many people. First of all we would like to thank all the authors who submitted papers to ICTERI 2013 and thus demonstrated their interest in the research problems within our scope. We are also very grateful to the members of our Program Committee for providing timely and thorough reviews and also for been cooperative in doing additional review work. We would like also to thank the local organizers of the conference whose devotion and efficiency made this instance of ICTERI a very comfortable and effective scientific forum. Finally a special acknowledgement is given to the support by our editorial assistant Olga Tatarintseva who invested a considerable effort in checking and proofing the final versions of our papers.
June, 2013 Vadim Ermolayev Heinrich C. Mayr Mykola Nikitchenko Aleksander Spivakovskiy Grygoriy Zholtkevych Mikhail Zavileysky Hennadiy Kravtsov Vitaliy Kobets
Vladimir Peschanenko
Ministry of Education and Science of Ukraine Kherson State University, Ukraine Alpen-Adria-Universität Klagenfurt, Austria Zaporizhzhya National University, Ukraine Institute of Information Technology and Teaching Resources, Ukraine V. N. Karazin Kharkiv National University, Ukraine Taras Shevchenko National University of Kyiv, Ukraine DataArt Solutions Inc.
Aleksander Spivakovsky, Kherson State University, Ukraine
Vadim Ermolayev, Zaporizhzhya National University, Ukraine Heinrich C. Mayr, Alpen-Adria-Universät Klagenfurt, Austria Natalia Morse, National University of Life and Environmental Sciences, Ukraine Mykola Nikitchenko, Taras Shevchenko National University of Kyiv, Ukraine Aleksander Spivakovsky, Kherson State University, Ukraine Mikhail Zavileysky, DataArt, Russian Federation
Grygoriy Zholtkevych, V.N.Karazin Kharkiv National University, Ukraine
Mykola Nikitchenko, Taras Shevchenko National University of Kyiv, Ukraine Grygoriy Zholtkevych, V.N.Karazin Kharkiv National University, Ukraine
Aleksander Spivakovsky, Kherson State University, Ukraine Mikhail Zavileysky, DataArt, Russian Federation
Vladimir A. Shekhovtsov, Alpen-Adria-Universität Klagenfurt, Austria Mikhail Simonov, Istituto Superiore Mario Boella, Italy Marcus Spies, Ludwig-Maximilians-Universität München, Germany Aleksander Spivakovsky, Kherson State University, Ukraine Martin Strecker, IRIT, Universite Paul Sabatier, France Olga Tatarintseva, Zaporizhzhya National University, Ukraine Vagan Terziyan, University of Jyväskylä, Finland Nikolay Tkachuk, National Technical University "Kharkiv Polytechnic Institute”, Ukraine Leo Van Moergestel, Utrecht University of Applied Sciences, Netherlands Maryna Vladymyrova, V. N. Karazin Kharkov National University, Ukraine Paul Warren, Knowledge Media Institute, the Open University, United Kingdom Iryna Zaretska, V. N. Karazin Kharkov National University, Ukraine Mikhail Zavileysky, DataArt Solutions Inc., Russian Federation
Grygoriy Zholtkevych, V. N. Karazin Kharkov National University, Ukraine
Fahdi Al Machot, Alpen-Adria-Universität Klagenfurt, Austria Antonio Gonzalez-Pardo, Universidad Autonoma de Madrid, Spain Alexey Vekschin, National Technical University "Kharkiv Polytechnic Institute”, Ukraine
DataArt (http://dataart.com/) develops custom applications, helping clients optimize time-to-market and save costs Kherson State University (http://www.ksu.ks.ua/) is a multidisciplinary scientific, educational, and cultural center in the south of Ukraine Zaporizhzhya National University (http://www.znu.edu.ua/) is a renowned educational and research center of Ukraine that offers a classically balanced diversity of high quality academic curricula and many opportunities to build your scientific carrier Aleksandr Spivakovsky is the chair of the Department of Informatics and the first vice-rector of Kherson State University Dmitriy Shchedrolosev is the head of DataArt’s R&D Center at Kherson Preface ..........................................................................................................................I 1.5 ICTERI Tutorials ............................................................................................. 288 Binary Quasi Equidistant and Reflected Codes in Mixed Numeration Systems.... 311 Mechanism Design for Foreign Producers of Unique Homogeneity Product........ 329 Features of National Welfare Innovative Potential Parametric Indication Information-Analytical Tools System in the Globalization Trends’ Context ........ 339 Matrix Analogues of the Diffie-Hellman Protocol ................................................ 352 Are Securities Secure: Study of the Influence of the International Debt Securities on the Economic Growth.............................................................. 360 How to Make High-tech Industry Highly Developed? Effective Model of National R&D Investment Policy...................................................................... 366 Author Index ........................................................................................................... 595
Invited Contributions
Wolf-Ekkehard Matzke MINRES Technologises GmbH, Neubiberg, Germany Abstract. Over the last decades economies around the globe have transformed into a knowledge-based economy (KBE). Information and Communication Technology (ICT) has served as the principal enabling technology for this transformation. Now biology becomes another major pillar – producing a knowledge-based bio-economy (KBBE). The challenges faced by biotechnology push the requirements for ICT in many ways to the extreme and far beyond its basic utility function. In particular, it is valid for synthetic biology which aims to break ground on the rational design and construction of artificial biological systems with ICT as its backbone for bio-design automation (BDA). This could be best illustrated using a metaphor of a “green triple-helix”, where “green” stands for environmental consciousness and “triple-helix” visualizes the interdependency of biotechnology, synthetic biology, and ICT as the helical strands. The talk will explore this inter-dependency in dynamics. High level ICT requirements will be identified and discussed along the dimensions of education, research and industry with the emphasis on synthetic biology and BDA. The guidelines for the architecture and implementation of an open BDA platform will be presented so that interested ICT researchers and practitioners will better understand the biology-specific ICT challenges of the KBBE.
Eastern Washington University, 202 Huston Hall, Cheney, Washington 99004, USA
Gary L. Pratt Abstract. Colleges and universities compete for students, faculty, and business, industry, and research partnerships with quality programs, strong faculty, research opportunities, affordable cost, and high student success factors. Yet, at the infrastructure level, most of these institutions provide many similar information technology services and support. On top of this, many of these institutions struggle to provide this quality infrastructure because of a variety of factors, including: shrinking budgets, minimal strategic planning, and a lack of institutional vision of information technology as a strategic asset. This presentation will showcase best practice examples of how higher education institutions can band together, to create strong consortium relationships that can help all partners in this relationship move forward as a strong force. Examples will include actual successes experience by the Kentucky Council on Postsecondary Educations Distance Learning Advisory Committee (DLAC), the Washington Legislative Technology Transformation Taskforce (TTT), and the Washington Higher Education Technology Consortium (WHETC).These successes range from statewide strategic planning efforts, to significant consortial purchasing contracts, to collaborative technology systems, services, and training opportunities. This presentation will show that institutions can be stronger working together than working individually.
Keywords. University consortium, best practice, competition, infrastructure, information technology, strategic asset, strategic planning, collaborative technology system General Theory of Interaction and Cognitive Architectures
Alexander Letichevsky Glushkov Institute of Cybernetics, Academy of Sciences of Ukraine 40 Glushkova ave., 03187, Kyiv, Ukraine
let@cyfra.net Abstract. The challenge of creating a real-life computational equivalent of the human mind is now attracting the attention of many scienti c groups from di erent areas of cybernetics and Arti cial Intelligence such as computational neuroscience, cognitive science, biologically inspired cognitive architectures etc. The paper presents a new cognitive architecture based on insertion modeling, one of the paradigms of a general theory of interaction, and a basis for multiagent system development. Insertion cognitive architecture is represented as a multilevel insertion machine which realizes itself as a high level insertion environment. It has a center to evaluate the success of its behavior which is a special type agent that can observe the interaction of a system with external environment. The main goal of a system is achieving maximum success repeated. As an agent this machine is inserted into its external environment and has the means to interact with it. The internal environment of intelligent cognitive agent creates and develops its own model and the model of external environment. If the external environment contains other agents, they can be modeled by internal environment which creates corresponding machines and interprets those machines using corresponding drivers, comparing the behaviors of models and external agents. Insertion architecture is now under development on the base of Insertion modeling system, developed in Glushkov Institute of Cybernetics. Key terms. AgentBasedSystem, DistributedArti cialIntelligence, Reasoning, FormalMethod, Simulation 1
Introduction
General theory of interaction is a theory of information interaction in complex
distributed multi-agent systems. It has a long history. Contemporary part of
this history can be considered as starting from neuro networks of
McCullochPitts [
Insertion modeling is a trend that is developing over the last decade as an
approach to a general theory of interaction of agents and environments in
complex distributed multi-agent systems. The rst works in this direction have been
published in the middle of 90s [
In recent years, insertion modeling has been applied to the development
of systems for the veri cation of requirements and speci cations of distributed
interacting systems [2, 12, 19{21]. The system VRS, developed in order from
Motorola, has been successfully applied to verify the requirements and speci cations
in the eld of telecommunication systems, embedded systems, and real-time
systems. A new insertion modeling system IMS [
This paper presents the main principals of insertion modeling and the
conception of cognitive architecture based on insertion modeling. To understand the
formal part of the paper reader must be familiar with the concepts of labeled
transition system, bisimilarity and basic notions of general process theory. The
mathematical foundation of insertion modeling is presented in [
The Basic Principals Insertion modeling deals with the construction of models and study the interaction of agents and environments in complex distributed multi-agent systems. Informally, the basic principles of the paradigm of insertion modeling can be formulated as follows. 1. The world is a hierarchy of environments and agents inserted into them. 2. Environments and agents are entities evolving in time. 3. Insertion of agent into environment changes the behavior of environment and produces new environment which is in general ready for the insertion of new agents. 4. Environments as agents can be inserted into higher level environment. 5. New agents can be inserted from external environment as well as from internal agents (environments). 6. Agents and environments can model another agents and environments on the di erent levels of abstraction.
All these principles can be formalized in terms of transition systems, behavior algebras, and insertion functions. This formalization can be used as high level abstractions of biological entities needed for computer modeling of human mind.
The rst and the second principals are commonly used in information modelling of di erent kinds of systems, for example as in object oriented or agent programming. They are also resembling to M. Minsky's approach of the society of mind [27].
The third principal is clear intuitively, but has a special re nement in insertion modelling. We treat agents as transition systems with states considered up to bisimilarity (or up to behavior, which is the same). The type of an agent is the set of actions it can perform. The term action we use as a synonim of label for transitions, and it can denote signals or messages to send, events in which an agent can participate etc. This is the most general notion of agent which must be distinguished from more special notions of autonomous or intellectual agents in AI.
Transition system consists of states and transitions that connect states.
Transitions are labeled by actions (signals, events, instructions, statements etc.).
Transition systems are evolving in time changing their states, and actions are
observable symbolic structures used for communication. We use the well-known
notation s a! s0 to express the fact that transition system can evolve from the
state s to s0 performing action a. Usually transition systems are nondeterministic
and there can be several transitions coming from the same state even labeled by
the same action. If we abstract from the structure of states and concentrate only
on (branching) sequences of observable actions we obtain the state equivalence
called bisimilarity (originated from [28] and [24], exact de nition can be found
in [
Environment by de nition is an agent that possesses the insertion function. Given the state of environment s and the state of agent u, insertion function computes the new state of environment which is denoted as s[u]. Note that we consider states up to bisimilarity and if we have some representation of behaviors, the behaviors of environment and agent can be used as states. The state s[u] is a state of environment and we can use insertion function to insert a new agent v into environment s[u] : (s[u])[v] = s[u; v]. Repeating this construction we can obtain the state of environment s[u1; u2; : : :] with several agents inserted into it. Insertion function can be considered as an operator over the states of environment, and if the states are identi ed with behaviors, then the insertion of a new agent changes the behavior of environment.
Environment is an agent with insertion function, so if we forget the insertion function, then environment can be inserted as agent into a higher level environment and we can obtain hierarchical structure like
s[s1[u11; u12; : : :]E1 ; s2[u21; u22; : : :]E2 ; : : :]E Here notation s[u1; u2; : : :]E explicitly shows the environment E to which the state s belongs (environment indexes can be omitted if they are known from the context). This re nes the fourth principle.
Environment is an agent which can be inserted into external environment and having agents inserted into this environment. The evolution of agents can be de ned by the rules for transitions. The rules s[u] a! s[u; v] and s[t[u; v]] a! s[t[u]; v] can be used for the illustration of the 5-th principal.
We consider the creating and manipulation of the models of external and internal environments as the main property of cognitive processes of intellectual agent. Formalization of this property in terms of insertion modeling supports the 6-th principal.
Cognitive architecture will be constructed as a multilevel insertion environment. Below we shall de ne the main kinds of blocks used for construction of cognitive architecture. They are local description unites and insertion machines. 3 To represent behaviors of transition systems we use behavior algebras (a kind of process algebra). Behavior algebra is de ned by the set of actions and the set of behaviors (processes). It has two operations and termination constants. Operations are pre xing a:u (a - action, u - behavior) and nondeterministic choice u + v (u and v - behaviors). Termination constants are successful termination , deadlock 0, and unde ned behavior ?. It has also approximation relation , which is a partial order with minimal element ?, and is used for constructing a complete algebra with xed point theorem. To de ne in nite behaviors we use equations in behavior algebra. These equations have the form of recursive de nitions ui = Fi(u1; u2; : : :); i = 1; 2; : : : and de ne left hand side functions as the components of a minimal xed point. Left hand sides of these de nitions can depend on parameters ui(x) = Fi(u; x) of di erent types. In complete behavior algebra each behavior has a representation (normal form) u =
X ai:ui + "i i2I which is de ned uniquely (up to commutativity and associativity of nondeterministic choice), if all ai:ui are di erent ("u is a termination constant).
The type of environment is de ned by two action sets: the set of environment actions and the set of agent actions. The last de nes the type of agents which can be inserted into this environment: if the set of agent actions is included in the set of agent actions of environment then this agent can be inserted into this environment. This relation is called compatibility relation between agents and environments (agent is compatible with environment if it can be inserted into this environment). Multilevel environment is a family of environments with distinguished the most external environment. The compatibility relation on the set of environments de nes a directed graph and we demand for multilevel environment that the outermost environment would be reachable from any environment of the family in this graph.
To de ne the insertion function for some environment it is su cient to de ne transition relation for all states of environment including states with inserted agents. The common approach is to de ne behavior by means of rules. The following is an example of such rule: s !b s0; u !a u0 s[u] !c s0[u0]
P (a; b; c) This rule can be interpreted as follows. Agent in the state u can make a transition u !a u0. Environment allows this transition if the predicate P (a; b; c) is true. This rule de nes behavior property of environment in some local neighborhood of the state s[u]. So such a rule belongs to the class of local description units discussed in the next section.
At a given moment of time an agent belongs (is inserted) to only one environment. But if the type of an agent is compatible with the type of another environment it can move to this environment. Such a movements can be described by the following types of rules: moving from internal to external environment; u moveup E E[F [u; v]; w] moveup(F !E!) E[F [v]; u0; w]
u movedn !F u0 E[F [v]; u; w] movedn(E!F !) E[F [u0; v]; w] P1(E; F; u; moveup(E)) P2(E; F; u; movedn(F )) tional testing. Hundreds of components were formally specified and tested with UniTESK. By the end of the first year of using UniTESK the positive effect appeared in shorter time of integration of new versions of the distributed system. However, a serious problem revealed. In the previous UniTESK applications the requirements to most interfaces were defined by standards and other well-developed documents. But here the level of components documentation often appeared to be insufficient for creation of consistent specifications. Recovery of documentation or requirements to interfaces in the systems of such size becomes almost unsolvable task, which often makes it impossible to use MBT in corpore. Possible solution of this problem will be briefly discussed in Conclusion.
The largest example of UniTESK application is the OLVER (Open Linux
VERification) project [
The experience of interface formalization for a large industrial standard and test suite development for such standard gave many lessons to learn. One of such lessons is importance of informational and methodological organization of such project. The amount of documentation and sources, especially with respect to multiple versions and variants for different hardware platforms, is huge. Besides, the development of the standard and development of interface implementations involve thousands of people around the world. It means that the documentation maintenance and availability is one of the most important concerns of the projects of such scale. On the organizational and methodical side, we faced the fact that the training of new employees and the specification and tests quality control require a lot of effort, and the quick achievement of the required professional level is still impossible. In other words, the scalability of the MBT projects in the part of increasing the number of specification and verification experts is one of the most complicated problems preventing MBT from wide introduction.
One of the methodical problems is the choice of the abstraction level for the model. More abstract models or models separated into two-three layers of different abstraction levels simplify the reuse of the models and tests yielding, however, the bigger and more complex test system. In the long term, it’s better to have multilayer models, while in the short term the models close to implementation in the detail level (of course, if the implementation already exists) are more appropriate. A professional and experienced verification expert can find the balance between the abstract description of the behavior, for example, of a file system and specifics and details of the interface of its particular implementation. UniTESK provides special support for the separation of abstraction levels. In particular, the specifics of interfaces can be encapsulated in the mediator-adapter layer. The choice of the balance is determined by the long-tem plans on using and improvement of the models and the test suite. So, the work of such kind requires a broad experience and long-term planning skills, which can hardly be expected from ordinary test engineers.
The results of the OLVER project were used later on in the development of the test
suite for the Russian real-time operating system OS2000/3000 [
Along with the start of the OLVER project, the work on the UniTESK application
to testing of microprocessor designs [
Similar to the projects on verification of software systems, one of the main
problems preventing MBT from introduction into practice (as well as many other
verification methods) is the lack of documentation and other descriptions of functional
requirements to components. However, the situation in microprocessors development is
slightly better than in the case of software development, because in this case it is
customary to build system and architectural models of instruction set semantics along
with the HLD models. Elements of these architectural models can be used to fill the
gap in the knowledge on behavior of some microprocessor design units [
It is important to mention the verification tasks that, on the one hand, could not be
reduced to modeling with contract specifications, and, on the other hand, pushed
forward the development of new MBT methods. In the first place, the task of compiler
testing should be mentioned, as well as the task of testing microprocessor as a whole,
the so-called “core testing”. The both cases are the tasks of system testing, where test
data and test stimuli are submitted to a big “black box” (in our case, these are test
programs submitted to the compiler or loaded into memory of the microprocessor
simulator), and it is interesting to test not just everything, but some specific behavior
modes or specific group of units. In the case of compiler testing, the OTK tool has
been developed that was used for testing of optimizing Intel compilers and Simulink
[
Conclusions and Further Work Let’s start with positive conclusions.
Positive Conclusions on Modern State of Using MBT
The world experience is confirmed [
Negative Aspects of the Modern State in the MBT Area
The main obstacle preventing MBT from wide introduction into practice is the
absence of specifications/models in casual software development. That is, the lack
of specifications is often not only the consequence of insufficient attention to
specification development or the consequence of short resources. The main reason
is often the lack of qualified specialists who are experts in the knowledge domain
and at the same time can create specification/model necessary for test generation.
If MBT is used in projects that do not involve MDD (Model Driven Development)
approach, then the model development delays the appearance of first tests – this
does not allow obtain tests early in the development. If MBT is used within MDD,
then the problems still remain, because different models required for development
and for testing, in particular, for generation of different artifacts of the test suite. It
is often considered as unacceptable additional cost, while with proper planning
many components of the development models can be reused during test generation
as demonstrated, for example, in M. M. Chupilko paper [
Directions of Further Works A variety of modeling paradigms should be used in various project contexts, in particular, contract specifications, various types of executable models, for example, finite-state machines, Kripke structures, etc. [32]. It is not obvious that the transformation of models from one paradigm into another one will bring real benefit. Each of the model kinds is suitable for analysis of specific aspects of the system behavior, so we should not expect that, for example, a functional model will facilitate estimation of the execution time and memory required. However, obtaining some skeleton or a prototype of the model of one kind on the basis of another kind is quite possible. The development of various tools for modeling and specification description for the MBT purposes is required. In spite of the progress in the area of technologies for development of Domain Specific Languages (DSL), practically, the systems based on universal languages benefit from the large number of programmers knowing such languages. The same can be also said about monolingual systems – they overtake multilingual ones. Modern achievements in the area of static and hybrid static-dynamic analysis allow integration of these techniques into the MBT systems, at that, the models/specifications as well as software implementations should be the subject of this analysis. To overcome the problems with the extreme lack of specifications in real practice, tools for work with requirements and models (see, for example, [33]), in particular, with system models [34, 35] should be developed and deployed. For multicomponent systems, MBT tools should be integrated with the tools for architecture and process mining.
Protoautomata as Models of Systems with Data
Accumulation Irina Mikhailova1 and Boris Novikov2 and Grygoriy Zholtkevych2 1 Luhansk Taras Shevchenko National University, Institute of Information Technology, 2, Oboronna Str., 91011, Luhansk, Ukraine 2 V.N. Karazin Kharkiv National University, School of Mathematics and Mechanics, 4, Svobody Sqr., 61022, Kharkiv, Ukraine Abstract. In the paper formal models of software systems and their components based on the notion of an abstract machine are discussed. Necessity to model systems with data accumulation sets the problem of study of generalizations of the notion of an abstract automaton. In the paper two generalizations, namely, preautomata and protoautomata, are considered. It is shown that passing from automata via preautomata to protoautomata can be naturally realized using the language and methods of category theory.
Keywords. system modelling, abstract automaton, category of automata,
preautomata, category of preautomata, globalization, protoautomaton,
category of protoautomaton, re ector, free protoautomaton
Key terms. MathematicalModel, Speci cationProcess, Veri
cationProcess
1
Theory of abstract state machines or abstract automata is widely applied in
di erent areas of Computer Science. While the early applications of automata
theory were connected with theory of compilators design (see, for example, [
But the practice of modelling system behaviour based on the automata approach has shown that the approach is inadequate if data accumulation for the correct response is necessary.
Using the concept of partial action of a semigroup on a set [
In this paper, we consider a more general class of automaton-liked systems |
the class of protoautomata. All necessary information from the theory of
semigroups, automata theory, and category theory can be found in the monographs
[
We use the notation ' : A 99K B for the partial mapping of A to B (unlike the complete mapping A ! B). If '(a) is not de ned for a 2 A, we write '(a) = ?. The free monoid on the alphabet is denoted by , and its unit by ". All actions and preactions used in the paper are right, as it is common in the automata theory. 2
Preliminaries We will use the de nition of the automaton in the following form (the condition of the niteness is ignored): De nition 1. Given a set X and a free monoid over the alphabet , an automaton is a mapping X ! X : (x; a) 7! xa such that for all x 2 X and u; v 2
x" = x; x(uv) = (xu)v: (1) (2)
More general concept is the following
De nition 2 (see [
The preautomata over the monoid phisms are such maps ' : X ! Y that form a category PAut( ); its mor(8 a 2 )(8 x 2 X)( xa 6= ? =) ? 6= '(x)a = '(xa)): (3) The category Aut( ) of the automata over is a full subcategory of PAut( ).
Preautomata appear in the following situation. Let Y be an automaton and X an arbitrary nonempty subset of Y . Then a restriction of an action on X is a preautomaton.
Conversely, let X M 99K X be a preautomaton. The construction which is inverse to restriction is called globalization. More precisely: De nition 3. A globalization of the preautomaton X is an automaton Z with an injection : X ! Z such that for all a 2 , x 2 X ? 6= (x)a = (xa); xa 6= ? & (xa) = (x)a: Obviously, is a morphism of PAut(M ). We also call it a globalization. De nition 4. A globalization : X ! Z is called universal if for any globalization 0 : X ! Z0 there is an unique morphism { : Z ! Z0 such that 0 = { . The following construction gives an universal globalization (obviously unique up to isomorphism) for any preautomaton X 99K X. De ne a relation ` on the set X : (x; ab) ` (xa; b) () xa 6= ?: Let ' be an equivalence relation generated by `, and XU = (X )= '. An equivalence class of ' containing a pair (x; a) is denoted by [x; a]. For [x; a] 2 XU and b 2 , we set [x; a]b = [x; ab]. Thus a complete action on XU is de ned. Theorem 1. The automaton XU with a morphism U : X ! XU : x 7! [x; "] is the universal globalization of the preautomaton X.
Proof. See [4, Theorem 2] 3
Protoautomata (4) The main object of this paper is a generalization of the notion of preautomaton: De nition 5. A protoautomaton is a partial mapping X (x; a) 7! xa such that 99K X : a) the condition (1) is ful lled; b) if xu 6= ? and (xu)v 6= ?, then x(uv) 6= ? and equality (2) is ful lled. We will also denote the protoautomaton from this de nition simply by X, if it does not cause a confusion.
Example 1. Let S be a free subsemigroup of and : X S ! X an automaton. De ne a partial mapping X 99K X as an extension of , putting xu = ? for u 2 n S; so we get a protoautomaton over . Note that in general it is not a preautomaton. In addition, this example shows that the automaton over an in nite alphabet can be represented as a protoautomaton over a two-letter alphabet.
Example 2. Let X = fx; yg be a two-element set, L a subset of protoautomaton X 99K X putting for a 6= " . De ne a xa = y; if a 2 L; ?; if a 2= L; and ya = ?. This example shows that protoautomata recognize all languages.
We denote the category of protoautomata with morphisms de ned by the condition (3) by PtAut( ); clearly, PAut( ) is its subcategory.
It follows from the theory of partial action of semigroups [6, Theorem 5.7], that a protoautomaton which is not a preautomaton has no globalization. More precisely, for the protoautomaton X we can construct an automaton XU as in Sec. 2, but in this case the morphism U is not injective in general.
In this situation, the concept of a re ector is useful. We recall its de nition De nition 6. A subcategory D of a category C is called re ective if with each object C 2 C an object RD(C) 2 D is associated (called D-re ector of the object C) and a morphism D(C) : C ! RD(C) (re ection morphism) such that for each D 2 D the diagram
C D(!C) RD(C) can be extended uniquely to a commutative diagram by some morphism out HomD(RD(C); D).
It is convenient to use another description of the equivalence ': Lemma 1. De ne a relation ] on the set X : (x; a) ] (y; b) () (9 a0; b0; p 2
)(a = a0p & b = b0p & xa0 = yb0 6= ?): Let be the equivalence relation generated by ]. Then coincides with '.
Proof. If (x; a) ] (y; b) then
(x; a) = (x; a0p) ` (xa0; p) = (yb0; p) a (y; b0p) = (y; b); whence '.
Conversely, if (x; a) ` (y; b), then a = cb; y = xc for some c 2 ` ]. Consequently, ' . Hence Remark 1. Obviously, ` is re exive and transitive, while ] is re exive and symmetric.
Lemma 2. Let X be a protoautomaton, Y be a preautomaton (both over ), : X ! Y be a morphism, x; y 2 X, a 2 . Then [x; "] = [y; a] implies (x) = (y)a 6= ?..
Proof. It follows from the condition that
(x; ") ] (z1; b1) ] : : : ] (zn; bn) ] (y; a) for some z1; : : : ; zn 2 X, b1; : : : ; bn 2
Proof has completed Similarly (and even easier) one can prove Lemma 3. Let X be a protoautomaton, Y be an automaton (both over ), : X ! Y be a morphism, x; y 2 X, a; b 2 . Then [x; a] = [y; b] implies (x)a = (y)b.
Proof is omitted tu
We set [X; "] = f[x; "] 2 XU j x 2 Xg. Obviously, [X; "], being a subset of XU , is a preautomaton, and in addition, U (X) = [X; "]. (z1)b1. Suppose bn = cp; a = dp; znc = yd 6= ? for some c; d; p 2 . Then (zn)c 6= ? and by the induction Since Y is a preautomaton then (zn)(cp) 6= ?. (x) = (zn)(cp) = (znc)p = (yd)p = ( (y)d)p = (y)a: tu Theorem 2. Let X be a protoautomaton over , then 1. [X; "] is a re ector for X in the category PAut( ), 2. XU is a re ector for X in Aut( ), 3. XU is a re ector for [X; "] in Aut( ).
Proof. 1) Let Y be some preautomaton and : X ! Y be a morphism of
protoautomata. The required morphism : [X; "] ! Y is uniquely determined
from the equality = U . Indeed, for x 2 X we have (x) = U (x) = ([x; "]).
It follows from Lemma 2 that is well-de ned.
2) Similarly, using Lemma 3.
3) Follows from 1), 2), and the following well-known fact [
Example 3. Let X = fx; y; z; tg, p; u; v 2 n f"g. We set zu = zv = t; z(up) = x; z(vp) = y and sw = ? for all s 2 X; w 2 n f"; p; u; vg. In such a manner X turns into a protoautomaton. Since (x; ") ] (z; up) ] (z; vp) ] (y; ") then [x; "] = [y; "] and the re ection morphism of X is non-injective.
A large class of protoautomata is contained in the following example.
Example 4. Consider a preautomaton X 99K X as a directed weighted
multigraph with states as vertices and with edges of the form (x; u; y), where
x; y 2 X, u 2 , and y = xu. Let U be an arbitrary subset of edges of X. Build
a transitive closure U t of the set U , extending it step by step by the rule: if the
edges (x; u; y) and (y; v; z) are at some stage in the expansion, then on the next
step we include the edge (x; uv; z). Then U t is a protoautomaton.
Example 3 shows that there exists a protoautomaton such that it can not be
embedded into some preautomaton (and thus into some automaton).
4
It is well known [
Recall the necessary de nitions: De nition 7. Let C and D be categories, F : C D be a functor, C be an object of C. An object D of D is called free on C with respect to the functor F , if there is a morphism : C ! F D such that for any object D0 2 D and any morphism : C ! F D0 there exists the unique morphism : D ! D0 such that F ( ) = :
We consider a category Rel( ) whose objects are pairs (X; ), where X is a set (X 2 Set), X is a binary relation such that X f"g . A morphism : (X; ) ! (Y; ) of Rel( ) is a map : X ! Y such that ( x; u) 2 for (x; u) 2 .
Next, let F be a forgetful functor F : PtAut( ) protoautomaton X 99K X to the pair (X; ) with Rel( ) mapping each = f(x; u) j xu 6= ?g.
Theorem 3. For each object (X; ) 2 Rel( ) there is a protoautomaton that is free on it with respect to the forgetful functor F .
Proof. For (X; ) 2 Rel( ) construct a protoautomaton M = ( de ning the action by the rule 99K ), (x; u)v = (x; uv); if (x; uv) 2
?; if (x; uv) 2= : Then F M = ( ; ^), where ^ = f((x; u); v) j (x; u)v = (x; uv)g . De ne the morphism : (X; ) ! ( ; ^) by the formula (x) = (x; ").
Let us show that M is a free protoautomaton on (X; ).
Let N = (Y 99K Y ) be some protoautomaton and F Y = (Y; ). For the required morphism : M ! N of (5) we have:
(x; ") = F ( )(x; ") = F ( ) (x) = (x): Then for any u 2 one can obtain
(x; u) = (x; ")u = (x)u; is uniquely determined Conclusion tu It seems that the class of protoautomata, which has been introduced in the paper, gives the most abstract models for systems with discrete behaviour. This class of abstract machines includes not only machines reacting on the received data immediately, as automata, but it also includes machines whose reactions depend on the accumulated information.
The machines of this class having a greedy behaviour are united into a
subclass whose instances are called preautomata. Machines of the subclass are used
for modelling behaviour systems for complex event processing as it was shown
earlier [
Therefore, by eliminating the condition c) we provide a possibility to study nondeterministic models. In our opinion, the models derived in this way (protoautomata) are interesting objects that can be used for speci cation and verication of complex systems.
Dmitriy Buy1 and Serhiy Kompan1 Taras Shevchenko National University of Kyiv, Faculty of Cybernetics, 03680 Academician Glushkov Avenue 4d, Kyiv, Ukraine Abstract. This paper describes the application of heterogeneous algebraic system for the construction of the formal model of object database instead of object algebra. Complete formalization of the operation of intersection of class specifications is given.
Keywords. object-oriented programming, object database, object algebra, class specification
Key terms. MathematicalModel
1
In applications of information technologies there is a problem of construction of the
so-called dependable and stable systems and infrastructures – the systems which
behave stably under all, especially, critical working circumstances. Similarity of risks
and increasing actuality of their decline to an acceptable level for critical applications
led to the appearance of a special term “safeware”, by the analogy with the terms
“hardware”, “software”, “firmware” etc., which combines two components: safe –
secure and ware – a product, an item. This term was suggested and patented by the
leading expert of NASA on the questions of infrastructure security, professor
N. Leveson, who registered the appearance of a modern field of knowledge called
safeware engineering [
For the full confidence in the fact that informational system will work stably (will
be dependable and stable), one should single out system components, describe them
formally and verify. Indeed, nowadays there is nothing instead of a “divide and rule”
approach to cope with this difficulty. In fact, one of the most important components
of any complex system (infrastructure) is databases. That’s why there should exist an
appropriate formal model. For the relational databases such a formal model has been
already constructed and explored considerably. This issue is exhaustively covered in
the literature, beginning from the pioneering works by E.F. Codd (see, e.g. [
Nowadays, there are a lot of formal models of object-oriented databases (OODB)
[
Practical results
The authors of this paper have conducted a number of investigations in the field under
research: for example, in the article [
Let’s start with the intersection operation . Let us formalize the notion of a class:
by a class we mean a pair K s, , where s is a functional binary relation which
associates an attribute with its meaning (from a universal domain D ), and is a
functional binary relation, which brings to conformity a method with its signature.
Therefore [
The intersection operation (of class specifications) is an operation of the form : , where: s1, 1 s2 , 2 s1 s2 , 1 2 , where is a standard set-theoretical intersection.
We will demonstrate some results concerning the structure of a partially ordered set (poset) F, , where
is a set of all the functional binary relations (on the
universal domain ), а is an ordinary set-theoretical inclusion. These results will
supplement the results of the paper [
Lemma 1. For the arbitrary functional binary relations and the following equality is true: f g ( f g) (domf domg) □
def
Proof. ■ Let us start with X domf domg . Let us use generally valid properties
of the set-theoretical restriction operation (a binary ratio on a set) (monotony,
distributivity etc.) [
Firstly, we have an inclusion dom( f g) domf domg X . Secondly, from this the next chain of equalities and inequalities follows: f g ( f g) dom( f g) ( f g) X f X g X f g .
Thus, f g ( f g) X ( f g ) (domf domg ) □ def Below is a relation of consistency: f g f X g X , where
def
X domf domg . In [
The following lemma’s corollary forms another criterion of consistency.
Corollary (the criterion of consistency of functional binary relations). Let f , g be arbitrary functional binary relations, and f g dom( f g) X , ( f g) dom( f g) X . □
Proof. ■ The proof is performed by using a Lemma 1 and inclusion dom( f g) X . It’s important to note that the second (the first) equivalence is a formal corollary of the first one (of the second one accordingly). □
As for the structure of the poset F, , there are two statements.
Statement 1. Poset
is a lower semilattice, and at the same time, inff , g f g . □
The proof results from the fact that is a commutative idempotent semigroup and
from a well-known connection between such semigroups and lower semilattices (see,
e.g. [
More complete information about the poset F, is given by the following statement.
Statement 2. (the structure of poset F, ). The following statements are true: 1. The empty function f is the smallest element (“a bottom”) def X domf domg .
Then: 2. The largest element in poset F,
exists if and only if the universe D is singleton 3. The infimum exists for any nonempty set F and inf F f F f 4. The supremum of the set F exists if and only if in the case when the set F is restricted, and supF f F f 5. The element f is an atom only when f is singleton 6. Poset F, is a relatively complete poset and a complete (upper) semilattice □ Let’s proceed to the substantial interpretation of above results.
The operation constructs a new class which will be basic (paternal) for classes arguments. This intersection can also be empty, in this case we will get a special empty class.
As the relation on the specifications is component wise ( s, s, s s ) , all properties of the relation (statements 1, 2) can be lifted to the relation . The corresponding formulations are obvious and thereby are omitted. 3
Results and conclusions The model of intersection operation of class specifications has been examined. This operation has been specified as set-theoretical intersection. The specification f g has been interpreted as the largest total part of f and g , that is, the specification from which specifications-arguments can be obtained by inheritance (in other words, the result specification is the specification of a paternal class). The conditions for nonempty (equivalent, empty) intersection have been examined.
As for formal results, natural criteria of function consistency have been presented (corollary) which supplement the already known criteria; the structure of a partially ordered set of partial functions has been specified (statements 1, 2).
References Alferov, Eugene................................... 108 Alobaidi, Mizal...................................... 18 Arkatov, Denis B. ................................ 178 Aronov, Andrey ................................... 252 Baiev, Oleksandr ................................. 118 Baklanova, Nadezhda .......................... 550 Batyiv, Andriy ....................................... 18 Becker, Karsten ................................... 424 Beletsky, Alexsander ........................... 352 Beletsky, Anatoly ........................ 311, 352 Beletsky, Evgeny ................................. 311 Bilousova, Lyudmyla........................... 209 Blinov, Igor Ol..................................... 565 Bodnenko, Dmitry ............................... 281 Bonda, Darya....................................... 360 Buy, Dmitriy........................................ 590
A B C D Chaabani, Mohamed ............................ 521 Cochez, Michael .................................. 221 Davidovsky, Maxim ...................... 99, 295 Derevianko, Andrii ................................ 30 Didenko, Ievgen................................... 118 Doroshenko, Anatoliy............................ 38 Dzyubenko, Artem............................... 252 Echahed, Rachid ..................................521 Ermolayev, Vadim ...... II, 64, 99, 108, 295
E Kandyba, Roman .................................352 Keberle, Natalya G.................................79 Kharchenko, Vyacheslav .....................146 Klionov, Dmitriy M. ............................464 Kobets, Vitaliy ........................ II, 310, 329 Kolgatin, Oleksandr .............................209 Kolgatina, Larisa..................................209 Kompan, Serhiy ...................................590 Kotkova, Vera......................................236 Kravtsov, Hennadiy ................ II, 236, 410 Kropotov, Aleksandr..............................30 Kryukov, Sergey ..................................310 Kryvolap, Andrii..................................533 Kukharenko, Vladimir .................273, 410 Maksimov, Andrey .............................. 573 Mallet, Frédéric ................... 130, 289, 475 Mantula, Elena....................................... 91 Manzhulam Anna ................................ 195 Mashtalir, Vladimir ............................... 91 Matthes, Ralph..................................... 506 Matzke, Wolf-Ekkehard .......................... 2 Mayr, Heinrich C.................................... II Mazol, Sergey...................................... 360 Mazol, Sergey...................................... 366 Mesropyan, Karine .............................. 385 Mikhailova, Irina ................................. 582 Moiseeva, Oksana................................ 366 Möller, Dietmar P.F............................. 424 Morze, Natalia ..................................... 264 Morze, Natalia V. ................................ 411
N O
P Nikitchenko, Mykola .............. II, 447, 533 Novikov, Boris .................................... 582 Odarushchenko, Oleg .......................... 146 Odarushchenko, Valentina................... 146 R S T V W
Y Popov, Peter.........................................146 Pratt, Gary L. ...........................................3 Protsenko, Galina.................................264 Ralo, Aleksandr .....................................30 Richter, Harald.....................................424 Romenska, Yuliia.................................130 Rudenko, Margarita .............................401 Tatarintseva, Olga..................................64 Tirronen, Ville .....................................221 Tkachuk, Nikolay...................................48 Tolok, Vyacheslav .................................99 Payentko, Tanya .................................. 310 Peschanenko, Vladimir ........... II, 447, 490 Petrenko, Alexander K......................... 573 Petukhova, Lyubov.............................. 236 Yatsenko, Olena.....................................38 Valko, Nataliya ....................................195 Varava, Anastasiia ...............................163 Vasylevych, Leonid .............................187 Vozniy, Oleksiy .....................................30 Weissblut, Alexander J. .......................374
Winckel, Mathias .................................506 Zaporozhchenko, Yulia........................ 410 Zaretska, Iryna..................................... 475 Zavileysky, Mikhail................................ II Zhereb, Kostiantyn.................................38 Zholtkevych, Galyna............................475 Zholtkevych, Grygoriy..... II, 18, 163, 475, 582