\n

@article{scp25,\ntitle = {Model-based testing of asynchronously communicating distributed controllers using validated mappings to formal representations},\njournal = {Science of Computer Programming},\nvolume = {242},\npages = {103265},\nyear = {2025},\nissn = {0167-6423},\ndoi = {https://doi.org/10.1016/j.scico.2025.103265},\nurl = {https://www.sciencedirect.com/science/article/pii/S0167642325000048},\nauthor = {Bence Graics and Milán Mondok and Vince Molnár and István Majzik},\nkeywords = {Model-based integration testing, Collaborating statecharts, Asynchronous communication, Validation of verification methods, Hidden formal methods, Tool suite},\nabstract = {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 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

@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

\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

@InProceedings{svcomp24-theta,\nauthor="Bajczi, Levente\nand Telbisz, Csan{\\'a}d\nand Somorjai, M{\\'a}rk\nand {\\'A}d{\\'a}m, Zs{\\'o}fia\nand Dobos-Kov{\\'a}cs, Mih{\\'a}ly\nand Szekeres, D{\\'a}niel\nand Mondok, Mil{\\'a}n\nand Moln{\\'a}r, Vince",\neditor="Finkbeiner, Bernd\nand Kov{\\'a}cs, Laura",\ntitle="Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)",\nbooktitle="Tools and Algorithms for the Construction and Analysis of Systems",\nyear="2024",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="412--417",\nabstract="Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.",\nisbn="978-3-031-57256-2",\nurl="https://link.springer.com/chapter/10.1007/978-3-031-57256-2_30",\ndoi="10.1007/978-3-031-57256-2_30"\n}\n\n

\n

\n Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.\n

\n

@InProceedings{svcomp24-emergentheta,\nauthor="Bajczi, Levente\nand Szekeres, D{\\'a}niel\nand Mondok, Mil{\\'a}n\nand {\\'A}d{\\'a}m, Zs{\\'o}fia\nand Somorjai, M{\\'a}rk\nand Telbisz, Csan{\\'a}d\nand Dobos-Kov{\\'a}cs, Mih{\\'a}ly\nand Moln{\\'a}r, Vince",\neditor="Finkbeiner, Bernd\nand Kov{\\'a}cs, Laura",\ntitle="EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)",\nbooktitle="Tools and Algorithms for the Construction and Analysis of Systems",\nyear="2024",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="371--375",\nabstract="Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta, a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta, and its first debut on SV-COMP'24 in the ReachSafety category.",\nisbn="978-3-031-57256-2",\nurl="https://link.springer.com/chapter/10.1007/978-3-031-57256-2_23",\ndoi="10.1007/978-3-031-57256-2_23"\n}\n\n

\n

\n Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta, a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta, and its first debut on SV-COMP'24 in the ReachSafety category.\n

\n

@inproceedings{minisy2024mm,\n    author     = {Mondok, Mil\\'an and Moln\\'ar, Vince},\n    title      = {Efficient Manipulation of Logical Formulas as Decision Diagrams},\n    year       = {2024},\n    booktitle  = {Proceedings of the 31st PhD Mini-Symposium},\n    location   = {Budapest, Hungary},\n    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n    editor     = {Renczes, Bal\\'azs},\n    pages      = {61--65},\n\n    type       = {Local event},\n    url_pdf    = {publications/minisy2024mm.pdf},\n    abstract   = {Constraint solving and the manipulation of Satisfiability Modulo Theories (SMT) formulas is a fundamental task in symbolic model checking. SMT solvers have proven to be efficient tools in exploiting the high expressive power and flexibility offered by SMT formulas. Decision diagram based approaches have also gained popularity for their capability to represent all solutions in a compact way and are used in numerous efficient algorithms. However, there is a gap between these two approaches. In this paper, we present a novel data structure that can combine the flexibility of SMT formulas and the power of SMT solvers with the efficient representation of the solutions. This data structure is a blend of decision diagrams and SMT formulas: it allows us to handle logical formulas as decision diagrams, leveraging both the power of SMT solvers and the advantages of diagram representation. The compatibility with decision diagrams allows the integration of efficient algorithms working on the two different representations. When discussing the benefits of this approach, we also emphasize how the intersection operation - a common problem in constraint solving - can be carried out more efficiently using lazy evaluation. We can also build on the same advantage in transitive closure calculations.},\n}\n\n

\n

\n Constraint solving and the manipulation of Satisfiability Modulo Theories (SMT) formulas is a fundamental task in symbolic model checking. SMT solvers have proven to be efficient tools in exploiting the high expressive power and flexibility offered by SMT formulas. Decision diagram based approaches have also gained popularity for their capability to represent all solutions in a compact way and are used in numerous efficient algorithms. However, there is a gap between these two approaches. In this paper, we present a novel data structure that can combine the flexibility of SMT formulas and the power of SMT solvers with the efficient representation of the solutions. This data structure is a blend of decision diagrams and SMT formulas: it allows us to handle logical formulas as decision diagrams, leveraging both the power of SMT solvers and the advantages of diagram representation. The compatibility with decision diagrams allows the integration of efficient algorithms working on the two different representations. When discussing the benefits of this approach, we also emphasize how the intersection operation - a common problem in constraint solving - can be carried out more efficiently using lazy evaluation. We can also build on the same advantage in transitive closure calculations.\n

\n

@inproceedings{minisy2020mm,\n    author     = {Mondok, Mil\\'an and V\\"or\\"os, Andr\\'as},\n    title      = {Abstraction-Based Model Checking of Linear Temporal Properties},\n    year       = {2020},\n    booktitle  = {Proceedings of the 27th PhD Mini-Symposium},\n    location   = {Budapest, Hungary},\n    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n    editor     = {Renczes, Bal\\'azs},\n    pages      = {29--32},\n\n    type       = {Local event},\n    url_pdf    = {publications/minisy2020mm.pdf},\n    abstract   = {Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of "lasso"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.},\n}\n\n

\n

\n Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of \"lasso\"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.\n