@inproceedings{MTMT:32527201, title = {Towards Interactive Learning for Model-based Software Engineering}, url = {https://m2.mtmt.hu/api/publication/32527201}, author = {Barcsa-Szabó, Áron and Várady, Balázs and Farkas, Rebeka and Molnár, Vince and Vörös, András}, booktitle = {Proceedings of the 28th PhD Mini-Symposium}, unique-id = {32527201}, abstract = {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.}, year = {2021}, pages = {28-31}, orcid-numbers = {Molnár, Vince/0000-0002-8204-7595} } @article{MTMT:30748493, title = {Diversity of Graph Models and Graph Generators in Mutation Testing}, url = {https://m2.mtmt.hu/api/publication/30748493}, author = {Semeráth, Oszkár and Farkas, Rebeka and Bergmann, Gábor and Varró, Dániel}, doi = {10.1007/s10009-019-00530-6}, journal-iso = {INT J SOFTW TOOLS TECHN TRANSFER}, journal = {INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER}, volume = {22}, unique-id = {30748493}, issn = {1433-2779}, year = {2020}, eissn = {1433-2787}, pages = {57-78}, orcid-numbers = {Bergmann, Gábor/0000-0002-2556-2582; Varró, Dániel/0000-0002-8790-252X} } @article{MTMT:30748705, title = {Backward reachability analysis for timed automata with data variables}, url = {https://m2.mtmt.hu/api/publication/30748705}, author = {Farkas, Rebeka and Tóth, Tamás and Hajdu, Ákos and Vörös, András}, doi = {10.14279/tuj.eceasst.76.1076.1043}, journal-iso = {ELECTR COMMUN EASST}, journal = {ELECTRONIC COMMUNICATIONS OF THE EASST}, volume = {76}, unique-id = {30748705}, issn = {1863-2122}, abstract = {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.}, keywords = {Reachability analysis; Timed automata; backward exploration; weakest precondition}, year = {2019}, pages = {1-20}, orcid-numbers = {Tóth, Tamás/0000-0001-7176-1278; Hajdu, Ákos/0000-0001-8001-8865} } @inproceedings{MTMT:30603470, title = {Adaptive Step Size Control for Hybrid CT Simulation without Rollback}, url = {https://m2.mtmt.hu/api/publication/30603470}, author = {Farkas, Rebeka and Bergmann, Gábor and Horváth, Ákos}, booktitle = {Proceedings of the 13th International Modelica Conference, Regensburg, Germany, March 4-6, 2019}, doi = {10.3384/ecp19157503}, unique-id = {30603470}, year = {2019}, pages = {503-512}, orcid-numbers = {Bergmann, Gábor/0000-0002-2556-2582} } @inproceedings{MTMT:3362977, title = {Towards Reliable Benchmarks of Timed Automata}, url = {https://m2.mtmt.hu/api/publication/3362977}, author = {Farkas, Rebeka and Bergmann, Gábor}, booktitle = {Proceedings of the 25th PhD Mini-Symposium}, unique-id = {3362977}, abstract = {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.}, year = {2018}, pages = {20-23}, orcid-numbers = {Bergmann, Gábor/0000-0002-2556-2582} } @inproceedings{MTMT:3203890, title = {Activity-Based Abstraction Refinement for Timed Systems}, url = {https://m2.mtmt.hu/api/publication/3203890}, author = {Farkas, Rebeka and Hajdu, Ákos}, booktitle = {Proceedings of the 24th PhD Mini-Symposium}, doi = {10.5281/zenodo.291891}, unique-id = {3203890}, year = {2017}, pages = {18-21}, orcid-numbers = {Hajdu, Ákos/0000-0001-8001-8865} } @inproceedings{MTMT:3234544, title = {Towards Efficient CEGAR-Based Reachability Analysis of Timed Automata}, url = {https://m2.mtmt.hu/api/publication/3234544}, author = {Farkas, Rebeka and Vörös, András}, booktitle = {Proceedings of the 23rd PhD Mini-Symposium}, unique-id = {3234544}, year = {2016}, pages = {10-13} }