This page has only limited features, please log in for full access.

Unclaimed
Marcin Szpyrka
Department of Applied Computer Science, Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering, AGH University of Science and Technology, 30-059 Krakow, Poland

Honors and Awards

The user has no records in this section


Career Timeline

The user has no records in this section.


Short Biography

The user biography is not available.
Following
Followers
Co Authors
The list of users this user is following is empty.
Following: 0 users

Feed

Journal article
Published: 15 December 2020 in Energies
Reads 0
Downloads 0

Conformance checking is a process mining technique that compares a process model with an event log of the same process to check whether the current execution stored in the log conforms to the model and vice versa. This paper deals with the conformance checking of a longwall shearer process. The approach uses place-transition Petri nets with inhibitor arcs for modeling purposes. We use event log files collected from a few coal mines located in Poland by Famur S.A., one of the global suppliers of coal mining machines. One of the main advantages of the approach is the possibility for both offline and online analysis of the log data. The paper presents a detailed description of the longwall process, an original formal model we developed, selected elements of the approach’s implementation and the results of experiments.

ACS Style

Marcin Szpyrka; Edyta Brzychczy; Aneta Napieraj; Jacek Korski; Grzegorz J. Nalepa. Conformance Checking of a Longwall Shearer Operation Based on Low-Level Events. Energies 2020, 13, 6630 .

AMA Style

Marcin Szpyrka, Edyta Brzychczy, Aneta Napieraj, Jacek Korski, Grzegorz J. Nalepa. Conformance Checking of a Longwall Shearer Operation Based on Low-Level Events. Energies. 2020; 13 (24):6630.

Chicago/Turabian Style

Marcin Szpyrka; Edyta Brzychczy; Aneta Napieraj; Jacek Korski; Grzegorz J. Nalepa. 2020. "Conformance Checking of a Longwall Shearer Operation Based on Low-Level Events." Energies 13, no. 24: 6630.

Journal article
Published: 22 April 2019 in Entropy
Reads 0
Downloads 0

Modern cars are equipped with plenty of electronic devices called Electronic Control Units (ECU). ECUs collect diagnostic data from a car’s components such as the engine, brakes etc. These data are then processed, and the appropriate information is communicated to the driver. From the point of view of safety of the driver and the passengers, the information about the car faults is vital. Regardless of the development of on-board computers, only a small amount of information is passed on to the driver. With the data mining approach, it is possible to obtain much more information from the data than it is provided by standard car equipment. This paper describes the environment built by the authors for data collection from ECUs. The collected data have been processed using parameterized entropies and data mining algorithms. Finally, we built a classifier able to detect a malfunctioning thermostat even if the car equipment does not indicate it.

ACS Style

Bartosz Kowalik; Marcin Szpyrka. An Entropy-Based Car Failure Detection Method Based on Data Acquisition Pipeline. Entropy 2019, 21, 426 .

AMA Style

Bartosz Kowalik, Marcin Szpyrka. An Entropy-Based Car Failure Detection Method Based on Data Acquisition Pipeline. Entropy. 2019; 21 (4):426.

Chicago/Turabian Style

Bartosz Kowalik; Marcin Szpyrka. 2019. "An Entropy-Based Car Failure Detection Method Based on Data Acquisition Pipeline." Entropy 21, no. 4: 426.

Journal article
Published: 01 January 2019 in Automatyka/Automatics
Reads 0
Downloads 0

Modern cars are equipped with a lot of electronic devices called Electronic Control Units (ECU). They collect diagnostic data from different car components to control their work, assess the quality of their work and and detect defects. Regardless of the development of on-board computers in cars, only a small amount of information is passed on to the driver. The paper describes how to build a data collecting environment for acquisition real data from a car. The system whose components include an Android based smartphone and Torque PRO application is able to send data via the Internet in real-time to the chosen server. The collected data can be further analysed both on-line and off-line.

ACS Style

Bartosz Kowalik; Marcin Szpyrka. Online environment for data acquisition from car sensors. Automatyka/Automatics 2019, 23, 1 .

AMA Style

Bartosz Kowalik, Marcin Szpyrka. Online environment for data acquisition from car sensors. Automatyka/Automatics. 2019; 23 (1):1.

