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 -