A verifiable simulation model for real-world microscopic traffic simulations

• Complete simulation model for real-world microscopic traffic simulations with executable formal semantics.
• Specification of a simulation engine with sequential or parallel operation and automatic domain decomposition.
• Supports formal verification and numerical solution verification for the simulation model and all subject-specific models.
• Road traffic network data model for real-world, large-scale networks in urban or highway environments.
• Demonstration of how to implement and verify each subject-specific model.

This article presents a scientific discussion about the ongoing progress in the development of traffic simulation system platforms. As part of the discussion, the presentation introduces a simulation model that is based on the fully functional, real-world online traffic information system OLSIMv4 which is the updated version of the traffic information platform for the highway network of North Rhine-Westphalia (Germany). The simulation model consists of a simulation engine and a combination of several subject-specific model families such as vehicle models, microscopic traffic models, detector models, and tuning element models. Additionally, it provides a data model for arbitrary road traffic networks in highway and urban environments.The presentation includes a demonstration of how to form and initialize all relevant system components by providing an example for each component. The demonstrations use the declarative programming language Maude to form and initialize the components due to its simplicity and expressive power. The components facilitate their enhancement by a verification and validation management approach. The goal of the enhancement effort is to optimize the further development of the underlying OLSIMv4 system. In addition, the presented methodology stands exemplarily for the design and implementation of a whole class of systems. Additionally, the definitions of the simulation model can be used as a specification for an implementation with sequential, parallel, and distributed operation. Therein, independent entities can be inferred automatically by the simulation engine as part of an automatic domain decomposition. It has been implemented as a sequential and a parallel simulation that exploits CPU thread-level parallelism.