Chicago/Turabian Style

Bartosz Kowalik; Marcin Szpyrka. 2019. "Online environment for data acquisition from car sensors." Automatyka/Automatics 23, no. 1: 1.

Journal article
Published: 06 December 2018 in IEEE Access
Reads 0
Downloads 0

Alvis is a formal modelling language intended for developing systems consisting of concurrently operating units (realtime, embedded and distributed systems). The paper describes the timed version of Alvis that is suitable for modelling discrete-time systems. The paper is the first relatively complete description of timed Alvis. We present formal definition and semantics of timed models, the algorithm of Labelled Transition Systems generation and introduce computer software we developed to support Alvis. All concepts are illustrated by examples.

ACS Style

Marcin Szpyrka; Michal Wypych; Jerzy Biernacki; Lukasz Podolski. Discrete-Time Systems Modeling and Verification With Alvis Language and Tools. IEEE Access 2018, 6, 78766 -78779.

AMA Style

Marcin Szpyrka, Michal Wypych, Jerzy Biernacki, Lukasz Podolski. Discrete-Time Systems Modeling and Verification With Alvis Language and Tools. IEEE Access. 2018; 6 (99):78766-78779.

Chicago/Turabian Style

Marcin Szpyrka; Michal Wypych; Jerzy Biernacki; Lukasz Podolski. 2018. "Discrete-Time Systems Modeling and Verification With Alvis Language and Tools." IEEE Access 6, no. 99: 78766-78779.

Chapter
Published: 06 August 2017 in Health Informatics: A Computational Perspective in Healthcare
Reads 0
Downloads 0

Alvis is a formal language specifically intended for modelling systems consisting of concurrently operating units. By default, the time dependencies of the modelled system are taken into account, what is expressed by the possibility of determining the duration of each statement performed by the model components. This makes Alvis suitable for modelling and verification of real-time systems. The paper focuses on Alvis time models. The article outlines the syntax and semantics of such models, and discusses the main issues related to the generation of Labelled Transition Systems for time models. Particular attention was paid to tools that support the verification process.

ACS Style

Marcin Szpyrka; Łukasz Podolski; Michał Wypych. Modelling and Verification of Real-Time Systems with Alvis. Health Informatics: A Computational Perspective in Healthcare 2017, 733, 165 -178.

AMA Style

Marcin Szpyrka, Łukasz Podolski, Michał Wypych. Modelling and Verification of Real-Time Systems with Alvis. Health Informatics: A Computational Perspective in Healthcare. 2017; 733 ():165-178.

Chicago/Turabian Style

Marcin Szpyrka; Łukasz Podolski; Michał Wypych. 2017. "Modelling and Verification of Real-Time Systems with Alvis." Health Informatics: A Computational Perspective in Healthcare 733, no. : 165-178.

Conference paper
Published: 24 May 2017 in Transactions on Petri Nets and Other Models of Concurrency XV
Reads 0
Downloads 0

The paper presents a method of using the Alvis formal modelling language and related software to model and simulate multi-agent systems. The approach has been illustrated with an example of a railway traffic management system for a real train station. One of the main advantages of this approach is the possibility of including artificial intelligence (AI) systems encoded in Haskell into Alvis models. Moreover, Alvis models can be developed at the level very close to the final implementation of the corresponding real system. Thus simulation logs can be treated as a virtual prototype logs.

ACS Style

Marcin Szpyrka; Piotr Matyasik; Łukasz Podolski; Michał Wypych. Simulation of Multi-agent Systems with Alvis Toolkit. Transactions on Petri Nets and Other Models of Concurrency XV 2017, 599 -608.

AMA Style

Marcin Szpyrka, Piotr Matyasik, Łukasz Podolski, Michał Wypych. Simulation of Multi-agent Systems with Alvis Toolkit. Transactions on Petri Nets and Other Models of Concurrency XV. 2017; ():599-608.

Chicago/Turabian Style

Marcin Szpyrka; Piotr Matyasik; Łukasz Podolski; Michał Wypych. 2017. "Simulation of Multi-agent Systems with Alvis Toolkit." Transactions on Petri Nets and Other Models of Concurrency XV , no. : 599-608.

