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 - JOUR AU - Semeráth, Oszkár AU - Farkas, Rebeka AU - Bergmann, Gábor AU - Varró, Dániel TI - Diversity of Graph Models and Graph Generators in Mutation Testing JF - INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER J2 - INT J SOFTW TOOLS TECHN TRANSFER VL - 22 PY - 2020 SP - 57 EP - 78 PG - 22 SN - 1433-2779 DO - 10.1007/s10009-019-00530-6 UR - https://m2.mtmt.hu/api/publication/30748493 ID - 30748493 LA - English DB - MTMT ER - TY - JOUR AU - Farkas, Rebeka AU - Tóth, Tamás AU - Hajdu, Ákos AU - Vörös, András TI - Backward reachability analysis for timed automata with data variables JF - ELECTRONIC COMMUNICATIONS OF THE EASST J2 - ELECTR COMMUN EASST VL - 76 PY - 2019 SP - 1 EP - 20 PG - 20 SN - 1863-2122 DO - 10.14279/tuj.eceasst.76.1076.1043 UR - https://m2.mtmt.hu/api/publication/30748705 ID - 30748705 N1 - Scopus:hiba:85121439778 2022-10-12 15:23 év nem egyezik AB - Efficient techniques for reachability analysis of timed automata are zone-based methods that explore the reachable state space from the initial state, and SMT-based methods that perform backward search from the target states. It is also possible to perform backward exploration based on zones, but calculating predecessor states for systems with data variables is computationally expensive, prohibiting the successful application of this approach so far. In this paper we overcome this limitation by combining zone-based backward exploration with the weakest precondition operation for data variables. This combination allows us to handle diagonal constraints efficiently as opposed to zone-based forward search where most approaches require additional operations to ensure correctness. We demonstrate the applicability and compare the efficiency of the algorithm to existing forward exploration approaches by measurements performed on industrial case studies. Although the large number of states often prevents successful verification, we show that data variables can be efficienlty handled by the weakest precondition operation. This way our new approach complements existing techniques. LA - English DB - MTMT ER - TY - CHAP AU - Farkas, Rebeka AU - Bergmann, Gábor AU - Horváth, Ákos TI - Adaptive Step Size Control for Hybrid CT Simulation without Rollback T2 - Proceedings of the 13th International Modelica Conference, Regensburg, Germany, March 4-6, 2019 PB - Linköping University Electronic Press CY - Linköping SN - 9789176851227 PY - 2019 SP - 503 EP - 512 PG - 10 DO - 10.3384/ecp19157503 UR - https://m2.mtmt.hu/api/publication/30603470 ID - 30603470 LA - English DB - MTMT ER - TY - CHAP AU - Farkas, Rebeka AU - Bergmann, Gábor ED - Pataki, Béla TI - Towards Reliable Benchmarks of Timed Automata T2 - Proceedings of the 25th PhD Mini-Symposium PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789633132852 PY - 2018 SP - 20 EP - 23 PG - 4 UR - https://m2.mtmt.hu/api/publication/3362977 ID - 3362977 AB - The verification of the time-dependent behavior of safety-critical systems is important, as design problems often arise from complex timing conditions. One of the most common formalisms for modeling timed systems is the timed automaton, which introduces clock variables to represent the elapse of time. Various tools and algorithms have been developed for the verification of timed automata. However, it is hard to decide which one to use for a given problem as no exhaustive benchmark of their effectiveness and efficiency can be found in the literature. Moreover, there does not exist a public set of models that can be used as an appropriate benchmark suite. In our work we have collected publicly available timed automaton models and industrial case studies and we used them to compare the efficiency of the algorithms implemented in the Theta model checker. In this paper, we present our preliminary benchmark suite, and demonstrate the results of the performed measurements. LA - English DB - MTMT ER - TY - CHAP AU - Farkas, Rebeka AU - Hajdu, Ákos ED - Pataki, Béla TI - Activity-Based Abstraction Refinement for Timed Systems T2 - Proceedings of the 24th PhD Mini-Symposium PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789633132432 PY - 2017 SP - 18 EP - 21 PG - 4 DO - 10.5281/zenodo.291891 UR - https://m2.mtmt.hu/api/publication/3203890 ID - 3203890 LA - English DB - MTMT ER - TY - CHAP AU - Farkas, Rebeka AU - Vörös, András ED - [sn], null TI - Towards Efficient CEGAR-Based Reachability Analysis of Timed Automata T2 - Proceedings of the 23rd PhD Mini-Symposium PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789633132203 PY - 2016 SP - 10 EP - 13 PG - 4 UR - https://m2.mtmt.hu/api/publication/3234544 ID - 3234544 LA - English DB - MTMT ER -