Integration Test Generation and Formal Verification for Distributed Controllers

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.