Skip to content

Commit

Permalink
Update publications.bib
Browse files Browse the repository at this point in the history
  • Loading branch information
@grbeni
grbeni authored Feb 2, 2024
1 parent 24246a0 commit 0b0d9fd
Showing 1 changed file with 62 additions and 45 deletions.
107 changes: 62 additions & 45 deletions publications/publications.bib
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@ @inproceedings {graics_molnar_minisy17
address = {Budapest, Hungary},
isbn = {978-963-313-243-2},
author = {Bence Graics and Vince Moln{\'a}r},
editor = {Pataki, B{\'e}la}
editor = {Pataki, B{\'e}la},
url_pdf = {https://inf.mit.bme.hu/sites/default/files/gamma/documents/Minisy2017_Graics.pdf},
}

@inproceedings {graics_molnar_minisy18,
Expand All @@ -17,7 +18,8 @@ @inproceedings {graics_molnar_minisy18
address = {Budapest, Hungary},
isbn = {978-963-313-285-2},
author = {Bence Graics and Vince Moln{\'a}r},
editor = {Pataki, B{\'e}la}
editor = {Pataki, B{\'e}la},
url_pdf = {https://inf.mit.bme.hu/sites/default/files/publications/minisy2018.pdf}
}

@inproceedings {molnar_et_al_icse18,
Expand All @@ -28,7 +30,9 @@ @inproceedings {molnar_et_al_icse18
publisher = {ACM},
address = {Gothenburg, Sweden},
author = {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}},
doi = {10.1145/3183440.3183489}
doi = {10.1145/3183440.3183489},
url_link = {https://dl.acm.org/doi/10.1145/3183440.3183489},
url_pdf = {https://inf.mit.bme.hu/sites/default/files/publications/icse18.pdf}
}

@inproceedings {nagy_mars_20,
Expand All @@ -37,35 +41,37 @@ @inproceedings {nagy_mars_20
pages = {240{\textendash}260},
year = {2020},
doi = {10.4204/EPTCS.316.9},
author = {Simon J{\'o}zsef Nagy and Bence Graics and Marussy Krist{\'o}f and Andr{\'a}s V{\"o}r{\"o}s}
author = {Simon J{\'o}zsef Nagy and Bence Graics and Marussy Krist{\'o}f and Andr{\'a}s V{\"o}r{\"o}s},
url_pdf = {https://arxiv.org/pdf/2004.13290},
url_link = {https://arxiv.org/abs/2004.13290}
}

@InProceedings{graics_facs23,
author="Graics, Bence and Mondok, Mil{\'a}n and Moln{\'a}r, Vince and Majzik, Istv{\'a}n",
editor="C{\'a}mara, Javier and Jongmans, Sung-Shik",
title="Model-Based Testing of Asynchronously Communicating Distributed Controllers",
booktitle="Formal Aspects of Component Software",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="23--44",
abstract="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.",
isbn="978-3-031-52183-6"
doi="10.1007/978-3-031-52183-6\_2"
author="Graics, Bence and Mondok, Mil{\'a}n and Moln{\'a}r, Vince and Majzik, Istv{\'a}n",
editor="C{\'a}mara, Javier and Jongmans, Sung-Shik",
title="Model-Based Testing of Asynchronously Communicating Distributed Controllers",
booktitle="Formal Aspects of Component Software",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="23--44",
abstract="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.",
isbn="978-3-031-52183-6"
doi="10.1007/978-3-031-52183-6_2"
}

@inproceedings{graics_fmics23,
author={Bence Graics and Vince Moln{\'a}r and Istv{\'a}n Majzik},
editor="Cimatti, Alessandro and Titolo, Laura",
title="Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers",
booktitle="Formal Methods for Industrial Critical Systems",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="76--95",
abstract="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.",
isbn="978-3-031-43681-9",
doi="10.1007/978-3-031-43681-9_5"
author={Bence Graics and Vince Moln{\'a}r and Istv{\'a}n Majzik},
editor="Cimatti, Alessandro and Titolo, Laura",
title="Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers",
booktitle="Formal Methods for Industrial Critical Systems",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="76--95",
abstract="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.",
isbn="978-3-031-43681-9",
doi="10.1007/978-3-031-43681-9_5"
}

@inproceedings {horvath_openmbee20,
Expand All @@ -78,15 +84,15 @@ @inproceedings {horvath_openmbee20
}

@article {horvath_incose_22,
author = {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},
title = {Pragmatic verification and validation of industrial executable {SysML} models},
journal = {Systems Engineering},
volume = {26},
number = {6},
pages = {693-714},
doi = {10.1002/sys.21679},
abstract = {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.},
year = {2023}
author = {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},
title = {Pragmatic verification and validation of industrial executable {SysML} models},
journal = {Systems Engineering},
volume = {26},
number = {6},
pages = {693-714},
doi = {10.1002/sys.21679},
abstract = {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.},
year = {2023}
}

@inproceedings {graics_majzik_minisy20,
Expand All @@ -98,7 +104,8 @@ @inproceedings {graics_majzik_minisy20
% organization = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},
address = {Budapest, Hungary},
author = {Bence Graics and Istv{\'a}n Majzik},
editor = {Bal{\'a}zs Renczes}
editor = {Bal{\'a}zs Renczes},
url_pdf = {https://inf.mit.bme.hu/sites/default/files/gamma/documents/Minisy2020_Graics.pdf}
}

@inproceedings{graics_majzik_minisy23,
Expand All @@ -111,7 +118,7 @@ @inproceedings{graics_majzik_minisy23
address = {Budapest, Hungary},
author = {Bence Graics and Istv{\'a}n Majzik},
editor = {Bal{\'a}zs Renczes},
doi = {10.3311/minisy2023-001}
doi = {10.3311/minisy2023-001}
}

@inproceedings {csuvarszki_graics_minisy21,
Expand All @@ -136,7 +143,8 @@ @article {graics_sosym_20
chapter = {1483},
% keywords = {component-based design, composition language, formal semantics, formal verification, statecharts, mine},
doi = {10.1007/s10270-020-00806-5},
author = {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}}
author = {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}},
url_link = {https://link.springer.com/article/10.1007/s10270-020-00806-5}
}

@article {graics_isse_22,
Expand All @@ -151,13 +159,13 @@ @article {graics_incose_22
publisher = {Wiley Periodicals LLC},
year = {2023},
author = {Bence Graics and Vince Moln{\'a}r and Istv{\'a}n Majzik},
journal = {Systems Engineering},
volume = {26},
number = {5},
pages = {567-589},
% keywords = {adaptation model, adaptive systems, adaptive contracts, component-based systems engineering, test generation, tool, verification},
doi = {10.1002/sys.21675},
abstract = {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.}
journal = {Systems Engineering},
volume = {26},
number = {5},
pages = {567-589},
% keywords = {adaptation model, adaptive systems, adaptive contracts, component-based systems engineering, test generation, tool, verification},
doi = {10.1002/sys.21675},
abstract = {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.}
}

@inproceedings {graics_depcos_21,
Expand Down Expand Up @@ -185,3 +193,12 @@ @inproceedings {almeida_graics_ladc_21
% url = {https://ieeexplore.ieee.org/document/9672594},
author = {Danilo Pallamin de Almeida and Bence Graics and Ronan Arraes Jardim Chagas and Fabiano Luis de Sousa and Fatima Mattiello-Francisco}
}

@misc{graics-bence-msc,
author = {Graics, Bence},
title = {Mixed-Semantics Composition of Statecharts for the Model-Driven Design of Reactive Systems},
note = {Master's Thesis, Budapest University of Technology and Economics},
year = {2018},
type = {Thesis},
url_pdf = {https://inf.mit.bme.hu/sites/default/files/gamma/documents/MSc2018_Graics.pdf},
}

0 comments on commit 0b0d9fd

Please sign in to comment.