Subject: [Sdn] Formal Specification to include boot process?

From: <[email-masked]>
Date: Thu, 2 Aug 2012 00:59:28 +0100

Myung-Ki & co-authors,

If time had permitted, I would have asked this question from the floor just now, but the list is next best...

I imagine the formal specification problem is hard enough without considering boot time, but I'm interested in how and whether a network can boot after various failures of individual nodes (and secondarily, whether it could go through a vulnerable state while booting).

I don't know much about the limitations of these specfication languages, but you sound like you do. Do you think this would be possible? If you're interested in taking up this challenge, that would be cool.

Bob

---

From: "Myung-Ki Shin" <[email-masked]>
Date: Fri, 3 Aug 2012 02:16:28 +0900

Hi Bob, 
Yes, we are also considering that kinds of boot time (?) issues if I
understand your question correctly. 
Basically, the formally verifiable networking platform may depend on
proposed SDN architecture, because 
it would be placed on the top of SDN controllers, normally. In this sense,
we are now assuming that
SDN controllers can gather the number of individual network nodes'
information/states in real-time (e.g., failure as you mentioned)
from e.g., northbound interfaces, and SNMP, etc. 
So, we can possibly specify and verify that kinds of desired properties
using semantics to eliminate boot time failures, 
for example, in case that even SDN apps are running in real time for dynamic
network topology or resources updates. 
Of course, it may be very hard enough in large scaled, real-time/critical
networks.
If you have any other further issues, please let us know. It could be very
helpful to us to take up this challenge.

Thanks, 
Myung-Ki, 

From: [email-masked] [mailto:[email-masked]] On Behalf Of
[email-masked]
Sent: Thursday, August 02, 2012 8:59 AM
To: [email-masked]
Cc: [email-masked]
Subject: [Sdn] Formal Specification to include boot process?

Myung-Ki & co-authors,

If time had permitted, I would have asked this question from the floor just
now, but the list is next best...

I imagine the formal specification problem is hard enough without
considering boot time, but I'm interested in how and whether a network can
boot after various failures of individual nodes (and secondarily, whether it
could go through a vulnerable state while booting). 

I don't know much about the limitations of these specfication languages, but
you sound like you do. Do you think this would be possible? If you're
interested in taking up this challenge, that would be cool.

Bob