The evolution of driving technology has recently progressed from active safety features and ADAS systems to fully sensor-guided autonomous driving. Bringing such a vehicle to market requires not only simulation and testing but formal verification to account for all possible traffic scenarios. A new verification approach, which combines the use of two well-known model checkers: model checker for multi-agent systems (MCMAS) and probabilistic model checker (PRISM), is presented for this purpose. The overall structure of our autonomous vehicle (AV) system consists of: (1) A perception system of sensors that feeds data into (2) a rational agent (RA) based on a belief–desire–intention (BDI) architecture, which uses a model of the environment and is connected to the RA for verification of decision-making, and (3) a feedback control systems for following a self-planned path. MCMAS is used to check the consistency and stability of the BDI agent logic during design-time. PRISM is used to provide the RA with the probability of success while it decides to take action during run-time operation. This allows the RA to select movements of the highest probability of success from several generated alternatives. This framework has been tested on a new AV software platform built using the robot operating system (ROS) and virtual reality (VR) Gazebo Simulator. It also includes a parking lot scenario to test the feasibility of this approach in a realistic environment. A practical implementation of the AV system was also carried out on the experimental testbed.

Deep Neural Networks (DNNs) have attained remarkable prediction outcomes in image classification tasks, leading to significant progress in computer vision applications. However, the presence of adversarial examples has emerged as a critical challenge to the robustness and efficiency of deep learning-based image classifiers. Adversarial examples are specially designed perturbations applied to input images to deceive the models into generating inaccurate predictions while appearing indistinguishable to human observers. In this paper, we present a defense mechanism, namely Defensive Distillation with Gaussian Blurring (DDGB), that improves the robustness of deep learning models towards adversarial attacks. First, two models, a teacher and a student model, were utilized to train and validate the presented approach. The teacher model is trained and then leveraged to determine softened probabilities, which are later utilized to train the student model. Second, a feature-squeezing technique based on Gaussian blurring is applied to the adversarial examples generated from the distilled student model as a form of defense mechanism to make the adversarial perturbations less effective. The obtained findings demonstrate that the proposed approach is effective in improving the performance, achieving classification accuracies of 87.61% and 87.48% using the Fast Gradient Sign Method (FGSM) and Basic Iterative Method (BIM) attacks, respectively, based on the CIFAR-10 dataset. In summary, the presented approach achieves a 70.66% reduction in computations for the student model, allowing the model to be deployed on devices with limited resources and provide improved prediction accuracy towards adversarial attacks.