摘要：AbstractThis paper presents a method to use model checking techniques to verify the safety of the behavior of cooperative vehicles. We model the roadway, cooperative and non-cooperative actors as automata that are used to construct the state space of the local traffic system using techniques from automata theory. We then translate the automata into a format readable by nuXmv, a state-of-the-art model checker. Together with specifications that model accident- and deadlock-freeness, we then use nuXmv to prove that a local traffic system is safe.
