Integration Test Generation and Formal Verification for Distributed Controllers

View/ Open
Metadata
Show full item record
Link to refer to this document:
Collections
Abstract
Software-intensive distributed controllers are becoming increasingly prevalent, among others, also in railway interlocking systems (RIS). As such systems carry out critical tasks, their systematic verification and testing are a must, which can be supported by formal methods. This paper presents a verification and testing approach for a distributed RIS subsystem using hidden formal methods. The subsystem’s functional behavior is modeled using statechart components defined in a high-level UML-based modeling language, which are integrated according to sound execution and interaction semantics defined by the RIS protocol. The emergent model is automatically mapped into input formalisms of model checker back-ends. Integration tests for the system implementation are derived according to various modelbased coverage criteria using the model checker back-ends and generated properties. The approach is implemented in our open source Gamma Statechart Composition Framework.- Title
- Integration Test Generation and Formal Verification for Distributed Controllers
- Author
- Graics, Bence
- Majzik, István
- Date of issue
- 2023
- Access level
- Open access
- Copyright owner
- Szerző
- Conference title
- 30th Minisymposium of the Department of Measurement and Information Systems
- Conference place
- Budapest
- Conference date
- 2023.02.06-2023.02.07.
- Language
- en
- Page
- 1 - 4
- Subject
- MBSE, collaborating statecharts, hidden formal methods, model checking, test generation, integrated tool suite
- Version
- Post print
- Identifiers
- DOI: 10.3311/minisy2023-001
- Title of the container document
- Proceedings of the 30th Minisymposium
- ISBN, e-ISBN
- 978-963-421-904-0
- Document type
- könyvfejezet
- Document genre
- Konferenciacikk
- University
- Budapest University of Technology and Economics
- Faculty
- Faculty of Electrical Engineering and Informatics
- Department
- Department of Measurement and Information Systems