opaal is a model checker with the design goals of enabling rapid prototyping, being easy to learn and being sufficiently fast. It should be the first tool used when wanting to try out a model checking concept, therefore it needs to be open source. It should be so easy to learn that a group of undergraduate students can implement something useful with it in one semester. This requires readability, good overview and loose coupling. It should be sufficiently fast, by implementing the low-hanging optimisation fruit - gold plating is forbidden!
The design criteria for opaal is:
- Rapid prototyping
- Easy to learn
- 80-20 rule for optimisations
1. Rapid prototyping
Try out concepts quickly
Before doing more time-consuming, optimised implementation
Open Source
2. Easy to learn
A group of 5th semester students should be able to implement
something in a project
Readability, overview, loose coupling
3. Implement the 20% of the optimisations that give 80% of the speedup
No gold plating
Sufficiently fast
We learn as we go
Site under construction
Please see https://launchpad.net/opaal for even less information!