Differences

This shows you the differences between two versions of the page.

Link to this comparison view

vv-lab:scenario-based-specification-and-verification [2015/02/18 22:47] (current)
egm created
Line 1: Line 1:
 +'''​Automate the construction of a formal model suitable for protocol verification from live sequence diagrams drawn in Visio'''​
  
 +Reduce the time it takes to get meaningful feedback to protocol architects. ​  Quick feedback yields fewer bugs.  Currently, the process of taking what the architects draw and turning those designs into a formal model suitable for analysis is fully manual. ​ Moreover, the process is tedious and error prone. ​ As a results, it takes significant time from when the architect is thinking about and designing a protocol to when a verification engineer is actually able to report to the architect the correctness of the protocol. ​ Reducing the feedback time means the architect is being presented with concerns while the protocol is fresh in the mind. More importantly,​ the verification engineer spends more time probing the behavior of the protocol and less time constructing the formal model from the architect drawings.
 +
 +== Modeling Assumptions ==
 +* Each agent has a single channel connecting it to other agents with which it directly communicates
 +* If communication is in both direction between agents, then two channels are required to handle both the ''​send''​ and ''​receive''​ traffic for a given agent
 +* Each channel has a unique language defined over the set of possible messages sent on the channel
 +* Message re-ordering (i.e., co-regions) and buffering is handled by the agents and must be modeled as part of their internal state
 +* Synchronous message are not buffered
 +* Asynchronous messages are buffered
 +
 +== Open Questions ==
 +* How are variables and constants expressed in the LSC diagram?
 +* Given several protocol definitions,​ how to you connect them amongst several different blocks. ​ For example if you have a set of agents that are connected with each interface using a different protocol, how would you express this in the diagram?
 +* How is an explicit clock managed where a Kleene-star is intermixed with express clock actions (see bvci protocol)?
vv-lab/scenario-based-specification-and-verification.txt ยท Last modified: 2015/02/18 22:47 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0