TY  - CONF
AU  - Ádám, Zsófia
AU  - Péter, Bertalan Zoltán
AU  - Micskei, Zoltán Imre
AU  - Kocsis, Imre
TI  - Smart Contract in the Loop: Fault Impact Assessment for Distributed Ledger Technologies
T2  - THE 14TH CONFERENCE OF PHD STUDENTS IN COMPUTER SCIENCE
PB  - Szegedi Tudományegyetem, Informatikai Intézet
C1  - Szeged
PY  - 2024
SP  - 15
EP  - 19
PG  - 5
UR  - https://m2.mtmt.hu/api/publication/35306936
ID  - 35306936
AB  - Due to their decentralized and trustless nature, blockchain and distributed ledger technologies are increasingly used in several domains, including critical applications. The behavior of such blockchain-integrated systems is typically driven by smart contracts. However, smart contracts are application-specific software and may, therefore, contain faults with severe system-level impacts. This is especially true in the case of the extensively used Hyperledger Fabric (HLF) platform, where smart contracts are written in general-purpose languages (Java, among others), and applications can go far beyond handling virtual-currency-like assets. In this work, we present a novel formal-verification-based approach to smart contract verification and a high-level empirical model of a HLF platform. Our Smart Contract in the Loop (SCIL) method uses a model checker (Java Pathfinder) to check whether specific error properties hold for a given smart contract, while a predefined combination of platform-level fault modes is active. We facilitate the checking of HLF smart contracts without modification and enable the propagation or non-propagation of platform faults through the smart contracts to the system failure level.
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Elekes, Márton
AU  - Molnár, Vince
AU  - Micskei, Zoltán Imre
TI  - To Do or Not to Do: Semantics and Patterns for Do Activities in UML PSSM State Machines
JF  - IEEE TRANSACTIONS ON SOFTWARE ENGINEERING
J2  - IEEE T SOFTWARE ENG
VL  - 50
PY  - 2024
IS  - 8
SP  - 2124
EP  - 2141
PG  - 18
SN  - 0098-5589
DO  - 10.1109/TSE.2024.3422845
UR  - https://m2.mtmt.hu/api/publication/35133148
ID  - 35133148
N1  - Export Date: 15 July 2024            
            CODEN: IESED            
            Funding text 1: This work was supported by project no. 2019-1.3.1-KK-2019-00004 under the 2019-1.3.1-KK funding scheme, project no. 2022-1.2.4-EUREKA-2023-00013 under the 2022-1.2.4-EUREKA funding scheme, and the \\u00DANKP-23-3-II-BME-362 New National Excellence Program of the Ministry for Culture and Innovation from the source of the National Research, Development and Innovation Fund of Hungary.
