We present a distributed railway interlocking (IXL) method based on trains communicating with switch boxes deployed along the railway network for switching points and monitoring the occupancy states of track elements. The method does not require any centralised IXL components. A distributed architecture is proposed that carefully separates the overall business logic and automated train operation from the safety-critical automated train protection and distributed IXL logic. This architecture is also suitable for autonomous trains traversing the railway network. The safety of the IXL logic is formally proven, using the Isabelle/HOL proof assistant. Experiments confirm that this proof-based approach is superior to model checking approaches, since the model checking effort grows exponentially with the size of the railway network. In contrast to this, the mathematical safety proof is performed once and for all railway networks fulfilling a realistic well-formedness condition. For a concrete network, only the well-formedness of the network and its initial train placements has to be verified, whereas the safety of the dynamic behaviour is a consequence of the network-independent safety proof.

The field of model-based testing has witnessed the development of several test strategies on finite state machines . Although these strategies are often related, little effort has been made to explicitly identify patterns shared between them, and their concrete implementations as well as completeness proofs regularly exhibit redundancy. In this paper, we propose an approach for the systematic verification and implementation of strategies for the language-equivalence conformance relation. We present frameworks in the form of higher order functions that implement shared behaviour once and encapsulate diverging behaviour in procedural parameters, thus reducing duplication and improving maintainability and extensibility. We show that this simplifies completeness proofs by proving complete all considered strategies using the same argument. All presented frameworks, proofs, and concrete strategy implementations have been mechanised using the proof assistant Isabelle.

Summary For partial, nondeterministic, finite state machines, a new conformance relation called strong reduction is presented. It complements other existing conformance relations in the sense that the new relation is well suited for model‐based testing of systems whose inputs are enabled or disabled, depending on the actual system state. Examples of such systems are graphical user interfaces and systems with interfaces that can be enabled or disabled in a mechanical way. We present a new test generation algorithm producing complete test suites for strong reduction. The suites are executed according to the grey‐box testing paradigm: it is assumed that the state‐dependent sets of enabled inputs can be identified during test execution, while the implementation states remain hidden, as in black‐box testing. We show that this grey‐box information is exploited by the generation algorithm in such a way that the resulting best‐case test suite size is only linear in the state space size of the reference model. Moreover, examples show that this may lead to significant reductions of test suite size in comparison to true black‐box testing for strong reduction.