The ProtoCollum team has a number of exciting plans and ideas for
future development of the tool. Some of these are discussed below.
Feel free to contact us if you have an interest in partnering
in some of these development efforts.
Reading 100's of pages of protocol specification written in English is not a great way
to have fun. The language is obviously inaccurate for describing a logical system, but
sorting through 100's of lines of obscure modeling code is also difficult.
A better way to learn a protocol is to actually use it and watch it in action insideof
ProtoCollum. Creating ProtoCollum models for some of the standard protocols
is an interesting area of work. We are currently working on a model of the 802.11 Wireless
LAN protocol to use as an educational device.
We are considering the following ideas on how the dynamic ProtoCollum and the static
formal verification tools might work together. The obvious goal is to use the strength of
each to best advantage.
ProtoCollum has an advantage when it comes to rapidly capturing the protocol and
insuring it is meeting the architects intentions by subjecting it to simulation. But at
certain points during development it would be great to subject the design to a formal
check.
One of the demo files was created by taking a SPIN description and turning it into a
ProtoCollum model. It was fairly straight forward work, after a while almost
methodical. So the question arises, would it be possible to write an add-on package
that could do it the other way, take a ProtoCollum description and algorithmically generate from it
a PROMELA description for the SPIN formal tool (or any other formal tool)?
Essentially this would provide a graphical capture front-end for a formal tool.
It would help the obviate the need for an engineer to learn yet another language, and
the formal languages are notoriously difficult.
Other ideas under consideration for ProtoCollum:
- generate official Message Sequence Charts (MSC) from Edit and Test sheets
- use as a graphical protocol analyzer
- use as a runtime rule checker
|