Integration Test Generation and Formal Verification for Distributed Controllers
Loading...
Date
2023
item.page.title
Integration Test Generation and Formal Verification for Distributed Controllers
item.page.contributor
item.page.advisor
Authors
Graics, Bence
Majzik, István
Majzik, István
item.page.spatial
item.page.createdDate
item.page.extent
item.page.medium
item.page.isbn
item.page.issn
item.page.language
en
Publisher
item.page.replaces
item.page.alternative
item.page.type
könyvfejezet
item.page.accessRights
Open access
item.page.rightsHolder
Szerző
item.page.address
item.page.conferenceDate
2023.02.06-2023.02.07.
item.page.conferencePlace
Budapest
item.page.conferenceTitle
30th Minisymposium of the Department of Measurement and Information Systems
item.page.containerIdentifierIsbn
978-963-421-904-0
item.page.containerIdentifierIssn
item.page.containerPeriodicalNumber
item.page.containerPeriodicalVolume
item.page.containerPeriodicalYear
item.page.containerTitle
Proceedings of the 30th Minisymposium
item.page.contributorLector
item.page.contributor.lector
item.page.contributorBody
item.page.courseCode
item.page.courseName
item.page.dateDefence
item.page.department
Department of Measurement and Information Systems
item.page.descriptionVersion
Post print
item.page.doctoralSchool
item.page.faculty
Faculty of Electrical Engineering and Informatics
item.page.firstpage
1
item.page.identifier
item.page.identifierLectureNotes
item.page.identifierReference
item.page.inscription
item.page.note
item.page.page
item.page.periodicalCreator
item.page.periodicalNumber
item.page.periodicalVolume
item.page.periodicalYear
item.page.scale
item.page.signature
item.page.subjectArea
item.page.subjectField
item.page.subjectOszkar
MBSE
collaborating statecharts
hidden formal methods
model checking
test generation
integrated tool suite
collaborating statecharts
hidden formal methods
model checking
test generation
integrated tool suite
item.page.technique
item.page.titlenumber
item.page.typeType
Konferenciacikk
item.page.university
Budapest University of Technology and Economics
item.page.universityProgram
item.page.universityProgramLevel
Journal Title
Journal ISSN
Volume Title
Publisher
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.