This page has only limited features, please log in for full access.
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.
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 StyleMarcin 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 StyleMarcin 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.
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.
Bartosz Kowalik; Marcin Szpyrka. An Entropy-Based Car Failure Detection Method Based on Data Acquisition Pipeline. Entropy 2019, 21, 426 .
AMA StyleBartosz Kowalik, Marcin Szpyrka. An Entropy-Based Car Failure Detection Method Based on Data Acquisition Pipeline. Entropy. 2019; 21 (4):426.
Chicago/Turabian StyleBartosz Kowalik; Marcin Szpyrka. 2019. "An Entropy-Based Car Failure Detection Method Based on Data Acquisition Pipeline." Entropy 21, no. 4: 426.
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.
Bartosz Kowalik; Marcin Szpyrka. Online environment for data acquisition from car sensors. Automatyka/Automatics 2019, 23, 1 .
AMA StyleBartosz Kowalik, Marcin Szpyrka. Online environment for data acquisition from car sensors. Automatyka/Automatics. 2019; 23 (1):1.
Chicago/Turabian StyleBartosz Kowalik; Marcin Szpyrka. 2019. "Online environment for data acquisition from car sensors." Automatyka/Automatics 23, no. 1: 1.
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.
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 StyleMarcin 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 StyleMarcin 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.
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.
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 StyleMarcin 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 StyleMarcin 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.
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.
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 StyleMarcin 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 StyleMarcin 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.
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.
Marcin Szpyrka; Bartosz Jasiul. Evaluation of Cyber Security and Modelling of Risk Propagation with Petri Nets. Symmetry 2017, 9, 32 .
AMA StyleMarcin Szpyrka, Bartosz Jasiul. Evaluation of Cyber Security and Modelling of Risk Propagation with Petri Nets. Symmetry. 2017; 9 (3):32.
Chicago/Turabian StyleMarcin Szpyrka; Bartosz Jasiul. 2017. "Evaluation of Cyber Security and Modelling of Risk Propagation with Petri Nets." Symmetry 9, no. 3: 32.
Marcin Szpyrka; Grzegorz J. Nalepa; Krzysztof Kluza. From Process Models to Concurrent Systems in Alvis Language. Informatica 2017, 28, 525 -545.
AMA StyleMarcin Szpyrka, Grzegorz J. Nalepa, Krzysztof Kluza. From Process Models to Concurrent Systems in Alvis Language. Informatica. 2017; 28 (3):525-545.
Chicago/Turabian StyleMarcin Szpyrka; Grzegorz J. Nalepa; Krzysztof Kluza. 2017. "From Process Models to Concurrent Systems in Alvis Language." Informatica 28, no. 3: 525-545.
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
Marcin Szpyrka; Jerzy Biernacki; Agnieszka Biernacka. Tools and Methods for RTCP-Nets Modeling and Verification. Archives of Control Sciences 2016, 26, 339 -365.
AMA StyleMarcin 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 StyleMarcin Szpyrka; Jerzy Biernacki; Agnieszka Biernacka. 2016. "Tools and Methods for RTCP-Nets Modeling and Verification." Archives of Control Sciences 26, no. 3: 339-365.
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 StyleJan 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 StyleJan 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.
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.
Przemysław Bereziński; Bartosz Jasiul; Marcin Szpyrka. An Entropy-Based Network Anomaly Detection Method. Entropy 2015, 17, 2367 -2408.
AMA StylePrzemysław Bereziński, Bartosz Jasiul, Marcin Szpyrka. An Entropy-Based Network Anomaly Detection Method. Entropy. 2015; 17 (4):2367-2408.
Chicago/Turabian StylePrzemysław Bereziński; Bartosz Jasiul; Marcin Szpyrka. 2015. "An Entropy-Based Network Anomaly Detection Method." Entropy 17, no. 4: 2367-2408.
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.
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 StylePiotr 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 StylePiotr 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.
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.
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 StyleAgnieszka 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 StyleAgnieszka 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.
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.
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 StyleMichał 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 StyleMichał 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.
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.
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 StyleBartosz 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 StyleBartosz 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.
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.
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 StyleJerzy 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 StyleJerzy 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.
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.
Bartosz Jasiul; Marcin Szpyrka; Joanna Sliwa. Detection and Modeling of Cyber Attacks with Petri Nets. Entropy 2014, 16, 6602 -6623.
AMA StyleBartosz Jasiul, Marcin Szpyrka, Joanna Sliwa. Detection and Modeling of Cyber Attacks with Petri Nets. Entropy. 2014; 16 (12):6602-6623.
Chicago/Turabian StyleBartosz Jasiul; Marcin Szpyrka; Joanna Sliwa. 2014. "Detection and Modeling of Cyber Attacks with Petri Nets." Entropy 16, no. 12: 6602-6623.
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.
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 StyleAdam 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 StyleAdam 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.
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.
Marcin Szpyrka; Bartosz Jasiul; Konrad Wrona; Filip Dziedzic. Telecommunications Networks Risk Assessment with Bayesian Networks. Computer Vision 2013, 277 -288.
AMA StyleMarcin Szpyrka, Bartosz Jasiul, Konrad Wrona, Filip Dziedzic. Telecommunications Networks Risk Assessment with Bayesian Networks. Computer Vision. 2013; ():277-288.
Chicago/Turabian StyleMarcin Szpyrka; Bartosz Jasiul; Konrad Wrona; Filip Dziedzic. 2013. "Telecommunications Networks Risk Assessment with Bayesian Networks." Computer Vision , no. : 277-288.
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.
Marcin Szpyrka; Tomasz Szmuc. Design and Verification of Rule-Based Systems for Alvis Models. Springer Texts in Business and Economics 2013, 539 -558.
AMA StyleMarcin Szpyrka, Tomasz Szmuc. Design and Verification of Rule-Based Systems for Alvis Models. Springer Texts in Business and Economics. 2013; ():539-558.
Chicago/Turabian StyleMarcin Szpyrka; Tomasz Szmuc. 2013. "Design and Verification of Rule-Based Systems for Alvis Models." Springer Texts in Business and Economics , no. : 539-558.