Formal Modelling and Verification of Multi-Parameter Context and Agent Transition Systems: Application to Urban Delivery Zone and Autonomous Electric Vehicle

The increasing integration of autonomous electric vehicles (EVs) into Intelligent Transportation Systems (ITSs) needs rigorous mechanisms to ensure their safe and effective operation in dynamic environments. The reliability of such vehicles depends not only on their internal capabilities but also on the suitability and safety of the environments in which they operate. This paper introduces a formal modelling framework that captures independently the dynamic evolution of the environmental context and the EV agent using multi-parameter transition systems. Two distinct models are defined: the Context Transition System (CTS), which models changes in environmental states, and the Agent Transition System (ATS), which captures the internal state evolution of the EV. Safety and liveness properties are formally specified in Computation Tree Logic (CTL) and verified using the nuXmv model checker. The framework is validated through two representative use cases: a dynamic urban delivery zone and an autonomous electric delivery vehicle. The results highlight the framework’s effectiveness in detecting unsafe conditions, verifying mission objectives, and supporting the reliable deployment of EVs in ITS.