Usually, the design of an Autonomous Vehicle (AV) does not take into account traffic rules and so the adoption of these rules can bring some challenges, e.g., how to come up with a Digital Highway Code which captures the proper behaviour of an AV against the traffic rules and at the same time minimises changes to the existing Highway Code? Here, we formally model and implement three Road Junction rules (from the UK Highway Code). We use timed automata to model the system and the MCAPL (Model Checking Agent Programming Language) framework to implement an agent and its environment. We also assess the behaviour of our agent according to the Road Junction rules using a double-level Model Checking technique, i.e., UPPAAL at the design level and AJPF (Agent Java PathFinder) at the development level. We have formally verified 30 properties (18 with UPPAAL and 12 with AJPF), where these properties describe the agent’s behaviour against the three Road Junction rules using a simulated traffic scenario, including artefacts like traffic signs and road users. In addition, our approach aims to extract the best from the double-level verification, i.e., using time constraints in UPPAAL timed automata to determine thresholds for the AVs actions and tracing the agent’s behaviour by using MCAPL, in a way that one can tell when and how a given Road Junction rule was selected by the agent. This work provides a proof-of-concept for the formal verification of AV behaviour with respect to traffic rules.

The development and deployment of Autonomous Vehicles (AVs) on our roads is not only realistic in the near future but can also bring significant benefits. In particular, it can potentially solve several problems relating to vehicles and traffic, for instance: (i) possible reduction of traffic congestion, with the consequence of improved fuel economy and reduced driver inactivity; (ii) possible reduction in the number of accidents, assuming that an AV can minimise the human errors that often cause traffic accidents; and (iii) increased ease of parking, especially when one considers the potential for shared AVs. In order to deploy an AV there are significant steps that must be completed in terms of hardware and software. As expected, software components play a key role in the complex AV system and so, at least for safety, we should assess the correctness of these components. In this paper, we are concerned with the high-level software component(s) responsible for the decisions in an AV. We intend to model an AV capable of navigation; obstacle avoidance; obstacle selection (when a crash is unavoidable) and vehicle recovery, etc, using a rational agent. To achieve this, we have established the following stages. First, the agent plans and actions have been implemented within the Gwendolen agent programming language. Second, we have built a simulated automotive environment in the Java language. Third, we have formally specified some of the required agent properties through LTL formulae, which are then formally verified with the AJPF verification tool. Finally, within the MCAPL framework (which comprises all the tools used in previous stages) we have obtained formal verification of our AV agent in terms of its specific behaviours. For example, the agent plans responsible for selecting an obstacle with low potential damage, instead of a higher damage obstacle (when possible) can be formally verified within MCAPL. We must emphasise that the major goal (of our present approach) lies in the formal verification of agent plans, rather than evaluating real-world applications. For this reason we utilised a simple matrix representation concerning the environment used by our agent.Comment: In Proceedings FVAV 2017, arXiv:1709.0212

The process of looking a spot could be a problem. There are computing solutions being developed to optimize this problem. One of these solutions is using multiagent systems (MAS). In this paper, a MAS is developed in order to allocate spots in a smart parking using the framework JaCaMo. This paper comprises of two types of agents: manager and drivers. The manager is responsible for administrating the parking spots which will be assigned to drivers according to a corresponding degree of trust. The trust degree is a value which shows the commitment of the driver before the manager. In order to verify the effectiveness of the MAS, several simulations were conducted in empirical scenarios. Experiments show that the degree of trust impacts in the parking spot allocation process.

The increase volume of vehicles circulating in large cities and the limited space for parking are factors that motivate the adoption of systems capable of dealing with such problems. In this context, smart parking systems are suitable solutions to avoid the traffic congestion, the air pollution and the long search to find a free parking spot. The inclusion of emergent ICT technologies and artificial intelligence techniques, and particularly using multi-agent systems, combined under the scope of Cyber-Physical Systems (CPS), ensure flexibility, modularity, adaptability and the decentralization of intelligence through autonomous, cooperative and proactive entities. Such smart parking systems can be easily adapted to any type of vehicle to be parked and scalable in terms of the number of parking spots and drivers/vehicles. A fundamental issue in these agent-based CPS parking systems is the interconnection between the cyber and physical counterparts, i.e. between the software agents and the physical asset controllers to access the parking spots. This paper focuses on developing an agent-based CPS for a smart parking system and particularly addressing how the software agents are interconnected with the physical asset controllers using proper Internet of Things technologies. The proposed approach was implemented in two distinct parking systems, one for bicycles and another for cars, showing an efficient, modular, adaptable and scalable operation.