Subject: Re: [manet] formal verification of ad hoc networks

From: "Ayyasamy, Senthilkumar (UMKC-Student)" <[email-masked]>
Date: Sat, 22 Feb 2003 05:51:03 -0600

>
> "K. Bhargavan, C. Gunter, M. Kim, I. Lee, D. Obradovic,O. Sokolsky, and M.
>  Viswanathan. Verisim: Formal  analysis of network simulations. In Int.
>  Symposium on Software Testing and Analysis, pages 2-13, 2000. "

  This work is more related to model checkers and theorem analyzers. They
concentrate more on the validation part of the communication protocols.
But, gerg is asking more related to process algebra. 

>> I'm doing research on formal verification of algorithms for ad-hoc networks.
>> I'm trying to apply transition systems (process algebras etc.) in modelling
>> and verification of the reactive algorithms running in ad-hoc environment

I am not sure, but their are two types of process algebra, which are useful 
for communication protocols: 
 - CCS (Calculus of Communication systems) and
 - PEPA (performance evaluation process algrbra.)
You can find a lot of material on the net and books.

But a word of caution: You cannot check your PA model unless you have a specification 
and design. So, i suggest using the techniques and reference mentioned by Tao lin. 

_______________________________________________
manet mailing list
[email-masked]
https://www1.ietf.org/mailman/listinfo/manet

---

From: Grzegorz Jablonski <[email-masked]>
Date: Mon, 24 Feb 2003 20:06:19 -0000

hi,

thanks, the papers on Verisim are very interesting. I wanted to go similar
way, by building an abstract model in a process algebra or similar formalism
and to verify it, with use of model checkers and equivalence relations.

I've tried Calculus of Broadcasting Systems, it seemed the most suitable for
my purposes. However, it turns out to be very difficult (at least for me!)
to build a suitable formal model, which would reflect the reality of ad-hoc
networks, could guide the implementation and be verifiable.
Anyway, I'm still trying.

Cheers
Greg

----- Original Message -----
From: "Ayyasamy, Senthilkumar (UMKC-Student)" <[email-masked]>
To: "celliott" <[email-masked]>; "jablonsk"
<[email-masked]>; "manet" <[email-masked]>
Cc: "taolin" <[email-masked]>
Sent: Saturday, February 22, 2003 11:51 AM
Subject: Re: [manet] formal verification of ad hoc networks