AB  - State machines are used in engineering many types of software-intensive systems. UML State Machines extend simple finite state machines with powerful constructs. Among the many extensions, there is one seemingly simple and innocent language construct that fundamentally changes state machines' reactive model of computation: doActivity behaviors. DoActivity behaviors describe behavior that is executed independently from the state machine once entered in a given state, typically modeling complex computation or communication as background tasks. However, the UML specification or textbooks are vague about how the doActivity behavior construct should be appropriately used. This lack of guidance is a severe issue as, when improperly used, doActivities can cause concurrent, non-deterministic bugs that are especially challenging to find and could ruin a seemingly correct software design. The Precise Semantics of UML State Machines (PSSM) specification introduced detailed operational semantics for state machines. To the best of our knowledge, there is no rigorous review yet of doActivity's semantics as specified in PSSM. We analyzed the semantics by collecting evidence from cross-checking the text of the specification, its semantic model and executable test cases, and the simulators supporting PSSM. We synthesized insights about subtle details and emergent behaviors relevant to tool developers and advanced modelers. We reported inconsistencies and missing clarifications in more than 20 issues to the standardization committee. Based on these insights, we studied 11 patterns for doActivities detailing the consequences of using a doActivity in a given situation and discussing countermeasures or alternative design choices. We hope that our analysis of the semantics and the patterns help vendors develop conformant simulators or verification tools and engineers design better state machine models.
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Bajczi, Levente
AU  - Ádám, Zsófia
AU  - Micskei, Zoltán Imre
TI  - ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)
JF  - LECTURE NOTES IN COMPUTER SCIENCE
J2  - LNCS
VL  - 14572
PY  - 2024
SP  - 330
EP  - 334
PG  - 5
SN  - 0302-9743
DO  - 10.1007/978-3-031-57256-2_16
UR  - https://m2.mtmt.hu/api/publication/34768972
ID  - 34768972
AB  - ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Serban, Andrada Alexia
AU  - Micskei, Zoltán Imre
TI  - Application of Mutation testing in Safety-Critical Embedded Systems: A Case Study
JF  - ACTA POLYTECHNICA HUNGARICA
J2  - ACTA POLYTECH HUNG
VL  - 21
PY  - 2024
IS  - 8
SP  - 87
EP  - 106
PG  - 20
SN  - 1785-8860
DO  - 10.12700/APH.21.8.2024.8.5
UR  - https://m2.mtmt.hu/api/publication/34727894
ID  - 34727894
N1  - Export Date: 5 April 2024
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Wilhelm, Imola Mária
AU  - Dékány, Éva Katalin
AU  - Hatvani, István Gábor
AU  - Fröhlich, Georgina
AU  - Micskei, Zoltán Imre
AU  - Pach, Péter Pál
AU  - Toldy, Andrea
AU  - Solymosi, Katalin
AU  - Szentgáli-Tóth, Boldizsár Artúr
AU  - Lengyel, Balázs
TI  - A Fiatal Kutatók Akadémiájának javaslatai a magyarországi fiatal kutatók helyzetének javítására
JF  - MAGYAR TUDOMÁNY
J2  - MAGYAR TUDOMÁNY
VL  - 184
PY  - 2023
IS  - 12
SP  - 1544
EP  - 1565
PG  - 7
SN  - 0025-0325
DO  - 10.1556/2065.184.2023.12.11
UR  - https://m2.mtmt.hu/api/publication/34412830
ID  - 34412830
LA  - Hungarian
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Horváth, Benedek
AU  - Molnár, Vince
AU  - Graics, Bence
AU  - Hajdu, Ákos
AU  - Ráth, István Zoltán
AU  - Horváth, Ákos
AU  - Karban, Robert
AU  - Trancho, Gelys
AU  - Micskei, Zoltán Imre
TI  - Pragmatic verification and validation of industrial executable SysML models
JF  - SYSTEMS ENGINEERING
J2  - SYSTEMS ENG
VL  - 26
PY  - 2023
IS  - 6
SP  - 693
EP  - 714
PG  - 22
SN  - 1098-1241
DO  - 10.1002/sys.21679
UR  - https://m2.mtmt.hu/api/publication/33809830
ID  - 33809830
N1  - IncQuery Labs cPlc., Budapest, Hungary            
            Department of Business Informatics - Software Engineering, Johannes Kepler University Linz, Linz, Austria            
            Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary            
            Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA, United States            
            TMT International Observatory LLC, Pasadena, CA, United States            
            Export Date: 26 May 2023            
            Correspondence Address: Horváth, B.; IncQuery Labs cPlcHungary; email: benedek.horvath@incquerylabs.com
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Elekes, Márton
AU  - Molnár, Vince
AU  - Micskei, Zoltán Imre
TI  - Assessing the specification of modelling language semantics: a study on UML PSSM
JF  - SOFTWARE QUALITY JOURNAL
J2  - SOFTWARE QUAL J
VL  - 31
PY  - 2023
IS  - 2
SP  - 575
EP  - 617
PG  - 43
SN  - 0963-9314
DO  - 10.1007/s11219-023-09617-5
UR  - https://m2.mtmt.hu/api/publication/33677595
ID  - 33677595
N1  - Correspondence Address: Micskei, Z.; Department of Measurement and Information Systems, Müegyetem rkp. 3., Hungary; email: micskeiz@mit.bme.hu
AB  - Modelling languages play a central role in developing complex, critical systems. A precise, comprehensible, and high-quality modelling language specification is essential to all stakeholders using, implementing, or extending the language. Many good practices can be found that improve the understandability or consistency of the languages’ semantics. However, designing a modelling language intended for a large audience is still challenging. In this paper, we investigate the challenges and typical issues with assessing the specifications of behavioural modelling language semantics. Our key insight is that the various stakeholder’s understandings of the language’s semantics are often misaligned, and the semantics defined in various artefacts (simulators, test suites) are inconsistent. Therefore assessment of semantics should focus on identifying and resolving these inconsistencies. To illustrate these challenges and techniques, we assessed parts of a state-of-the-art specification for a general-purpose modelling language, the Precise Semantics of UML State Machines (PSSM). We reviewed the text of the specification, analysed and executed PSSM’s conformance test suite, and categorised our experiences according to questions generally relevant to modelling languages. Finally, we made recommendations for improving the development of future modelling languages by representing the semantic domain and traces more explicitly, applying diverse test design techniques to obtain conformance test suites, and using various tools to support early-phase language design.
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Elekes, Márton
AU  - Micskei, Zoltán Imre
ED  - Andrey, Brito
ED  - Fernando, Pedone
TI  - Towards Testing the UML PSSM Test Suite
T2  - 2021 10th Latin-American Symposium on Dependable Computing (LADC)
PB  - Institute of Electrical and Electronics Engineers (IEEE)
CY  - Piscataway (NJ)
SN  - 9781665478311
PY  - 2021
SP  - 1
EP  - 4
PG  - 4
DO  - 10.1109/LADC53747.2021.9672570
UR  - https://m2.mtmt.hu/api/publication/32616888
ID  - 32616888
N1  - Export Date: 2 May 2022
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Horváth, Benedek
AU  - Graics, Bence
AU  - Hajdu, Ákos
AU  - Micskei, Zoltán Imre
AU  - Molnár, Vince
AU  - Ráth, István Zoltán
AU  - Andolfato, Luigi
AU  - Gomes, Ivan
AU  - Karban, Robert
ED  - Esther, Guerra
ED  - Ludovico, Iovino
TI  - Model checking as a service: Towards pragmatic hidden formal methods
T2  - Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings
PB  - Association for Computing Machinery (ACM)
CY  - New York, New York
SN  - 9781450381352
PY  - 2020
PG  - 5
DO  - 10.1145/3417990.3421407
UR  - https://m2.mtmt.hu/api/publication/31647412
ID  - 31647412
AB  - Executable models can be used to support all engineering activities in Model-Based Systems Engineering. Testing and simulation of such models can provide early feedback about design choices. However, in today's complex systems, failures could arise due to subtle errors that are hard to find without checking all possible execution paths. Formal methods, and especially model checking can uncover such subtle errors, yet their usage in practice is limited due to the specialized expertise and high computing power required. Therefore we created an automated, cloud-based environment that can verify complex reachability properties on SysML State Machines using hidden model checkers. The approach and the prototype is illustrated using an example from the aerospace domain.
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Honfi, Dávid
AU  - Micskei, Zoltán Imre
TI  - White-box software test generation with Microsoft Pex on open source C# projects: A dataset
JF  - DATA IN BRIEF
J2  - DATA BRIEF
VL  - 31
PY  - 2020
PG  - 10
SN  - 2352-3409
DO  - 10.1016/j.dib.2020.105962
UR  - https://m2.mtmt.hu/api/publication/31372840
ID  - 31372840
AB  - The paper presents a dataset on software tests generated using the Microsoft Pex (IntelliTest) test generator tool for 10 open source projects. The projects were selected randomly from popular GitHub repositories written in C#. The selected projects contain 7187 methods from which Pex was able to generate tests for 2596 methods totaling 38,618 lines of code. Data collection was performed on a cloud virtual machine. The dataset presents metrics about the attributes of the selected projects (e.g., cyclomatic complexity or number of external method calls) and the test generation (e.g., statement and branch coverage, number of warnings). This data is compared to an automated isolation technique in the paper Automated Isolation for White-box Test Generation [1]. To the best of our knowledge, this is the largest public dataset about the test generation performance of Microsoft Pex on open source projects. The dataset highlights current practical challenges and can be used as a baseline for new test generation techniques.
LA  - English
DB  - MTMT
ER  -