search
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)?
