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.

We advocate a fusion of property-oriented testing (POT) and model-based testing (MBT). The existence of a symbolic finite state machine (SFSM) model fulfilling the properties of interest is exploited for property-directed test data generation and to create a test oracle. A new test generation strategy is presented for verifying that the system under test (SUT) satisfies the same LTL safety conditions over a given set of atomic propositions as the model. We prove that this strategy is exhaustive in the sense that any SUT violating at least one of these formulae will fail at least one test case of the generated suite. It is shown that the existence of a model allows for significantly smaller exhaustive test suites as would be necessary for POT without reference models. As a corollary, the main theorem also generalises a known result about SFSM-based conformance testing for language equivalence. Our approach fits well to industrial development processes for (potentially safety-critical) cyber-physical systems, where both models and properties representing system requirements are elaborated for development, verification, and validation.

Abstract In this paper, we review software-based technologies already known to be, or expected to become essential for autonomous train control systems with grade of automation GoA 4 (unattended train operation) in existing open railway environments. It is discussed which types of technology can be developed and certified already today on the basis of existing railway standards. Other essential technologies, however, require modifications or extensions of existing standards, in order to provide a certification basis for introducing these technologies into non-experimental “real-world” rail operation. Regarding these, we check the novel pre-standard ANSI/UL 4600 with respect to suitability as a certification basis for safety-critical autonomous train control functions based on methods from artificial intelligence. As a thought experiment, we propose a novel autonomous train controller design and perform an evaluation according to ANSI/UL 4600. This results in the insight that autonomous freight trains and metro trains using this design could be evaluated and certified on the basis of ANSI/UL 4600 .

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.

Abstract In this paper, an efficient approach to data validation of distributed geographical interlocking systems (IXLs) is presented. In the distributed IXL paradigm, track elements are controlled by local computers communicating with other control components over local and wide area networks. The overall control logic is distributed over these track-side computers and remote server computers that may even reside in one or more cloud server farms. Redundancy is introduced to ensure fail-safe behaviour, fault-tolerance, and to increase the availability of the overall system. To cope with the configuration-related complexity of such distributed IXLs, the software is designed according to the digital twin paradigm: physical track elements are associated with software objects implementing supervision and control for the element. The objects communicate with each other and with high-level IXL control components in the cloud over logical channels realised by distributed communication mechanisms. The objective of this article is to explain how configuration rules for this type of IXLs can be specified by temporal logic formulae interpreted on Kripke Structure representations of the IXL configuration. Violations of configuration rules can be specified using formulae from a well-defined subset of LTL. By decomposing the complete configuration model into sub-models corresponding to routes through the model, the LTL model checking problem can be transformed into a CTL checking problem for which highly efficient algorithms exist. Specialised rule violation queries that are hard to express in LTL can be simplified and checked faster by performing sub-model transformations adding auxiliary variables to the states of the underlying Kripke Structures. Further performance enhancements are achieved by checking each sub-model concurrently. The approach presented here has been implemented in a model checking tool which is applied by Siemens Mobility for data validation of geographical IXLs.

This paper is about practical verification of Airbus avionic systems during type certification, with special focus on automated testing. The material is based on test and verification services performed for Airbus by a spinoff company of the University of Bremen, as well as on consultancy services delivered by our research group to Airbus and its suppliers. In the context of model-based systems engineering, the test automation approach is currently shifting from manual test procedure programming to model-based testing (MBT), where test cases are automatically identified in models describing the application behavior, allowing for automated test data calculation and test procedure generation. We describe the situations where today's MBT technology is already adequate to increase the effectiveness of automated testing in industry. In addition, we describe some open challenges arising from practical avionic systems testing, where satisfactory solutions still require some research effort.

Abstract The main objective of this article is to present a complete finite black-box testing theory for non-deterministic Kripke structures with possibly infinite input domains, but finite domains for internal state variables and outputs. To this end, an abstraction from Kripke structures of this sub-domain to finite state machines is developed. It is shown that every complete black-box testing theory for (deterministic or nondeterministic) finite state machines in the range of this abstraction induces a complete black-box input equivalence class partition testing (IECPT) theory for the Kripke structures under consideration. Additionally, it is shown that each of these IECPT theories can be combined with random testing, such that a random value is selected from an input equivalence class, whenever a representative from this class is required in a test step. Experiments have shown that this combination increases the test strength of equivalence class tests for systems under test (SUT) outside the fault domain, while we show here that this randomisation preserves the completeness property for SUT inside the domain. The investigations lead to several complete IECPT strategies which, to our best knowledge, were not known before for this sub-domain of Kripke structures. The elaboration and presentation of results is performed on a semantic level, so that the testing theories under consideration can be applied to models presented in any concrete formalism, whose behaviour is reflected by a member of our semantic category.

