PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 22

Liczba wyników na stronie
first rewind previous Strona / 2 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 2 next fast forward last
1
Content available A survey of Alvis communication modes
Szpyrka M., Biernacki J., Matyasik P., Wypych M.
International Journal of Microelectronics and Computer Science
|
2017
|
Vol. 8, nr 1
1--9
EN
Concurrent systems appear natural and intuitive solution for many real IT problems. However, designing a more complex concurrent system is a difficult task. The main problem is that for systems that have more than several subsystems it becomes difficult to control their properties at the design stage. Applications of formal methods in the development process may remarkable reduce the problem. An important issue is to choose a suitable formal modelling language, that supports the required methods of communication between subsystems. The paper provides a survey of communication modes introduced to the Alvis modelling language and discusses how the communication modes may be used while modelling concurrent systems.
2
Content available remote Classifiers for Behavioral Patterns Identification Induced from Huge Temporal Data
Bazan J. G., Szczur A., Dydo L., Wojtowicz H., Szpyrka M.
Fundamenta Informaticae
|
2016
|
Vol. 143, nr 1/2
19--34
EN
A new method of constructing classifiers from huge volume of temporal data is proposed in the paper. The novelty of introduced method finds expression in a multi-stage approach to build hierarchical classifiers that combines process mining, feature extraction based on temporal patterns and constructing classifiers based on a decision tree. Such an approach seems to be practical when dealing with huge volume of temporal data. As a proof of concept a system for packet-based network traffic anomaly detection was constructed, where anomalies are represented by spatio-temporal complex concepts and called by behavioral patterns. Hierarchical classifiers constructed with the new approach turned out to be better than “flat” classifiers based directly on captured network traffic data.
3
Content available Tools and Methods for RTCP-Nets Modeling and Verification
Szpyrka M., Biernacki J., Biernacka A.
Archives of Control Sciences
|
2016
|
Vol. 26, no. 3
339--365
EN
RTCP-nets are high level Petri nets similar to timed colored Petri nets, but with different time model and some structural restrictions. The paper deals with practical aspects of using RTCP-nets for modeling and verification of real-time systems. It contains a survey of software tools developed to support RTCP-nets. Verification of RTCP-nets is based on coverability graphs which represent the set of reachable states in the form of directed graph. Two approaches to verification of RTCP-nets are considered in the paper. The former one is oriented towards states and is based on translation of a coverability graph into nuXmv (NuSMV) finite state model. The later approach is oriented towards transitions and uses the CADP toolkit to check whether requirements given as μ-calculus formulae hold for a given coverability graph. All presented concepts are discussed using illustrative examples.
4
Content available remote Formal Description of Alvis Language with α0 System Layer
Szpyrka M., Matyasik P., Mrówka R., Kotulski L.
Fundamenta Informaticae
|
2014
|
Vol. 129, nr 1/2
161--171
EN
The paper presents a formal description of a subset of the Alvis language designed for the modelling and formal verification of concurrent systems. Alvis combines possibilities of a formal models verification with flexibility and simplicity of practical programming languages. Alvis provides a graphical modelling of interconnections among agents and a high level programming language used for the description of agents behaviour. Its semantic depends on the so-called system layer. The most universal system layer α0, described in the paper, makes Alvis similar to other formal languages like Petri nets, process algebras, time automata, etc.
5
Content available Communication with Environment in Alvis Models
Szpyrka M., Matyasik P., Mrówka R., Kotulski L.
International Journal of Electronics and Telecommunications
|
2012
|
Vol. 58, No. 3
247-254
EN
Alvis is a modelling language defined for the design and a formal verification of embedded systems. An Alvis model is a system of agents that usually run concurrently, communicate one with another, compete for shared resources etc. Due to the fact that an embedded system usually collects inputs that come from its environment and provides outputs that go to the environment it is necessary to provide a mechanism to describe such a communication. In contrast to another formal languages used to model embedded systems it is not necessary, using Alvis, to design such an environment as a part of a model. The paper deals with the problem of modelling a communication with an embedded system environment with Alvis.
6
Content available Modelling concurrent systems with Alvis
Szpyrka M.
Pomiary Automatyka Robotyka
|
2011
|
R. 15, nr 12
239-240
EN
Alvis is a new modeling language for developing concurrent (embedded) systems. The language is being developed within the confines of the Alvis project at AGH University of Science and Technology, Department of Automatics. The Alvis language combines hierarchical graphical modelling with a high level programming language. Moreover, a formal verification of a model, based on an LTS graph (Labelled Transition System) is possible. The paper describes selected features of the language and the future plans of the project.
PL
Alvis jest nowym językiem modelowania przeznaczonym do rozwijania systemów współbieżnych, zwłaszcza systemów wbudowanych. Język jest rozwijany w Katedrze Automatyki AGH w ramach projektu o tej samej nazwie. Język Alvis łączy w sobie cechy języków programowania wysokiego poziomu z hierarchicznym językiem modelowania połączeń między agentami. Ponadto umożliwia on formalną weryfikację systemu wbudowanego bazującego na grafie LTS, stanowiącego formalną reprezentację przestrzeni stanów modelu. Artykuł zawiera przegląd podstawowych informacji na temat języka i projektu.
7
Content available Introduction to Alvis modelling language
Szpyrka M., Matysik P., Mrówka R., Witalec W., Baniewicz J., Balicki K.
Pomiary Automatyka Kontrola
|
2011
|
R. 57, nr 9
1086-1089
EN
Alvis is a novel modelling language designed for embedded systems. It combines both high level programming language used to define agents behaviour with hierarchical graphical modelling language used to define interconnections between agents. The paper presents a survey of the most important features of the language.
PL
Alvis jest nowym językiem modelowania przeznaczonym do rozwijania systemów wbudowanych. Łączy w sobie cechy języków programowania wysokiego poziomu z hierarchicznym językiem modelowania połączeń między agentami. Podstawowym elementem języka Alvis są agenty, które mogą działać współbieżnie, komunikować się ze sobą, czy też współzawodniczyć o zasoby dzielone. Dynamika poszczególnych agentów jest opisywana w warstwie kodu używającej do tego celu języka programowania wysokiego poziomu (połączenie natywnych konstrukcji języka Alvis i języka funkcyjnego Haskell). W warstwie graficznej definiowane są połączenia między agentami wskazujące, które agenty się ze sobą komunikują i jaki jest kierunek tej komunikacji. Warstwa ta ma postać grafu hierarchicznego, co pozwala rozwijać systemu wbudowane metodą od ogółu do szczegółu lub odwrotnie. Formalną reprezentacjąmodelu w języku Alvis jest graf LTS (Labelled Transition System), który reprezentuje wszystkie osiągalne stany i przejścia między nimi. Graf ten jest stosowany do formalnej weryfikacji modelu. Artykuł zawiera przegląd najistotniejszych cech języka Alvis.
8
Content available Introduction to modelling embedded systems with Alvis
Szpyrka M., Matyasik P., Mrówka R., Witalec W., Baniewicz J., Kotulski L.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2011
|
T. 15, z. 2
435-442
EN
Alvis is a modelling language for concurrent and real-time systems. It combines hierarchical graphical modelling with a Haskell-based high level programming language. The graphical layer is used to define data and control flow among agents. The code layer is used to describe the behaviour of individual agents. An Alvis model is transformed into a labelled transition system (LTS) that is used for formal verification of the model. The paper discusses some aspects of modelling embedded systems with Alvis.
PL
Alvis jest językiem modelowania rozwijanym z myślą o systemach współbieżnych w szczególności systemach wbudowanych. Łączy on w sobie graficzny język modelowania, przeznaczony do definiowania połączeń komunikacyjnych między agentami, z językiem programowania wysokiego poziomu, przeznaczonym do definiowania zachowania poszczególnych agentów. W artykule przedstawiono wybrane aspekty modelowania systemów wbudowanych z użyciem języka Alvis.
9
Alvis approach to Hexor robot controller development
Szpyrka M., Matyasik P., Mrówka R.
Elektronika : konstrukcje, technologie, zastosowania
|
2010
|
Vol. 51, nr 11
63-66
PL
Alvis jest językiem modelowania, rozwijanym głównie z myślą o projektowaniu i weryfikacji systemów wbudowanych. Wywodzi się on z algebr procesów CCS i XCCS, ale w języku tym równania algebraiczne zostały zastąpione przez język programowania wysokiego poziomu oparty na języku Haskell. W przeciwieństwie do algebr procesów, które umożliwiają wyłącznie tekstowy opis systemów wbudowanych, w języku Alvis struktura projektowanego systemu, z punktu widzenia przepływu danych i sterowania, przedstawiana jest graficznie za pomocą diagramów komunikacji. Poniższy artykuł zawiera wprowadzenie do języka Alvis zilustrowane modelem sterownika dla robota mobilnego Hexor II.
EN
Alvis is a novel modelling language defined especially for the embedded systems design and verification. The language has its origin in CCS and XCCS process algebras, but algebraic equations have been replaced with a Haskell based high level programming language. Moreover, Alvis provides communication diagrams for the visual modelling of an embedded system structure, especially from the control and data-flow point of view. This paper presents an introduction to Alvis based on a model of a controller for the Hexor II mobile robot.
10
Content available remote Formal Definition of XCCS Modelling Language
Balicki K., Szpyrka M.
Fundamenta Informaticae
|
2009
|
Vol. 93, nr 1-3
1-15
EN
The paper presents a formal definition of XCCS - a graphical extension of CCS process calculus. The aim of this extension is to supply graphical means for creating models and thus to eliminate problems typical for modelling in textual manner inherent to CCS process algebra. XCCS diagrams consist of two layers, a graphical one that represents the structure of a modelled system and algebraic one that describes behaviour of individual agents. The graphical layer takes the form of a directed graph, while the algebraic one is a set of sequences of algebraic equations similar to those in the CCS calculus. The formal definition presented in the paper deals with both parts of such models. At the end of the paper we define the Synchronization Relation and present the Basic Conversion Algorithm that converts XCCS diagrams into CCS scripts.
11
Content available A conceptual model for web knowledge acquisition system with GIS component
Ligęza A., Ernst S., Nalepa G. J., Szpyrka M.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2009
|
T. 13, z. 2
421-428
EN
Building efficient tools for supporting Knowledge Acquisition and Knowledge Management is a challenge and hot research topic with potentially infinite numbers of applications. In modern computer science, the web technologies open a completely new chances for massive, distributed knowledge acquisition. Examples of such social phenomena as Wikipedia constitute a working proof of high potentials incorporated in the synergy of human and web interaction. This paper discusses certain issues concerning the conceptual model for a distributed knowledge acquisition system gathering and organizing knowledge on threats of various nature and aimed at improving safety of citizens in urban environments. The system for registering citizen-provided information is a part of the INDECT FP7 Project. Contemporary tools and techniques to be applied, including GIS technologies and Semantic Wikis are presented in brief and future problems to be solved are identified.
PL
Wytworzenie skutecznych narzędzi wspierających pozyskiwanie wiedzy oraz zarządzanie wiedzą jest wyjątkowo trudnym zadaniem, którego rozwiązanie mogłoby skutkować potencjalnie nieograniczoną liczbą zastosowań. Rozwój technologii webowych daje współcześnie zupełnie nowe możliwości implementacji dużych rozproszonych systemów pozyskiwania wiedzy. Przykładem takiego systemu jest Wikipedia będąca dowodem na niezwykłe możliwości wynikające z interakcji człowieka i sieci web. W referacie przedstawiono wybrane aspekty związane z konceptualnym modelem rozproszonego systemu pozyskiwania wiedzy, którego zadaniem jest gromadzenie i organizacja wiedzy różnego typu, w celu poprawy bezpieczeństwa mieszkańców terenów miejskich. System rejestracji informacji dostarczanych przez mieszkańców jest częścią projektu INDECT (FP7). W referacie zawarto przegląd współczesnych narzędzi i technik, które zostaną zastosowane w projekcie (m.in. GIS i Semantic Wikis), wraz z identyfikacją problemów, które muszą zostać rozwiązane.
12
Content available Dynamiczny model świata w sterowaniu autonomicznym robotem mobilnym
Kułakowski K., Wąs J., Szpyrka M.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2008
|
T. 12, z. 3
833-840
PL
Skuteczne działanie autonomicznego robota mobilnego zależy w dużym stopniu od umiejętności planowania swoich ruchów tak, aby osiągnąć założone cele. Istotną rolę w takim planowaniu odgrywa model otaczającego świata. Pozwala on z jednej strony na przechowywanie wiedzy o świecie, z drugiej zaś, na efektywne planowanie sekwencji ruchów dopuszczalnych. W prezentowanej pracy autorzy rozważają model reprezentacji świata w postaci automatu komórkowego. W pracy zaprezentowano również studialny, prosty algorytm sterujący robotem dla problemu planowania ścieżki.
EN
Successful working of autonomous mobile robot highly depends on ability to plan its own motion in such a way, which allows accomplishing specified tasks. Important role in such planning plays model of the surrounding world. It serves as knowledge storage and it allows for effective computing a sequence of admissible motions of the robot. In the presented paper authors take into a consideration world model in a form of cellular automaton. A simple control algorithm for a collision free path finding problem is also discussed.
13
Content available Architektura autonomicznego robota mobilnego z dynamicznym modelem świata
Kułakowski K., Wąs J., Szpyrka M.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2008
|
T. 12, z. 3
821-831
PL
Skuteczne działanie autonomicznego robota mobilnego zależy w dużym stopniu od umiejętności planowania swoich ruchów tak, aby osiągnąć założone cele. Istotną rolę w takim planowaniu odgrywa model otaczającego świata. Pozwala on z jednej strony na przechowywanie wiedzy o świecie, z drugiej zaś, na efektywne planowanie sekwencji ruchów dopuszczalnych. W prezentowanej pracy autorzy pragną przedstawić projekt ogólnej architektury inteligentnego systemu sterowania autonomicznym robotem mobilnym, wykorzystujący dynamiczny model świata skonstruowany z wykorzystaniem wiedzy w postaci automatu komórkowego.
EN
Successful working of autonomous mobile robot highly depends on ability to plan its own motion in such a way, which allows accomplishing specified tasks. Important role in such planning plays model of the surrounding world. It serves as knowledge storage and it allows for effective computing a sequence of admissible motions of the robot. In the presented paper authors would like to present a general architecture of intelligent control system for autonomous mobile robot with dynamic world model using knowledge in form of cellular automaton.
14
Content available remote Analysis of RTCP-nets with Reachability Graphs
Szpyrka M.
Fundamenta Informaticae
|
2006
|
Vol. 74, nr 2,3
375-390
EN
RTCP-nets are a subclass of timed coloured Petri nets defined for modelling and analysis of embedded real-time systems. One of the main advantages of strongly bounded RTCP-nets is a possibility to present the set of reachable states of an RTCP-net using a finite reachability and/or coverability graph. These graphs can be used to verify most of the net's properties, including the timing ones. The paper discusses analysis methods based on these graphs. A formal definition of RTCP-nets and a survey of their properties are also presented in the paper.
15
Content available remote D-nets - Petri net form of rule-based systems
Szpyrka M., Szmuc T.
Foundations of Computing and Decision Sciences
|
2006
|
Vol. 31, No. 2
175-190
EN
A formal approach to design and analysis of rule-based systems incorporated into embedded systems is presented in the paper. RTCP-nets, a subclass of timed coloured Petri nets, are used as a modelling language. They enable modelling of embedded systems incorporating an RBS (rule-based system). Such a system is represented as a D-net (decision net) that constitutes the bottom layer of the model. D-nets are used to represent a set of generalized decision rules with non-atomic attribute values. In order to assure reliable and efficient performance, analysis and verification of selected qualitative properties (such as completeness, consistency and optirnality) are carried out. The analysis and verification stage are based on Petri nets analysis methods and are included into the design process. Design and verification are supported by computer tools.
16
Development of embedded systems with RTCP-nets
Szpyrka M.
Elektronika : konstrukcje, technologie, zastosowania
|
2006
|
Vol. 47, nr 10
19-22
EN
Using of formal methods at different stages in the embedded system development process may both increase the quality of developed software and reduce the cost of its testing and the debugging. The presented approach is based on a class of Petri nets called RTCP-nets. The paper focuses on computer tools, that are being developed at AGH University of Science and Technology in Kraków, that support the design and verification of hierarchical RTCP-nets models. A short description of hierarchical RTCP-nets and a survey of main software features are presented in the paper.
PL
Wykorzystanie metod formalnych na różnych etapach wytwarzania systemów wbudowanych może zarówno poprawić jakość końcowego produktu, jak również zredukować koszty testowania tworzonego systemu. Prezentowane podejście jako język modelowania wykorzystuje RTCP-sieci będące klasą sieci Petriego. W artykule skupiono się na praktycznych aspektach wykorzystania tych sieci, ze szczególnym uwzględnieniem narzędzi komputerowych, rozwijanych na AGH w Krakowie, które wspierają projektowanie i weryfikację hierarchicznych RTCP-sieci. Artykuł zawiera krótki opis RTCP-sieci i przegląd najistotniejszych cech rozwijanego oprogramowania.
17
Content available remote A formal approach to modelling of real-time systems using RTCP-nets
Szpyrka M., Szmuc T., Matyasik P., Szmuc W.
Foundations of Computing and Decision Sciences
|
2005
|
Vol. 30, No. 1
61-71
EN
The paper deals with an application of formal methods for modelling of real-time systems. The main objective of this approach is to support development of these systems in order to ensure that the produced software artefacts are correct, as well as to improve the development process. The Real-Time Coloured Petri nets (RTCP-nets), which are a subclass of time coloured Petri nets, are used as a modelling tool. To make the nets more suitable for modelling and analysis RTCP-nets are derived from coloured Petri nets. Applications of RTCP-nets as a modelling and verification tool are strongly supported by the so-called Adder Tools. The formal description of RTCP-nets is not presented here since the paper focuses on the main properties of these and the supporting facilities of the Adder Tools. The approach is illustrated by a practical example, that shows the expressiveness of RTCP-nets for modelling and verification of real-time systems. 1 1Supported by KBN Research Project No 4 T11C 035 24
18
Content available remote Fast and flexible modelling of real-time systems with RTCP-nets
Szpyrka M.
Computer Science
|
2004
|
Vol. 6
81-94
EN
A large number of formalisms has been proposed for real-time systems modelling. However, formal methods are not widely used in industrial software development. Such a situation could be treated as a result of a lack of suitable tools for fast designing of a model, its analysis and modification. RTCP-nets have been defined to facilitate fast modelling of embedded systems incorporating rule-based systems. Computer tools that are being developed for RTCP-nets, use a template mechanism to allow users to design models and manipulate its properties fast and effectively. Both theoretical and practical aspects of RTCP-nets are presented in the paper.
PL
Pomimo różnorodności dostępnych formalizmów wspomagających modelowanie i analizę systemów czasu rzeczywistego, metody formalne nie są powszechnie wykorzystywane w procesie wytwarzania oprogramowania. Przyczyną takiej sytuacji może być brak odpowiednich narzędzi, które umożliwiałyby szybkie stworzenie modelu, jego analizę i łatwą modyfikację. RTCP-sieci zostały zdefiniowane w celu umożliwienia szybkiego modelowania systemów wbudowanych, w szczególności działających przy wykorzystaniu systemów regułowych. Rozwijane narzędzia wspierające wykorzystanie RTCP-sieci wykorzystują mechanizm szablonów umożliwiający szybkie stworzenie modelu i łatwą manipulację jego własnościami. W artykule przedstawiono zarówno teoretyczne, jak i praktyczne aspekty RTCP-sieci.
19
Content available remote Specification of external system behaviour based on D-nets: theoretical aspects and computer tools
Szpyrka M., Szmuc T.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2003
|
T. 7, z. 1-2
275-281
EN
A special subclass of coloured Petri nets (so-called D-nets) is presented in the paper. The concept is based on coloured Petri nets (CP-nets [2]) but special structure of such D-nets allows carrying out very interesting formal analysis. The main advantage of the D-nets is possibility of efficient verification of system requirements, i.e., elimination of ambiguity, inconsistency and incompleteness. Such a specification of requirements is prepared as a decision table with rules patterns and then it is transformed into a D-net and computer software is used for automatic verification of its properties. The relevant definitions and main properties of D-nets are presented, and main features of ADDER tool software designed for D-nets analysis are put forward.
PL
W artykule przedstawiona została podklasa kolorowanych sieci Petriego, tzw. D-sieci. Pojęcie bazuje na kolorowanych sieciach Petriego, ale specyficzna struktura D-sieci pozwala na przeprowadzenie formalnej analizy reprezentowanej przez nie specyfikacji zachowania się systemu. Główną zaletą D-sieci jest możliwość efektywnej weryfikacji specyfikacji wymagań, tj. eliminacji dwuznaczności, niezgodności i niezupełności. Specyfikacja wymagań jest przygotowywana jako tablica decyzyjna zawierająca szablony reguł decyzyjnych, a następnie jest transformowana do postaci D-sieci i automatycznie analizowana z wykorzystaniem odpowiednich narzędzi komputerowych. W artykule przedstawione zostały definicje podstawowych pojęć dotyczących D-sieci oraz główne cechy systemu ADDER - rozwijanego oprogramowania , którego jedną z możliwości jest analiza D-sieci.
20
Content available remote Analysis, verification and design of tabular systems. Logical, algebraic and graphical methods
Ligęza A., Nalepa G. J., Szmuc T., Szpyrka M., Szwed P., Wojnicki I.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2001
|
T. 5, z. 1/2
345-354
EN
This paper is devoted to presentation of certain issues concerning analysis and verification of tabular systems. Such systems constitute an extension of relational databases and attributive decision tables. In order to assure safe and reliable performance of tabular systems, certain logical properties should be verified. The paper provides a logical model of tabular systems and states logical definitions of features such as completeness, consistency with constraints and determinism. Further, an algebraic approach to verification of these properties is proposed. A graphical interpretation and use of some graphical methods is also discussed.
PL
W pracy przedstawiono zagadnienia analizy, weryfikacji i projektowania tablicowych systemów regułowych. Systemy takie stanowią istotne rozszerzenie relacyjnych baz danych i atrybutowych tablic decyzyjnych. Aby zapewnić ich niezawodną i bezpieczną pracę, pewne własności logiczne powinny zostać zweryfikowane. W pracy przedstawiono model logiczny systemów tablicowych oraz podano definicje logiczne własności takich, jak zupełność, zgodność z ograniczeniami i determizm. Zaproponowano elementy algebraicznego podejścia do weryfikacji tych własności. Przedstawiono także ideę zastosowania podejścia graficznego do wspomagania projektowania.
first rewind previous Strona / 2 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.