var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Fftsrg.mit.bme.hu%2Fgamma%2Fpublications%2Fpublications.bib&jsonp=1&theme=side&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Fftsrg.mit.bme.hu%2Fgamma%2Fpublications%2Fpublications.bib&jsonp=1&theme=side\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Fftsrg.mit.bme.hu%2Fgamma%2Fpublications%2Fpublications.bib&jsonp=1&theme=side\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
    2. \n
  2. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
    3. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2025\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Model-based testing of asynchronously communicating distributed controllers using validated mappings to formal representations.\n \n \n \n \n\n\n \n Graics, B.; Mondok, M.; Molnár, V.; and Majzik, I.\n\n\n \n\n\n\n Science of Computer Programming, 242: 103265. 2025.\n \n\n\n\n
\n\n\n\n \n \n \"Model-basedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@article {graics_scp25,\n\ttitle = {Model-based testing of asynchronously communicating distributed controllers using validated mappings to formal representations},\n\tjournal = {Science of Computer Programming},\n\tvolume = {242},\n\tpages = {103265},\n\tyear = {2025},\n\tissn = {0167-6423},\n\tdoi = {10.1016/j.scico.2025.103265},\n\turl = {https://www.sciencedirect.com/science/article/pii/S0167642325000048},\n\tauthor = {Bence Graics and Mil\\'{a}n Mondok and Vince Moln\\'{a}r and Istv\\'{a}n Majzik},\n\tkeywords = {Model-based integration testing, Collaborating statecharts, Asynchronous communication, Validation of verification methods, Hidden formal methods, Tool suite},\n\tabstract = {Programmable controllers are gaining prevalence even in distributed safety-critical applications, e.g., in the railway and aerospace industries. In general, such systems are integrated using various loosely-coupled reactive components and must satisfy critical requirements. Thus, the verification of the design models and systematic testing of the implementation are essential tasks, which can be encumbered by the systems' distributed characteristics. In addition, the correctness of these verification methods is also vital. This paper, on the one hand, presents a model-based integration test generation (MBT) approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then automatically mapped (via a symbolic transition systems formalism – XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta, Spin and nuXmv. The model checkers are utilized to generate tests based on formalized properties adhering to multiple coverage criteria. Furthermore, the paper presents a complementing validation approach for the proposed MBT approach based on demonstrating the semantic equivalence of high-level design models and the derived formal models used by the integrated model checkers for verification and test generation. The approaches are implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.}\n}\n\n
\n
\n\n\n
\n Programmable controllers are gaining prevalence even in distributed safety-critical applications, e.g., in the railway and aerospace industries. In general, such systems are integrated using various loosely-coupled reactive components and must satisfy critical requirements. Thus, the verification of the design models and systematic testing of the implementation are essential tasks, which can be encumbered by the systems' distributed characteristics. In addition, the correctness of these verification methods is also vital. This paper, on the one hand, presents a model-based integration test generation (MBT) approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then automatically mapped (via a symbolic transition systems formalism – XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta, Spin and nuXmv. The model checkers are utilized to generate tests based on formalized properties adhering to multiple coverage criteria. Furthermore, the paper presents a complementing validation approach for the proposed MBT approach based on demonstrating the semantic equivalence of high-level design models and the derived formal models used by the integrated model checkers for verification and test generation. The approaches are implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2024\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Model-Based Testing of Asynchronously Communicating Distributed Controllers.\n \n \n \n\n\n \n Graics, B.; Mondok, M.; Molnár, V.; and Majzik, I.\n\n\n \n\n\n\n In Cámara, J.; and Jongmans, S., editor(s), Formal Aspects of Component Software, pages 23–44, Cham, 2024. Springer Nature Switzerland\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{graics_facs23,\n\tauthor="Graics, Bence and Mondok, Mil{\\'a}n and Moln{\\'a}r, Vince and Majzik, Istv{\\'a}n",\n\teditor="C{\\'a}mara, Javier and Jongmans, Sung-Shik",\n\ttitle="Model-Based Testing of Asynchronously Communicating Distributed Controllers",\n\tbooktitle="Formal Aspects of Component Software",\n\tyear="2024",\n\tpublisher="Springer Nature Switzerland",\n\taddress="Cham",\n\tpages="23--44",\n\tabstract="Programmable controllers are gaining prevalence even in distributed safety-critical infrastructures, e.g., in the railway and aerospace industries. Such systems are generally integrated using multiple loosely-coupled reactive components and must satisfy various critical requirements. Thus, their systematic testing is an essential task, which can be encumbered by their distributed characteristics. This paper presents a model-based integration test generation approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then transformed (via a symbolic transition systems formalism -- XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta and Spin in an automated way. The model checkers are utilized for test generation based on multiple coverage criteria. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.",\n\tisbn="978-3-031-52183-6",\n\tdoi="10.1007/978-3-031-52183-6_2"\n}\n\n
\n
\n\n\n
\n Programmable controllers are gaining prevalence even in distributed safety-critical infrastructures, e.g., in the railway and aerospace industries. Such systems are generally integrated using multiple loosely-coupled reactive components and must satisfy various critical requirements. Thus, their systematic testing is an essential task, which can be encumbered by their distributed characteristics. This paper presents a model-based integration test generation approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then transformed (via a symbolic transition systems formalism – XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta and Spin in an automated way. The model checkers are utilized for test generation based on multiple coverage criteria. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Towards the Formal Verification of SysML v2 Models.\n \n \n \n\n\n \n Molnár, V.; Graics, B.; Vörös, A.; Tonetta, S.; Cristoforetti, L.; Kimberly, G.; Dyer, P.; Giammarco, K.; Koethe, M.; Hester, J.; Smith, J.; and Grimm, C.\n\n\n \n\n\n\n In Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems, of MODELS Companion '24, pages 1086–1095, New York, NY, USA, 2024. Association for Computing Machinery\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings {molnar_graics_modevva24,\n\tauthor = {Moln\\'{a}r, Vince and Graics, Bence and V\\"{o}r\\"{o}s, Andr\\'{a}s and Tonetta, Stefano and Cristoforetti, Luca and Kimberly, Greg and Dyer, Pamela and Giammarco, Kristin and Koethe, Manfred and Hester, John and Smith, Jamie and Grimm, Christoph},\n\ttitle = {Towards the Formal Verification of {SysML v2} Models},\n\tyear = {2024},\n\tisbn = {9798400706226},\n\tpublisher = {Association for Computing Machinery},\n\taddress = {New York, NY, USA},\n\tdoi = {10.1145/3652620.3687820},\n\tabstract = {Systems Modeling Language (SysML) is the de facto standard in the industry for modeling complex systems. SysML v2 is the new version of the language with reworked fundamentals. In this paper, we explore how the new formal semantics of SysML v2 can enable formal verification and various forms of automated reasoning. Formal verification involves mathematically proving the correctness of a system's design with respect to certain specifications or properties. This rigorous approach ensures that models behave as intended under all possible conditions. Through a detailed examination, we demonstrate how five specific tools - Gamma, MP-Firebird, Imandra, SAVVS, and SysMD - can formally analyze SysML v2 models. We show how these tools support the different concepts in the language, as well as the set of features and technologies they provide to users of SysML v2, such as model checking, theorem proving, contract-based design, or automatic fault injections. We propose a workflow for applying formal methods on SysML v2 models, illustrated by example models and artifacts generated by the above tools.},\n\tbooktitle = {Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems},\n\tpages = {1086–1095},\n\tnumpages = {10},\n\tkeywords = {SysML V2, systems modeling, formal methods, verification and validation, automated reasoning, tools},\n\tlocation = {Linz, Austria},\n\tseries = {MODELS Companion '24}\n}\n\n
\n
\n\n\n
\n Systems Modeling Language (SysML) is the de facto standard in the industry for modeling complex systems. SysML v2 is the new version of the language with reworked fundamentals. In this paper, we explore how the new formal semantics of SysML v2 can enable formal verification and various forms of automated reasoning. Formal verification involves mathematically proving the correctness of a system's design with respect to certain specifications or properties. This rigorous approach ensures that models behave as intended under all possible conditions. Through a detailed examination, we demonstrate how five specific tools - Gamma, MP-Firebird, Imandra, SAVVS, and SysMD - can formally analyze SysML v2 models. We show how these tools support the different concepts in the language, as well as the set of features and technologies they provide to users of SysML v2, such as model checking, theorem proving, contract-based design, or automatic fault injections. We propose a workflow for applying formal methods on SysML v2 models, illustrated by example models and artifacts generated by the above tools.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2023\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers.\n \n \n \n\n\n \n Graics, B.; Molnár, V.; and Majzik, I.\n\n\n \n\n\n\n In Cimatti, A.; and Titolo, L., editor(s), Formal Methods for Industrial Critical Systems, pages 76–95, Cham, 2023. Springer Nature Switzerland\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{graics_fmics23,\n\tauthor={Bence Graics and Vince Moln{\\'a}r and Istv{\\'a}n Majzik},\n\teditor="Cimatti, Alessandro and Titolo, Laura",\n\ttitle="Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers",\n\tbooktitle="Formal Methods for Industrial Critical Systems",\n\tyear="2023",\n\tpublisher="Springer Nature Switzerland",\n\taddress="Cham",\n\tpages="76--95",\n\tabstract="Distributed programmable controllers are getting prevalence in critical infrastructure, among others, in railway interlocking systems (RIS). Generally, such systems are integrated using various reactive components and must carry out critical tasks. Accordingly, their systematic testing is vital, which can be hindered by their complexity and distributed nature. This paper presents a model-based test generation approach using hidden formal methods. It is based on the collaborating statechart models of the system components and parametric test coverage criteria configurable by declarative model queries. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then automatically mapped into the inputs of model checker back-ends, namely UPPAAL, Theta and Spin. The model checkers generate tests by traversing the emergent analysis models to cover the elements of the test model as specified by pattern-based model queries. The returned diagnostic traces are then concretized to different execution environments. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on a distributed RIS subsystem under development.",\n\tisbn="978-3-031-43681-9",\n\tdoi="10.1007/978-3-031-43681-9_5"\n}\n\n
\n
\n\n\n
\n Distributed programmable controllers are getting prevalence in critical infrastructure, among others, in railway interlocking systems (RIS). Generally, such systems are integrated using various reactive components and must carry out critical tasks. Accordingly, their systematic testing is vital, which can be hindered by their complexity and distributed nature. This paper presents a model-based test generation approach using hidden formal methods. It is based on the collaborating statechart models of the system components and parametric test coverage criteria configurable by declarative model queries. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then automatically mapped into the inputs of model checker back-ends, namely UPPAAL, Theta and Spin. The model checkers generate tests by traversing the emergent analysis models to cover the elements of the test model as specified by pattern-based model queries. The returned diagnostic traces are then concretized to different execution environments. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on a distributed RIS subsystem under development.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Pragmatic verification and validation of industrial executable SysML models.\n \n \n \n\n\n \n Horváth, B.; Molnár, V.; Graics, B.; Hajdu, Á.; Ráth, I.; Horváth, Á.; Karban, R.; Trancho, G.; and Micskei, Z.\n\n\n \n\n\n\n Systems Engineering, 26(6): 693-714. 2023.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article {horvath_incose_22,\n\tauthor = {Horváth, Benedek and Molnár, Vince and Graics, Bence and Hajdu, Ákos and Ráth, István and Horváth, Ákos and Karban, Robert and Trancho, Gelys and Micskei, Zoltán},\n\ttitle = {Pragmatic verification and validation of industrial executable {SysML} models},\n\tjournal = {Systems Engineering},\n\tvolume = {26},\n\tnumber = {6},\n\tpages = {693-714},\n\tdoi = {10.1002/sys.21679},\n\tabstract = {Abstract In recent years, Model-Based Systems Engineering (MBSE) practices have been applied in various industries to design, simulate and verify complex systems. The verification and validation (V\\&V) of such systems engineering models are crucial to develop high-quality systems. However, this is a challenging problem due to the complexity of the models and semantic differences in how different tools interpret the models, which can undermine the validity of the obtained results if they go undiscovered. To address these issues, we propose (i) a subset of the SysML language for which the practical semantic integrity of tools can be achieved and (ii) a cloud-based V\\&V framework for this subset, lifting verification to an industrial scale. We demonstrate the feasibility of our approach on an industrial-scale model from the aerospace domain and summarize the lessons learned during transitioning formal verification tools to an industrial context.},\n\tyear = {2023}\n}\n\n
\n
\n\n\n
\n Abstract In recent years, Model-Based Systems Engineering (MBSE) practices have been applied in various industries to design, simulate and verify complex systems. The verification and validation (V&V) of such systems engineering models are crucial to develop high-quality systems. However, this is a challenging problem due to the complexity of the models and semantic differences in how different tools interpret the models, which can undermine the validity of the obtained results if they go undiscovered. To address these issues, we propose (i) a subset of the SysML language for which the practical semantic integrity of tools can be achieved and (ii) a cloud-based V&V framework for this subset, lifting verification to an industrial scale. We demonstrate the feasibility of our approach on an industrial-scale model from the aerospace domain and summarize the lessons learned during transitioning formal verification tools to an industrial context.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Integration Test Generation and Formal Verification for Distributed Controllers.\n \n \n \n\n\n \n Graics, B.; and Majzik, I.\n\n\n \n\n\n\n In Renczes, B., editor(s), 30th Minisymposium of the Department of Measurement and Information Systems, pages 1–4, Budapest, Hungary, 2023. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{graics_majzik_minisy23,\n\ttitle = {Integration Test Generation and Formal Verification for Distributed Controllers},\n\tbooktitle = {30th Minisymposium of the Department of Measurement and Information Systems},\n\tyear = {2023},\n \tpages = {1{\\textendash}4},\n% \tpublisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n% \torganization = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n\taddress = {Budapest, Hungary},\n\tauthor = {Bence Graics and Istv{\\'a}n Majzik},\n\teditor = {Bal{\\'a}zs Renczes},\n\tdoi = {10.3311/minisy2023-001}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Component-based specification, design and verification of adaptive systems.\n \n \n \n\n\n \n Graics, B.; Molnár, V.; and Majzik, I.\n\n\n \n\n\n\n Systems Engineering, 26(5): 567-589. 2023.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article {graics_incose_22,\n\ttitle = {Component-based specification, design and verification of adaptive systems},\n\tpublisher = {Wiley Periodicals LLC},\n\tyear = {2023},\n\tauthor = {Bence Graics and Vince Moln{\\'a}r and Istv{\\'a}n Majzik},\n\tjournal = {Systems Engineering},\n\tvolume = {26},\n\tnumber = {5},\n\tpages = {567-589},\n%\tkeywords = {adaptation model, adaptive systems, adaptive contracts, component-based systems engineering, test generation, tool, verification},\n\tdoi = {10.1002/sys.21675},\n\tabstract = {Abstract Control systems are typically tightly embedded into their environment to enable adaptation to environmental effects. As the complexity of such adaptive systems is rapidly increasing, there is a strong need for coherent tool-centric approaches to aid their systematic development. This paper proposes an end-to-end component-based specification, design and verification approach for adaptive systems based on the integration of a high-level scenario language (sequence chart variant) and an adaptation definition language (statechart extension) in the open source Gamma tool. The scenario language supports high-level constructs for specifying contracts and the adaptation definition language supports the flexible activation and deactivation of static contracts and managed elements (state-based components) based on internal changes (e.g., faults), environmental changes (e.g., varying context) or interactions. The approach supports linking managed elements to static contracts to formally verify their adherence to the specified behavior at design time using integrated model checkers. Implementation can be derived from the adaptation model automatically, which can be tested using automated test generation and verified at runtime by contract-based monitors.} \n}\n\n
\n
\n\n\n
\n Abstract Control systems are typically tightly embedded into their environment to enable adaptation to environmental effects. As the complexity of such adaptive systems is rapidly increasing, there is a strong need for coherent tool-centric approaches to aid their systematic development. This paper proposes an end-to-end component-based specification, design and verification approach for adaptive systems based on the integration of a high-level scenario language (sequence chart variant) and an adaptation definition language (statechart extension) in the open source Gamma tool. The scenario language supports high-level constructs for specifying contracts and the adaptation definition language supports the flexible activation and deactivation of static contracts and managed elements (state-based components) based on internal changes (e.g., faults), environmental changes (e.g., varying context) or interactions. The approach supports linking managed elements to static contracts to formally verify their adherence to the specified behavior at design time using integrated model checkers. Implementation can be derived from the adaptation model automatically, which can be tested using automated test generation and verified at runtime by contract-based monitors.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Integration test generation for state-based components in the Gamma framework.\n \n \n \n\n\n \n Graics, B.; Molnár, V.; and Majzik, I.\n\n\n \n\n\n\n . 2022.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article {graics_isse_22,\n\ttitle = {Integration test generation for state-based components in the {Gamma} framework},\n\tpublisher = {Springer},\n\tyear = {2022},\n\tauthor = {Bence Graics and Vince Moln{\\'a}r and Istv{\\'a}n Majzik}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Model-Driven Development of Heterogeneous Cyber-Physical Systems.\n \n \n \n\n\n \n Csuvarszki, C.; Graics, B.; and Vörös, A.\n\n\n \n\n\n\n In Renczes, B., editor(s), 28th Minisymposium of the Department of Measurement and Information Systems, Budapest, Hungary, 2021. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {csuvarszki_graics_minisy21,\n\ttitle = {Model-Driven Development of Heterogeneous Cyber-Physical Systems},\n\tbooktitle = {28th Minisymposium of the Department of Measurement and Information Systems},\n\tyear = {2021},\n% \tpages = {25{\\textendash}28},\n% \tpublisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n% \torganization = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n\taddress = {Budapest, Hungary},\n\tauthor = {Csan{\\'a}d Csuvarszki and Bence Graics and Andr{\\'a}s V{\\"o}r{\\"o}s},\n\teditor = {Bal{\\'a}zs Renczes}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Contract-Based Specification and Test Generation for Adaptive Systems.\n \n \n \n\n\n \n Graics, B.; Molnár, V.; and Majzik, I.\n\n\n \n\n\n\n In 16th International Conference on Dependability of Computer Systems (DepCoS-RELCOMEX), volume 1389, of Advances in Intelligent Systems and Computing, pages 136-145, Wrocław, Poland, 2021. Springer, Springer\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {graics_depcos_21,\n\ttitle = {Contract-Based Specification and Test Generation for Adaptive Systems},\n\tbooktitle = {16th International Conference on Dependability of Computer Systems (DepCoS-RELCOMEX)},\n\tseries = {Advances in Intelligent Systems and Computing},\n\tvolume = {1389},\n\tyear = {2021},\n\tpages = {136-145},\n\tpublisher = {Springer},\n\torganization = {Springer},\n\taddress = {Wroc{\\l}aw, Poland},\n\tdoi = {10.1007/978-3-030-76773-0},\n\tauthor = {Bence Graics and Vince Moln{\\'a}r and Istv{\\'a}n Majzik}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Towards Simulation of CubeSat Operational Scenarios under a Cyber-Physical Systems View.\n \n \n \n\n\n \n de Almeida, D. P.; Graics, B.; Chagas, R. A. J.; de Sousa, F. L.; and Mattiello-Francisco, F.\n\n\n \n\n\n\n In 10th Latin-American Symposium on Dependable Computing (LADC 2021), Florianópolis, Brazil, 2021. IEEE, IEEE\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {almeida_graics_ladc_21,\n\ttitle = {Towards Simulation of {CubeSat} Operational Scenarios under a Cyber-Physical Systems View},\n\tbooktitle = {10th Latin-American Symposium on Dependable Computing (LADC 2021)},\n\tyear = {2021},\n\tpublisher = {IEEE},\n\torganization = {IEEE},\n\taddress = {Florian{\\'o}polis, Brazil},\n\tdoi = {10.1109/LADC53747.2021.9672594},\n%\turl = {https://ieeexplore.ieee.org/document/9672594},\n\tauthor = {Danilo Pallamin de Almeida and Bence Graics and Ronan Arraes Jardim Chagas and Fabiano Luis de Sousa and Fatima Mattiello-Francisco}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Simulation-based Safety Assessment of High-level Reliability Models.\n \n \n \n \n\n\n \n Nagy, S. J.; Graics, B.; Kristóf, M.; and Vörös, A.\n\n\n \n\n\n\n In 4th Workshop on Models for Formal Analysis of Real Systems, pages 240–260, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"Simulation-based pdf\n  \n \n \n \"Simulation-based link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {nagy_mars_20,\n\ttitle = {Simulation-based Safety Assessment of High-level Reliability Models},\n\tbooktitle = {4th Workshop on Models for Formal Analysis of Real Systems},\n\tpages = {240{\\textendash}260},\n\tyear = {2020},\n\tdoi = {10.4204/EPTCS.316.9},\n\tauthor = {Simon J{\\'o}zsef Nagy and Bence Graics and Marussy Krist{\\'o}f and Andr{\\'a}s V{\\"o}r{\\"o}s},\n\turl_pdf = {https://arxiv.org/pdf/2004.13290},\n\turl_link = {https://arxiv.org/abs/2004.13290}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Model Checking as a Service: Towards Pragmatic Hidden Formal Methods.\n \n \n \n\n\n \n Horváth, B.; Graics, B.; Hajdu, Á.; Micskei, Z.; Molnár, V.; Ráth, I.; Andolfato, L.; Gomes, I.; and Karban, R.\n\n\n \n\n\n\n In Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, pages 1–5, 2020. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 8 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {horvath_openmbee20,\n\ttitle = {Model Checking as a Service: Towards Pragmatic Hidden Formal Methods},\n\tbooktitle = {Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings},\n\tpages = {1{\\textendash}5},\n\tyear = {2020},\n\tdoi = {10.1145/3417990.3421407},\n\tauthor = {Benedek Horv{\\'a}th and Bence Graics and {\\'A}kos Hajdu and Zolt{\\'a}n Micskei and Vince Moln{\\'a}r and Istv{\\'a}n R{\\'a}th and Luigi Andolfato and Ivan Gomes and Robert Karban}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modeling and Analysis of an Industrial Communication Protocol in the Gamma Framework.\n \n \n \n \n\n\n \n Graics, B.; and Majzik, I.\n\n\n \n\n\n\n In Renczes, B., editor(s), 27th Minisymposium of the Department of Measurement and Information Systems, pages 25–28, Budapest, Hungary, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"Modeling pdf\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {graics_majzik_minisy20,\n\ttitle = {Modeling and Analysis of an Industrial Communication Protocol in the {Gamma} Framework},\n\tbooktitle = {27th Minisymposium of the Department of Measurement and Information Systems},\n\tyear = {2020},\n \tpages = {25{\\textendash}28},\n% \tpublisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n% \torganization = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n\taddress = {Budapest, Hungary},\n\tauthor = {Bence Graics and Istv{\\'a}n Majzik},\n\teditor = {Bal{\\'a}zs Renczes},\n\turl_pdf = {https://inf.mit.bme.hu/sites/default/files/gamma/documents/Minisy2020_Graics.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Mixed-Semantics Composition of Statecharts for the Component-Based Design of Reactive Systems.\n \n \n \n \n\n\n \n Graics, B.; Molnár, V.; Vörös, A.; Majzik, I.; and Varró, D.\n\n\n \n\n\n\n Software and Systems Modeling, 19: 1483–1517. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"Mixed-Semantics link\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article {graics_sosym_20,\n\ttitle = {Mixed-Semantics Composition of Statecharts for the Component-Based Design of Reactive Systems},\n\tjournal = {Software and Systems Modeling},\n\tvolume = {19},\n\tyear = {2020},\n \tpages = {1483{\\textendash}1517},\n\tpublisher = {Springer},\n\tchapter = {1483},\n%\tkeywords = {component-based design, composition language, formal semantics, formal verification, statecharts, mine},\n\tdoi = {10.1007/s10270-020-00806-5},\n\tauthor = {Bence Graics and Vince Moln{\\'a}r and Andr{\\'a}s V{\\"o}r{\\"o}s and Istv{\\'a}n Majzik and D{\\'a}niel Varr{\\'o}},\n\turl_link = {https://link.springer.com/article/10.1007/s10270-020-00806-5}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Mix-and-Match Composition in the Gamma Framework.\n \n \n \n \n\n\n \n Graics, B.; and Molnár, V.\n\n\n \n\n\n\n In Pataki, B., editor(s), 25th Minisymposium of the Department of Measurement and Information Systems, pages 24–27, Budapest, Hungary, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"Mix-and-Match pdf\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {graics_molnar_minisy18,\n\ttitle = {Mix-and-Match Composition in the {Gamma} Framework},\n\tbooktitle = {25th Minisymposium of the Department of Measurement and Information Systems},\n\tyear = {2018},\n \tpages = {24{\\textendash}27},\n\taddress = {Budapest, Hungary},\n\tisbn = {978-963-313-285-2},\n\tauthor = {Bence Graics and Vince Moln{\\'a}r},\n\teditor = {Pataki, B{\\'e}la},\n\turl_pdf = {https://inf.mit.bme.hu/sites/default/files/publications/minisy2018.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Gamma Statechart Composition Framework.\n \n \n \n \n\n\n \n Molnár, V.; Graics, B.; Vörös, A.; Majzik, I.; and Varró, D.\n\n\n \n\n\n\n In 40th International Conference on Software Engineering (ICSE), pages 113–116, Gothenburg, Sweden, 2018. ACM\n \n\n\n\n
\n\n\n\n \n \n \"The link\n  \n \n \n \"The pdf\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {molnar_et_al_icse18,\n\ttitle = {The {Gamma Statechart Composition Framework}},\n\tbooktitle = {40th International Conference on Software Engineering ({ICSE})},\n\tyear = {2018},\n\tpages = {113{\\textendash}116},\n\tpublisher = {ACM},\n\taddress = {Gothenburg, Sweden},\n\tauthor = {Vince Moln{\\'a}r  and Bence Graics and Andr{\\'a}s V{\\"o}r{\\"o}s and Istv{\\'a}n Majzik and D{\\'a}niel Varr{\\'o}},\n\tdoi = {10.1145/3183440.3183489},\n\turl_link = {https://dl.acm.org/doi/10.1145/3183440.3183489},\n\turl_pdf = {https://inf.mit.bme.hu/sites/default/files/publications/icse18.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Mixed-Semantics Composition of Statecharts for the Model-Driven Design of Reactive Systems.\n \n \n \n \n\n\n \n Graics, B.\n\n\n \n\n\n\n 2018.\n Master's Thesis, Budapest University of Technology and Economics\n\n\n\n
\n\n\n\n \n \n \"Mixed-Semantics pdf\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{graics-bence-msc,\n\tauthor = {Graics, Bence},\n\ttitle = {Mixed-Semantics Composition of Statecharts for the Model-Driven Design of Reactive Systems},\n\tnote = {Master's Thesis, Budapest University of Technology and Economics},\n\tyear = {2018},\n\ttype = {Thesis},\n\turl_pdf = {https://inf.mit.bme.hu/sites/default/files/gamma/documents/MSc2018_Graics.pdf},\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Formal Compositional Semantics for Yakindu Statecharts.\n \n \n \n \n\n\n \n Graics, B.; and Molnár, V.\n\n\n \n\n\n\n In Pataki, B., editor(s), 24th Minisymposium of the Department of Measurement and Information Systems, pages 22–25, Budapest, Hungary, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"Formal pdf\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings {graics_molnar_minisy17,\n\ttitle = {Formal Compositional Semantics for {Yakindu} Statecharts},\n\tbooktitle = {24th Minisymposium of the Department of Measurement and Information Systems},\n\tyear = {2017},\n \tpages = {22{\\textendash}25},\n\taddress = {Budapest, Hungary},\n\tisbn = {978-963-313-243-2},\n\tauthor = {Bence Graics and Vince Moln{\\'a}r},\n\teditor = {Pataki, B{\\'e}la},\n\turl_pdf = {https://inf.mit.bme.hu/sites/default/files/gamma/documents/Minisy2017_Graics.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);