Journal article
Published: 26 February 2017 in Symmetry
Reads 0
Downloads 0

This article presents a new method of risk propagation among associated elements. On thebasis of coloured Petri nets, a new class called propagation nets is defined. This class providesa formal model of a risk propagation. The proposed method allows for model relations betweennodes forming the network structure. Additionally, it takes into account the bidirectional relationsbetween components as well as relations between isomorphic, symmetrical components in variousbranches of the network. This method is agnostic in terms of use in various systems and it canbe adapted to the propagation model of any systems’ characteristics; however, it is intentionallyproposed to assess the risk of critical infrastructures. In this paper, as a proof of concept example, weshow the formal model of risk propagation proposed within the project Cyberspace Security ThreatsEvaluation System of the Republic of Poland. In the article, the idea of the method is presented aswell as its use case for evaluation of risk for cyber threats. With the adaptation of Petri nets, it ispossible to evaluate the risk for the particular node and assess the impact of this risk for all relatednodes including hierarchic relations of components as well as isomorphism of elements.

ACS Style

Marcin Szpyrka; Bartosz Jasiul. Evaluation of Cyber Security and Modelling of Risk Propagation with Petri Nets. Symmetry 2017, 9, 32 .

AMA Style

Marcin Szpyrka, Bartosz Jasiul. Evaluation of Cyber Security and Modelling of Risk Propagation with Petri Nets. Symmetry. 2017; 9 (3):32.

Chicago/Turabian Style

Marcin Szpyrka; Bartosz Jasiul. 2017. "Evaluation of Cyber Security and Modelling of Risk Propagation with Petri Nets." Symmetry 9, no. 3: 32.

Journal article
Published: 01 January 2017 in Informatica
Reads 0
Downloads 0
ACS Style

Marcin Szpyrka; Grzegorz J. Nalepa; Krzysztof Kluza. From Process Models to Concurrent Systems in Alvis Language. Informatica 2017, 28, 525 -545.

AMA Style

Marcin Szpyrka, Grzegorz J. Nalepa, Krzysztof Kluza. From Process Models to Concurrent Systems in Alvis Language. Informatica. 2017; 28 (3):525-545.

Chicago/Turabian Style

Marcin Szpyrka; Grzegorz J. Nalepa; Krzysztof Kluza. 2017. "From Process Models to Concurrent Systems in Alvis Language." Informatica 28, no. 3: 525-545.

Journal article
Published: 01 September 2016 in Archives of Control Sciences
Reads 0
Downloads 0

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

ACS Style

Marcin Szpyrka; Jerzy Biernacki; Agnieszka Biernacka. Tools and Methods for RTCP-Nets Modeling and Verification. Archives of Control Sciences 2016, 26, 339 -365.

AMA Style

Marcin Szpyrka, Jerzy Biernacki, Agnieszka Biernacka. Tools and Methods for RTCP-Nets Modeling and Verification. Archives of Control Sciences. 2016; 26 (3):339-365.

Chicago/Turabian Style

Marcin Szpyrka; Jerzy Biernacki; Agnieszka Biernacka. 2016. "Tools and Methods for RTCP-Nets Modeling and Verification." Archives of Control Sciences 26, no. 3: 339-365.

Journal article
Published: 02 February 2016 in Fundamenta Informaticae
Reads 0
Downloads 0
ACS Style

Jan G. Bazan; Marcin Szpyrka; Adam Szczur; Lukasz Dydo; Hubert Wojtowicz. Classifiers for Behavioral Patterns Identification Induced from Huge Temporal Data. Fundamenta Informaticae 2016, 143, 19 -34.

AMA Style

Jan G. Bazan, Marcin Szpyrka, Adam Szczur, Lukasz Dydo, Hubert Wojtowicz. Classifiers for Behavioral Patterns Identification Induced from Huge Temporal Data. Fundamenta Informaticae. 2016; 143 (1-2):19-34.

Chicago/Turabian Style

Jan G. Bazan; Marcin Szpyrka; Adam Szczur; Lukasz Dydo; Hubert Wojtowicz. 2016. "Classifiers for Behavioral Patterns Identification Induced from Huge Temporal Data." Fundamenta Informaticae 143, no. 1-2: 19-34.

