Models and formal verification for Electric Vehicle and Urban Delivery Zone

This dataset contains formal models and verification data related to the symbolic modelling and verification of a dynamic Electric Vehicle and urban delivery zone. It includes nuXmv specifications for the Context Transiton System (CTS) and Agent Transition System (ATS) with Computation Tree Logic (CTL) properties, figures of verification results, and figures of CTS and ATS. The dataset is associated with a research manuscript currently under submission.