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 - Bajczi, Levente AU - Telbisz, Csanád Ferenc AU - Somorjai, Márk AU - Ádám, Zsófia AU - Dobos-Kovács, Mihály AU - Szekeres, Dániel AU - Mondok, Milán AU - Molnár, Vince TI - Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 412 EP - 417 PG - 6 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_30 UR - https://m2.mtmt.hu/api/publication/34768428 ID - 34768428 AB - Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support. LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Szekeres, Dániel AU - Mondok, Milán AU - Ádám, Zsófia AU - Somorjai, Márk AU - Telbisz, Csanád Ferenc AU - Dobos-Kovács, Mihály AU - Molnár, Vince TI - EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 371 EP - 375 PG - 5 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_23 UR - https://m2.mtmt.hu/api/publication/34768422 ID - 34768422 AB - Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta , a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta , and its first debut on SV-COMP’24 in the ReachSafety category. 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 - Debreczeni, Máté Imre AU - Klenik, Attila AU - Kocsis, Imre TI - Transaction Conflict Control in Hyperledger Fabric: a Taxonomy, Gaps, and Design for Conflict Prevention JF - IEEE ACCESS J2 - IEEE ACCESS VL - 12 PY - 2024 SP - 18987 EP - 19008 PG - 22 SN - 2169-3536 DO - 10.1109/ACCESS.2024.3361318 UR - https://m2.mtmt.hu/api/publication/34560592 ID - 34560592 N1 - Funding Agency and Grant Number: Cooperation Agreement between the Hungarian National Bank (MNB) and the Budapest University of Technology and Economics (BME) in the Digitization, Artificial Intelligence, and Data Age Workgroup Funding text: No Statement Available AB - The execute-order-validate approach to blockchain consensus, most notably implemented by Hyperledger Fabric, facilitates highly scalable execution of smart contract – in Fabric terminology, ”chaincode” – invocations in cross-organizational blockchains; at the expense of requiring multi-version concurrency control conflict handling during block validation. Consequently, the system-level goodput can be significantly lower than throughput. Although several solutions have been proposed for handling and avoiding conflicts in Hyperledger Fabric, a systematic and holistic approach is missing. We introduce the notion of conflict-controlled operation, propose a novel taxonomy of its means based on the codified principles of dependable computing and categorize the known approaches. Based on this taxonomy, we identified the critical gaps in the state-of-the-art. Design-time conflict prevention is one such gap, and we propose the application of a model-driven engineering process for this purpose. For the last, storage mapping stage of the process, we propose entity attribute partitioning for conflict prevention, describe a data mapper-style chaincode layer and empirically evaluate our solution. Authors LA - English DB - MTMT ER - TY - CHAP AU - Graics, Bence AU - Mondok, Milán AU - Molnár, Vince AU - Majzik, István ED - Jongmans, Sung-Shik ED - Cámara, Javier TI - Model-Based Testing of Asynchronously Communicating Distributed Controllers T2 - Formal Aspects of Component Software PB - Springer Nature Switzerland AG CY - Cham SN - 9783031521836 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 14485. PY - 2024 SP - 23 EP - 44 PG - 22 DO - 10.1007/978-3-031-52183-6_2 UR - https://m2.mtmt.hu/api/publication/34504488 ID - 34504488 N1 - Conference code: 306759 Export Date: 19 February 2024 Correspondence Address: Graics, B.; Department of Measurement and Information Systems, Műegyetem rkp. 3., Hungary; email: graics@mit.bme.hu LA - English DB - MTMT ER - TY - JOUR AU - Babikian, Aren A. AU - Semeráth, Oszkár AU - Varró, Dániel TI - Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search JF - IEEE TRANSACTIONS ON SOFTWARE ENGINEERING J2 - IEEE T SOFTWARE ENG VL - 50 PY - 2024 IS - 1 SP - 48 EP - 68 PG - 21 SN - 0098-5589 DO - 10.1109/TSE.2023.3331254 UR - https://m2.mtmt.hu/api/publication/34375495 ID - 34375495 N1 - Department of Electrical and Computer Engineering, McGill University, Canada Department of Measurement and Information Systems, Budapest University of Technology and Economics, Hungary Export Date: 30 November 2023 CODEN: IESED Funding Agency and Grant Number: NSERC Funding text: No Statement Available AB - Existing safety assurance approaches for autonomous vehicles (AVs) perform system-level safety evaluation by placing the AV-under-test in challenging traffic scenarios captured by abstract scenario specifications and investigated in realistic traffic simulators. As a first step towards scenario-based testing of AVs, the initial scene of a traffic scenario must be concretized. In this context, the scene concretization challenge takes as input a high-level specification of abstract traffic scenes and aims to map them to concrete scenes where exact numeric initial values are defined for each attribute of a vehicle (e.g. position or velocity). In this paper, we propose a traffic scene concretization approach that places vehicles on realistic road maps such that they satisfy an extensible set of abstract constraints defined by an expressive scene specification language which also supports static detection of inconsistencies. Then, abstract constraints are mapped to corresponding numeric constraints, which are solved by metaheuristic search with customizable objective functions and constraint aggregation strategies. We conduct a series of experiments over three realistic road maps to compare eight configurations of our approach with three variations of the state-of-the-art Scenic tool, and to evaluate its scalability. LA - English DB - MTMT ER - TY - JOUR AU - Toldi, Balázs Ádám AU - Kocsis, Imre TI - Blockchain-Based, Confidentiality-Preserving Orchestration of Collaborative Workflows JF - INFOCOMMUNICATIONS JOURNAL J2 - INFOCOMM J VL - 15 PY - 2023 IS - 3 SP - 72 EP - 81 PG - 10 SN - 2061-2079 DO - 10.36244/ICJ.2023.3.8 UR - https://m2.mtmt.hu/api/publication/34292157 ID - 34292157 N1 - Export Date: 14 December 2023 AB - Business process collaboration between independent parties is challenging when participants do not completely trust each other. Tracking actions and enforcing the activity authorizations of participants via blockchain-hosted smart contracts is an emerging solution to this lack of trust, with most state-of-the-art approaches generating the orchestrating smart contract logic from Business Process Model and Notation (BPMN) models. However, compared to centralized business process orchestration services, smart contract state typically leaks potentially sensitive information about the state of the collaboration, limiting the applicability of decentralized process orchestration. This paper presents a novel, collaboration confidentiality-preserving approach where the process orchestrator smart contract only stores encrypted and hashed process states and validates participant actions against a BPMN model using zero-knowledge proofs. We cover a subset of BPMN, which is sufficient from the practical point of view, support messagepassing between participants, and provide an open-source, endto-end prototype implementation that automatically generates the key software artifacts. LA - English DB - MTMT ER - TY - CHAP AU - Graics, Bence AU - Molnár, Vince AU - Majzik, István ED - Titolo, Laura ED - Cimatti, Alessandro TI - Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers T2 - Formal Methods for Industrial Critical Systems PB - Springer Nature Switzerland AG CY - Cham SN - 9783031436819 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 14290. PY - 2023 SP - 76 EP - 95 PG - 20 DO - 10.1007/978-3-031-43681-9_5 UR - https://m2.mtmt.hu/api/publication/34144059 ID - 34144059 N1 - Export Date: 26 October 2023 Correspondence Address: Graics, B.; Department of Measurement and Information Systems, Műegyetem rkp. 3., Hungary; email: graics@mit.bme.hu LA - English DB - MTMT ER - TY - CHAP AU - Augusto, André AU - Belchior, Rafael AU - Kocsis, Imre AU - Gönczy, László AU - Vasconcelos, André AU - Correia, Miguel TI - CBDC Bridging between Hyperledger Fabric and Permissioned EVM-based Blockchains T2 - 2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC) PB - IEEE CY - Piscataway (NJ) SN - 9798350310191 PY - 2023 SP - 1 EP - 9 PG - 9 DO - 10.1109/ICBC56567.2023.10174953 UR - https://m2.mtmt.hu/api/publication/34112239 ID - 34112239 LA - English DB - MTMT ER -