Journal article
Published: 20 April 2015 in Entropy
Reads 0
Downloads 0

Data mining is an interdisciplinary subfield of computer science involving methods at the intersection of artificial intelligence, machine learning and statistics. One of the data mining tasks is anomaly detection which is the analysis of large quantities of data to identify items, events or observations which do not conform to an expected pattern. Anomaly detection is applicable in a variety of domains, e.g., fraud detection, fault detection, system health monitoring but this article focuses on application of anomaly detection in the field of network intrusion detection.The main goal of the article is to prove that an entropy-based approach is suitable to detect modern botnet-like malware based on anomalous patterns in network. This aim is achieved by realization of the following points: (i) preparation of a concept of original entropy-based network anomaly detection method, (ii) implementation of the method, (iii) preparation of original dataset, (iv) evaluation of the method.

ACS Style

Przemysław Bereziński; Bartosz Jasiul; Marcin Szpyrka. An Entropy-Based Network Anomaly Detection Method. Entropy 2015, 17, 2367 -2408.

AMA Style

Przemysław Bereziński, Bartosz Jasiul, Marcin Szpyrka. An Entropy-Based Network Anomaly Detection Method. Entropy. 2015; 17 (4):2367-2408.

Chicago/Turabian Style

Przemysław Bereziński; Bartosz Jasiul; Marcin Szpyrka. 2015. "An Entropy-Based Network Anomaly Detection Method." Entropy 17, no. 4: 2367-2408.

Conference paper
Published: 01 January 2015 in INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015)
Reads 0
Downloads 0

Alvis is a formal language that combines graphical modelling of interconnections between system entities (called agents) and a high level programming language to describe behaviour of any individual agent. An Alvis model can be verified formally with model checking techniques applied to the model LTS graph that represents the model state space. This paper presents transformation of an Alvis model into executable Java code. Thus, the approach provides a method of automatic generation of a Java application from formally verified Alvis model.

ACS Style

Piotr Matyasik; Marcin Szpyrka; Michał Wypych. Generation of Java code from Alvis model. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 2015, 1702, 100013 .

AMA Style

Piotr Matyasik, Marcin Szpyrka, Michał Wypych. Generation of Java code from Alvis model. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015). 2015; 1702 (1):100013.

Chicago/Turabian Style

Piotr Matyasik; Marcin Szpyrka; Michał Wypych. 2015. "Generation of Java code from Alvis model." INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 1702, no. 1: 100013.

Conference paper
Published: 01 January 2015 in INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015)
Reads 0
Downloads 0

The paper deals with an algorithm of translation of RTCP-nets’ (real-time coloured Petri nets) coverability graphs into nuXmv state machines. The approach enables users to verify RTCP-nets with model checking techniques provided by the nuXmv tool. Full details of the algorithm are presented and an illustrative example of the approach usefulness is provided.

ACS Style

Agnieszka Biernacka; Jerzy Biernacki; Marcin Szpyrka. State-based verification of RTCP-nets with nuXmv. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 2015, 1702, 100011 .

AMA Style

Agnieszka Biernacka, Jerzy Biernacki, Marcin Szpyrka. State-based verification of RTCP-nets with nuXmv. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015). 2015; 1702 (1):100011.

Chicago/Turabian Style

Agnieszka Biernacka; Jerzy Biernacki; Marcin Szpyrka. 2015. "State-based verification of RTCP-nets with nuXmv." INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 1702, no. 1: 100011.

Conference paper
Published: 01 January 2015 in INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015)
Reads 0
Downloads 0

Alvis is a formal modelling language that enables possibility of verification of distributed concurrent systems. An Alvis model semantics finds expression in an LTS graph (labelled transition system). Execution of any language statement is expressed as a transition between formally defined states of such a model. An LTS graph is generated using a middle-stage Haskell representation of an Alvis model. Moreover, Haskell is used as a part of the Alvis language and is used to define parameters’ types and operations on them. Thanks to the compiler’s modular construction many aspects of compilation of an Alvis model may be modified. Providing new plugins for Alvis Compiler that support languages like Java or C makes possible using these languages as a part of Alvis instead of Haskell. The paper presents the compiler internal model and describes how the default specification language can be altered by new plugins.