The Unified Modeling Language (UML) is a defacto standard for software development and, together with the Object Constraint Language (OCL), allows for a precise description of a system prior to its implementation. At the same time, these descriptions can be employed to check the consistency and, hence, the correctness of a given UML/OCL model. In the recent past, numerous (automated) approaches have been proposed for this purpose. The behavior of the systems has usually been considered by means of sequence diagrams, state machines, and activity diagrams. But with the increasing popularity of design by contract, also composite structures, classes, and operations are frequently used to describe behavior in UML/OCL. However, for these description means no solution for the validation and verification of concurrent behavior is available yet. In this work, we propose such a solution. To this end, we discuss the possible interpretations of “concurrency” which are admissible according to the common UML/OCL interpretation and, afterwards, propose a methodology which exploits solvers for SAT Modulo Theories (i. e., SMT solvers) in order to check the concurrent behavior of UML/OCL models. How to address the resulting problems is described and illustrated by means of a running example. Finally, the application of the proposed method is demonstrated.

In order to cope with the complexity of today's system designs, higher levels of abstraction are considered. Modeling languages such as SysML provide adequate description means for an abstract specification of the structure and the behavior of a system to be implemented. Due to its sufficient degree of formality, SysML additionally allows for performing several automated test and verification tasks. For these tasks, however, a formal encoding of the behavioral model semantics is required; this is typically achieved by generating initial state conditions as well as the transition relation from the model. Since SysML provides a multitude of alternative or complementary notations, this poses a significant challenge to the development of corresponding tool support. In this paper, we therefore propose an alternative approach to the generation of transition relations: In a first step, a model-to-model transformation is applied which unifies the behavioral descriptions into one single notation, namely operations allocated in blocks and specified by pre- and post-conditions. Afterwards, only pre- and post-conditions as well as some auxiliary constraints for fixing semantic variation points need to be considered when generating the transition relation. The approach presented here has been evaluated in the development of industrial tools supporting bounded model checking and model-based test generation.

Abstract This paper describes a complete model-based development and verification approach for railway control systems. For each control system to be generated, the user makes a description of the application-specific parameters in a domain-specific language. This description is automatically transformed into an executable control system model expressed in SystemC. This model is then compiled into object code. Verification is performed using three main methods applied to different levels. (0) The domain-specific description is validated wrt. internal consistency by static analysis. (1) The crucial safety properties are verified for the SystemC model by means of bounded model checking. (2) The object code is verified to be I/O behaviourally equivalent to the SystemC model from which it was compiled.

In this paper we introduce Timed Moore Automata, a specification formalism which is used in industrial train control applications for specifying the real-time behavior of cooperating reactive software components. We define an operational semantics for the sequential components (units) with an abstraction of time that is suitable for checking timeout behavior of these units. A model checking algorithm for live lock detection is presented, and two alternative methods of test case/test data generation techniques are introduced. The first one is based on Kripke structures as used in explicit model checking, while the second method does not require an explicit representation but relies on SAT solving techniques.

The hybrid low-level framework HL3is a generic compilation target for high-level specification formalisms for hybrid systems. It is designed to support and validate the transformation of high-level specifications into executable code. We present a formal operational semantics for the execution of HL3models, which assigns formal meaning to the high-level specification within a transformational approach or serves as concrete target formalism in a refinement approach. The HL3runtime environment has been optimized for execution on high-speed multi-CPU cluster architectures which is also reflected in the operational rules.

The authors introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.

This paper presents experiences gained from the verification of a large-scale real-world embedded system by means of formal methods. This industrial verification project was performed for a fault-tolerant system designed and implemented by DaimlerChrysler Aerospace for the International Space Station ISS. The verification involved various aspects of system correctness, like deadlock and livelock analysis, correct protocol implementation, etc. The approach is based on CSP specifications and uses the model-checking tool FDR. It is realized by combining methods for the development as well as for the analysis. It is illustrated by examples and results obtained during the verification of the Byzantine agreement protocol implementation, where the combination of different abstraction methods is required.