Formal Specification Language for Vehicular Ad-Hoc Networks

Vehicular Ad-Hoc Network (VANET) is a form of Mobile Ad-Hoc Network (wireless
Network), originally used to provide safety & comfort for passengers, & currently being
used to establish Dedicated Short Range Communications (DSRC) among near by
Vehicles (V2V Communications) and between vehicles and nearby fixed infrastructure
equipments; Roadside equipments (V2I Communications). VANET was used also to
warn drivers of collision possibilities, road sign alarms, auto-payment at road tolls and
parks. Usually VANET can be found in Intelligent Transportation Systems (ITS).
VANET is the current and near future hot topic for research, that has been
targeted by many researchers to develop some applications and protocols specifically for
the VANET. But a problem facing all VANET researchers is the unavailability of a
formal specification language to specify the VANET systems, protocols, applications and
scenarios proposed by those researchers.
A specification language is a formal language that is used during the systems
design, analysis, and requirements analysis. Using a formal specification language, a
researcher can show “What his system does”, Not How.
As a contribution of our research we have created a formal specification language
for VANET. We made the use of some Romans characters & some basic symbols to
represent VANET Systems & Applications. In addition, we have created some combined
symbols to represent actions and operations of the VANET system and its participating
devices. Our formal specification language covers many of the VANET aspects, and
offers Validity Test and Consistency Test for the systems.
Using our specification language, we have presented three different case studies
based on a VANET system model we have created and put them into the system validity
and consistency tests and showed how to describe a VANET system and its applications
using our formal specification language.