ACS Style

Michał Wypych; Marcin Szpyrka; Piotr Matyasik. Extension of Alvis compiler front-end. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 2015, 1702, 100015 .

AMA Style

Michał Wypych, Marcin Szpyrka, Piotr Matyasik. Extension of Alvis compiler front-end. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015). 2015; 1702 (1):100015.

Chicago/Turabian Style

Michał Wypych; Marcin Szpyrka; Piotr Matyasik. 2015. "Extension of Alvis compiler front-end." INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 1702, no. 1: 100015.

Book chapter
Published: 01 January 2015 in Lecture Notes in Electrical Engineering
Reads 0
Downloads 0

We propose a formal modeling method of malicious software that support its detection and countermeasure. In order to detect malware there is a need to posses either digital signatures or behavioral models. As the obfuscation techniques makes the malware almost undetectable the classic signature-based anti-virus tools must be supported by behavioral analysis. A malware hunting tool we developed bases on the formal models in the form of Colored Petri nets and the attitude to modeling is presented in this article.

ACS Style

Bartosz Jasiul; Marcin Szpyrka; Joanna Śliwa. Formal Specification of Malware Models in the Form of Colored Petri Nets. Lecture Notes in Electrical Engineering 2015, 330, 475 -482.

AMA Style

Bartosz Jasiul, Marcin Szpyrka, Joanna Śliwa. Formal Specification of Malware Models in the Form of Colored Petri Nets. Lecture Notes in Electrical Engineering. 2015; 330 ():475-482.

Chicago/Turabian Style

Bartosz Jasiul; Marcin Szpyrka; Joanna Śliwa. 2015. "Formal Specification of Malware Models in the Form of Colored Petri Nets." Lecture Notes in Electrical Engineering 330, no. : 475-482.

Conference paper
Published: 01 January 2015 in INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015)
Reads 0
Downloads 0

The paper presents an RTCP-nets’ (real-time coloured Petri nets) coverability graphs into Aldebaran format translation algorithm. The approach provides the possibility of automatic RTCP-nets verification using model checking techniques provided by the CADP toolbox. An actual fire alarm control panel system has been modelled and several of its crucial properties have been verified to demonstrate the usability of the approach.

ACS Style

Jerzy Biernacki; Agnieszka Biernacka; Marcin Szpyrka. Action-based verification of RTCP-nets with CADP. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 2015, 1702, 100010 .

AMA Style

Jerzy Biernacki, Agnieszka Biernacka, Marcin Szpyrka. Action-based verification of RTCP-nets with CADP. INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015). 2015; 1702 (1):100010.

Chicago/Turabian Style

Jerzy Biernacki; Agnieszka Biernacka; Marcin Szpyrka. 2015. "Action-based verification of RTCP-nets with CADP." INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015) 1702, no. 1: 100010.

Journal article
Published: 19 December 2014 in Entropy
Reads 0
Downloads 0

The aim of this article is to present an approach to develop and verify a method of formal modeling of cyber threats directed at computer systems. Moreover, the goal is to prove that the method enables one to create models resembling the behavior of malware that support the detection process of selected cyber attacks and facilitate the application of countermeasures. The most common cyber threats targeting end users and terminals are caused by malicious software, called malware. The malware detection process can be performed either by matching their digital signatures or analyzing their behavioral models. As the obfuscation techniques make the malware almost undetectable, the classic signature-based anti-virus tools must be supported with behavioral analysis. The proposed approach to modeling of malware behavior is based on colored Petri nets. This article is addressed to cyber defense researchers, security architects and developers solving up-to-date problems regarding the detection and prevention of advanced persistent threats.

ACS Style

Bartosz Jasiul; Marcin Szpyrka; Joanna Sliwa. Detection and Modeling of Cyber Attacks with Petri Nets. Entropy 2014, 16, 6602 -6623.

AMA Style

Bartosz Jasiul, Marcin Szpyrka, Joanna Sliwa. Detection and Modeling of Cyber Attacks with Petri Nets. Entropy. 2014; 16 (12):6602-6623.

