TY - CHAP AU - Molnár, Vince AU - Graics, Bence AU - Vörös, András AU - Tonetta, Stefano AU - Cristoforetti, Luca AU - Kimberly, Greg AU - Dyer, Pamela AU - Giammarco, Kristin AU - Koethe, Manfred AU - Hester, John AU - Smith, Jamie AU - Grimm, Christoph TI - Towards the Formal Verification of SysML v2 Models T2 - MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9798400706226 PY - 2024 SP - 1086 EP - 1095 PG - 10 DO - 10.1145/3652620.3687820 UR - https://m2.mtmt.hu/api/publication/35500643 ID - 35500643 N1 - Funding Agency and Grant Number: German BMBF [2022-1.2.4-EUREKA-2023-00013, 2022-1.2.4-EUREKA] Funding text: We would like to thank every member of the Formal Methods Working Group who helped us write this paper with their insights and comments. We are also grateful to Ed Seidewitz and Conrad Bock, who never get tired of answering our questions. SysMD received support (GENIAL, KI4BoardNet) from the German BMBF. Gamma received support project no. 2022-1.2.4-EUREKA-2023-00013 under the 2022-1.2.4-EUREKA funding scheme. LA - English DB - MTMT ER - TY - JOUR AU - Somorjai, Márk AU - Dobos-Kovács, Mihály AU - Ádám, Zsófia AU - Bajczi, Levente AU - Vörös, András TI - Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification JF - ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE J2 - ELECTRON PROC THEOR COMPUT SCI VL - 402 PY - 2024 SP - 105 EP - 117 PG - 13 SN - 2075-2180 DO - 10.4204/EPTCS.402.11 UR - https://m2.mtmt.hu/api/publication/33784283 ID - 33784283 N1 - Conference code: 199105 Export Date: 10 May 2024 Funding details: Nemzeti Kutatási, Fejlesztési és Innovaciós Alap, NKFIA Funding text 1: Funding. This research was partially funded by the \\u00DANKP-22-{2,3}-I New National Excellence Program and the 2019-1.3.1-KK-2019-00004 project from the National Research, Development and Innovation Fund of Hungary. AB - Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al. LA - English DB - MTMT ER - TY - CHAP AU - Dobos-Kovács, Mihály AU - Vörös, András ED - Anon, A TI - Evaluation of SMT solvers in abstraction-based software model checking T2 - Proceedings of the 11th Latin-American Symposium on Dependable Computing, LADC '22 PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450397377 PY - 2022 SP - 109 EP - 116 PG - 8 DO - 10.1145/3569902.3570187 UR - https://m2.mtmt.hu/api/publication/33575796 ID - 33575796 N1 - Export Date: 20 February 2023 LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Vörös, András ED - Renczes, Balázs TI - Dependability Modeling of Cyber-Physical Systems in the Gamma Framework T2 - Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789634218722 PY - 2022 SP - 20 EP - 23 PG - 4 UR - https://m2.mtmt.hu/api/publication/32679018 ID - 32679018 LA - English DB - MTMT ER - TY - CHAP AU - Barcsa-Szabó, Áron AU - Várady, Balázs AU - Farkas, Rebeka AU - Molnár, Vince AU - Vörös, András ED - Renczes, Balázs TI - Towards Interactive Learning for Model-based Software Engineering T2 - Proceedings of the 28th PhD Mini-Symposium PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789634218456 PY - 2021 SP - 28 EP - 31 PG - 4 UR - https://m2.mtmt.hu/api/publication/32527201 ID - 32527201 AB - Model-based technologies improve the efficiency of the design and development of IT systems by making it possible to automate verification, code generation and system analysis based on a formal model. A simple way of describing the behavior of systems is state-based modeling, which - due to the advancements of formal analysis techniques in recent years - can be widely and effectively utilized when analyzing systems. A possible way of synthesizing such models is to apply active automata learning algorithms. Acquiring a correct formal model of a system can be challenging because of the different theoretical and practical obstacles of both manual and automated approaches. We propose a semi-automated solution, that applies automata learning to provide an interactive environment for model development. LA - English DB - MTMT ER - TY - CHAP AU - Csuvarszki, János Csanád AU - Graics, Bence AU - Vörös, András ED - Renczes, Balázs TI - Model-Driven Development of Heterogeneous Cyber-Physical Systems T2 - Proceedings of the 28th PhD Mini-Symposium PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789634218456 PY - 2021 SP - 24 EP - 27 PG - 4 UR - https://m2.mtmt.hu/api/publication/31868691 ID - 31868691 AB - Cyber-physical systems (CPS) are becoming more prevalent for the reliable execution of critical tasks, e.g., in the aerospace and medical fields. The development of such systems is challenging, due to the heterogeneity of the components ranging from sensors and embedded controllers to cloud solutions. Model-driven approaches can provide a high-level abstraction to combat the challenges. This paper proposes a model-driven development approach supporting the precise modeling of CPS and the automatic derivation of implementation from the resulting models. The approach introduces a composition semantics tailored to heterogeneous architectures for the precise description of component interactions. Automated code generators allow the execution of standalone software components on real-time controllers and support the synthesis of standalone hardware components, enabling both the derivation of embedded software and the description of logical circuit behavior. Component interactions are supported by multiple communication solutions generally used in critical, real-time embedded systems. The approach is implemented in the Gamma framework and its applicability is demonstrated in two case studies. LA - English DB - MTMT ER - TY - CHAP AU - Dobos-Kovács, Mihály AU - Hajdu, Ákos AU - Vörös, András ED - Andrey, Brito ED - Fernando, Pedone TI - Bitvector Support in the Theta Formal Verification Framework 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 - 01 EP - 08 PG - 8 DO - 10.1109/LADC53747.2021.9672595 UR - https://m2.mtmt.hu/api/publication/32678888 ID - 32678888 LA - English DB - MTMT ER - TY - CHAP AU - Nagy, Simon József AU - Szabó, Richárd AU - Vajda, Mate Levente AU - Vörös, András ED - Andrey, Brito ED - Fernando, Pedone TI - Demonstrator for dependable edge-based cyber-physical systems 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 - 8 PG - 8 DO - 10.1109/LADC53747.2021.9672569 UR - https://m2.mtmt.hu/api/publication/32678847 ID - 32678847 LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Vörös, András TI - Towards formally analyzed Cyber-Physical Systems T2 - Student Forum Proceedings- EDCC 2021 PB - arXiv.org CY - München PY - 2021 SP - 1 EP - 4 PG - 4 UR - https://m2.mtmt.hu/api/publication/32678929 ID - 32678929 LA - English DB - MTMT ER - TY - JOUR AU - Graics, Bence AU - Molnár, Vince AU - Vörös, András AU - Majzik, István AU - Varró, Dániel TI - Mixed-Semantics Composition of Statecharts for the Component-Based Design of Reactive Systems JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 19 PY - 2020 IS - 6 SP - 1483 EP - 1517 PG - 35 SN - 1619-1366 DO - 10.1007/s10270-020-00806-5 UR - https://m2.mtmt.hu/api/publication/31343505 ID - 31343505 N1 - Correspondence Address: Graics, B.; MTA-BME Lendület Cyber-physical Systems Research GroupHungary; email: graics@mit.bme.hu AB - The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous, and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain. LA - English DB - MTMT ER -