Model-Based Testing of Asynchronously Communicating Distributed Controllers. Graics, B., Mondok, M., Molnár, V., & Majzik, I. In Cámara, J. & Jongmans, S., editors, Formal Aspects of Component Software, pages 23–44, Cham, 2024. Springer Nature Switzerland.
Paper doi abstract bibtex 3 downloads 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.
@InProceedings{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",
url="https://link.springer.com/chapter/10.1007/978-3-031-52183-6_2",
doi="10.1007/978-3-031-52183-6_2"
}
Downloads: 3
{"_id":"z56uT45bg6Lg6zhoW","bibbaseid":"graics-mondok-molnr-majzik-modelbasedtestingofasynchronouslycommunicatingdistributedcontrollers-2024","author_short":["Graics, B.","Mondok, M.","Molnár, V.","Majzik, I."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Graics"],"firstnames":["Bence"],"suffixes":[]},{"propositions":[],"lastnames":["Mondok"],"firstnames":["Milán"],"suffixes":[]},{"propositions":[],"lastnames":["Molnár"],"firstnames":["Vince"],"suffixes":[]},{"propositions":[],"lastnames":["Majzik"],"firstnames":["István"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Cámara"],"firstnames":["Javier"],"suffixes":[]},{"propositions":[],"lastnames":["Jongmans"],"firstnames":["Sung-Shik"],"suffixes":[]}],"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","url":"https://link.springer.com/chapter/10.1007/978-3-031-52183-6_2","doi":"10.1007/978-3-031-52183-6_2","bibtex":"@InProceedings{facs23,\nauthor=\"Graics, Bence\nand Mondok, Mil{\\'a}n\nand Moln{\\'a}r, Vince\nand Majzik, Istv{\\'a}n\",\neditor=\"C{\\'a}mara, Javier\nand Jongmans, Sung-Shik\",\ntitle=\"Model-Based Testing of Asynchronously Communicating Distributed Controllers\",\nbooktitle=\"Formal Aspects of Component Software\",\nyear=\"2024\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"23--44\",\nabstract=\"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.\",\nisbn=\"978-3-031-52183-6\",\nurl=\"https://link.springer.com/chapter/10.1007/978-3-031-52183-6_2\",\ndoi=\"10.1007/978-3-031-52183-6_2\"\n}\n\n","author_short":["Graics, B.","Mondok, M.","Molnár, V.","Majzik, I."],"editor_short":["Cámara, J.","Jongmans, S."],"key":"facs23","id":"facs23","bibbaseid":"graics-mondok-molnr-majzik-modelbasedtestingofasynchronouslycommunicatingdistributedcontrollers-2024","role":"author","urls":{"Paper":"https://link.springer.com/chapter/10.1007/978-3-031-52183-6_2"},"metadata":{"authorlinks":{}},"downloads":3},"bibtype":"inproceedings","biburl":"https://mondokm.github.io/publications.bib","dataSources":["ceR4xqaQusy7vTLW9","aKoGt6pfXxS85NpEf"],"keywords":[],"search_terms":["model","based","testing","asynchronously","communicating","distributed","controllers","graics","mondok","molnár","majzik"],"title":"Model-Based Testing of Asynchronously Communicating Distributed Controllers","year":2024,"downloads":3}