Chicago/Turabian Style

Bartosz Jasiul; Marcin Szpyrka; Joanna Sliwa. 2014. "Detection and Modeling of Cyber Attacks with Petri Nets." Entropy 16, no. 12: 6602-6623.

Book chapter
Published: 01 January 2013 in Advances in Intelligent and Soft Computing
Reads 0
Downloads 0

In the paper we present the formal description of the agent-based light sensors (LSA - Light Sensors Agents) serving as data suppliers for a multiagent system controlling the distribution and work parameters of lighting points distributed across a given urban area. The cooperation and behavior of sensor agents are modeled and verified using Alvis modeling language.

ACS Style

Adam Sędziwy; Leszek Kotulski; Marcin Szpyrka. Formal Methods Supporting Agent Aided Smart Lighting Design. Advances in Intelligent and Soft Computing 2013, 170, 225 -239.

AMA Style

Adam Sędziwy, Leszek Kotulski, Marcin Szpyrka. Formal Methods Supporting Agent Aided Smart Lighting Design. Advances in Intelligent and Soft Computing. 2013; 170 ():225-239.

Chicago/Turabian Style

Adam Sędziwy; Leszek Kotulski; Marcin Szpyrka. 2013. "Formal Methods Supporting Agent Aided Smart Lighting Design." Advances in Intelligent and Soft Computing 170, no. : 225-239.

Conference paper
Published: 01 January 2013 in Computer Vision
Reads 0
Downloads 0

We propose a solution which provides a system operator with valuation of security risk introduced by various components of the communication and information system. This risk signature of the system enables the operator to make an informed decision about which network elements shall be used in order to provide a service requested by the user while minimising security risk related to service execution. In considered scenario transmitted data can be intercepted, modified or dropped by an attacker. Each network component and path can be potentially used to compromise information, since an adversary is able to utilise various vulnerabilities of network elements in order to perform an attack. The impact and probability of such successful attacks can be assessed by analysing the severity of the vulnerabilities and the difficulty of exploiting them, including the required equipment and knowledge. In consequence, each possible service work-flow can be assigned a security risk signature.

ACS Style

Marcin Szpyrka; Bartosz Jasiul; Konrad Wrona; Filip Dziedzic. Telecommunications Networks Risk Assessment with Bayesian Networks. Computer Vision 2013, 277 -288.

AMA Style

Marcin Szpyrka, Bartosz Jasiul, Konrad Wrona, Filip Dziedzic. Telecommunications Networks Risk Assessment with Bayesian Networks. Computer Vision. 2013; ():277-288.

Chicago/Turabian Style

Marcin Szpyrka; Bartosz Jasiul; Konrad Wrona; Filip Dziedzic. 2013. "Telecommunications Networks Risk Assessment with Bayesian Networks." Computer Vision , no. : 277-288.

Book chapter
Published: 01 January 2013 in Springer Texts in Business and Economics
Reads 0
Downloads 0

Alvis is a modelling language designed for embedded systems that provides a possibility of a formal model verification. Because of the fact that many embedded systems contain a rule-based system as a part of them, it is necessary to provide a possibility to include such systems into Alvis models. Alvis combines flexible graphical modelling of interconnections among agents with a high level programming language used for the description of agents behaviour. The most natural way of including a rule-based system into an Alvis model is to encode it in the Haskell functional language. Some Haskell features like lazy evaluation, pattern matching, high level functions etc. make it a very attractive proposition from the rule-based systems’ engineering point of view. The paper presents a method of encoding and verification of rule-based systems with Haskell to include them into Alvis models.

ACS Style

Marcin Szpyrka; Tomasz Szmuc. Design and Verification of Rule-Based Systems for Alvis Models. Springer Texts in Business and Economics 2013, 539 -558.

AMA Style

Marcin Szpyrka, Tomasz Szmuc. Design and Verification of Rule-Based Systems for Alvis Models. Springer Texts in Business and Economics. 2013; ():539-558.

Chicago/Turabian Style

Marcin Szpyrka; Tomasz Szmuc. 2013. "Design and Verification of Rule-Based Systems for Alvis Models." Springer Texts in Business and Economics , no. : 539-558.