KARAVAN (Smart traffic flow - design and formal verification)

Project Title

KARAVAN (Smart traffic flow - design and formal verification)

Project Area of Specialization Internet of ThingsProject Summary

With continuous advancements in technology, the
concept of autonomous cars has gained immense
popularity over the years. An autonomous vehicle is
capable of moving with little or no human input while
sensing and monitoring the environment around it.
Technology has time and again proven to be beneficial to humankind as it helps us to work smarter and quicker,
saving our time and effort, but drastically increasing
efficiency. Artificially Intelligent systems have proven
to make work so much easier for humans by either
assisting them or completely replacing them. A few
applications include robots in car manufacturing
factories, to robots on other planets.
Similarly, one recurring issue is road traffic accidents
that can cause huge material and life loss. Highways and
Motorways are common roads for trucks and buses to
move on as a caravan. This increases the likeliness of
accidents more due to rash driving, suddenly changing
lanes or even just dozing off at the steering wheel due to
continuous traveling. In many situations, it is possible
that the accidents are unintentional, such as the driver
being tired or exhausted. This is where the concept of
autonomous cars come in to assist the drivers in order to
avoid accidents.
This project suggests a solution to assist in prevention of
the occurrence of accidents on Highways and
Motorways due to careless driving and sleepy drivers,
which are inevitable human errors. Hence, this project
implements a system to assist the drivers in safe driving.
In addition to the project design and implementation, the
project will be formally validated and verified using
model checking on IAR VisualState and UPPAAL Tool,
which again is a field gaining more popularity now. This
ensures the system being verified is safe, accurate and
correct.
Software verification and validation are two different
elements of software checking. Verification checks if the
software is correct, whereas validation checks whether

the software is according to the demands. They’re
popularly known as V&V. They have been quite helpful
in producing quality software as the software goes
through multiple tests where it has to satisfy certain
properties in order to be marked as accurate and
correctly functional software. However, model checking
differs from other testing methods that only use specific
inputs to examine outputs. Here, the whole model of the
system is also drawn and tested. This enables us to
figure out where exactly and what exactly the fault is in
software hence making efficient and less time
consuming to fix errors.

Project Objectives

• To develop a system of autonomous vehicles communicating with each other whle following a track
• To develop a Bluetooth based Indoor Positioning System to enable location tracking
• To perform Formal verification and Model checking of the algorithms to ensure their correctiveness

Project Implementation Method

The development process of this project has four phases:
1. Build Hardware for Autonomous Robot
To get started, we have attached the motors and the
H bridge (the card that delivers power to the motors)
to the lower part of the chassis. First, we attached
the four metal brackets (they’re rectangular, drilled
blocks of metal) to each motor using two long bolts
and two nuts. Then each motor attached to the
chassis by using two short bolts in the bottom of
each metal bracket. The next step is to attach the
Arduino.
2. Arduino Device Setup
We have attached the motor shield on the Arduino
and motor shield is connected with the actuators.
The Arduino is controlling the actuators using the
motor shield with commands.
3. Configure Raspberry Pi
First, we install the OpenCV dependencies and then
image and video libraries. These are critical to being
able to work with image and video files. After
installing the required dependencies, we configured
the environment of python 3 on Raspberry Pi.
4. Image Processing
After capturing the image from the camera we
process the image in the raspberry pi using Gaussian
filtering and edge detection algorithms. We removed
high frequency noise and detect lane edge more
accurately. Finally, we can make reference control
line mean of right, left side lane.

5. Leading Car Operation
After the image processing, the leading car will use
the proportional integral derivative algorithm to
control the car steering and follow the white line.
This algorithm also helps car to get on track if
there’s any instability.
6. Communication between leading car and
Following Car
The raspberry pi attached on the leading car will
communicate with the raspberry bi on the following
car to align the cars properly. The leading car will
send the Stop, Start and Turn signal to leading car.

Benefits of the Project

This project presents a proof of concept of a real life
implementation of autonomous cars moving in a line
like a caravan. 

This system can be used as a basis of a driver assistance
and lane keeping system that can assist drivers while
driving on motorways.
This project can also be applied to a real life application
of swarm robotics since it involves multiple robots
communicating with each other and working to achieve
a certain goal.
Many of these applications are safety critical and this
project showcases the use of formal verification to ensure
that these systems are robust and reliable.
This system can also be used as a starting point for an
autonomous caravan system applicable in scenarios such
as military convoys, public transport, cargo trucks and
security detail.
Real-life applications may require additional sensors
such as LiDAR, radars and sonar. They will also require

more complex algorithms as a result of which the
models created will also be more complex. However,
this project proves that model checking can be applied
effectively to prove the correctness of these algorithms.

Technical Details of Final Deliverable

The final deliverable will consist of the following:

1. Assembled Cars that have the abiltiy to autonomously navigate around a track while safely following each other by communicating over a network

2. An Indoor Positioning System that tracks the movement of the cars around the track with sufficient accuracy. This is implemented using esp32 BLE beacons

3. Research paper highlighting our findings, processes and results

Final Deliverable of the Project HW/SW integrated systemCore Industry TransportationOther IndustriesCore Technology Internet of Things (IoT)Other Technologies Artificial Intelligence(AI), RoboticsSustainable Development Goals Industry, Innovation and Infrastructure, Sustainable Cities and CommunitiesRequired Resources

Item Name	Type	No. of Units	Per Unit Cost (in Rs)	Total (in Rs)
			Total in (Rs)	53550
Raspberry pi	Equipment	3	9000	27000
Arduino Uno Car	Equipment	3	4000	12000
ESP32 Arduino	Equipment	5	750	3750
Batteries	Equipment	6	1800	10800