07/08/06: Topsy in Spin

Spin model of Topsy for verification of task isolation

The whole archive: topsy_spin.tar.gz

Contents overview:

• Model for the kernel and a test application
• Common LTL definitions
• LTL definition of status correctness
• LTL definition of status consistency
• LTL definition of reply consistency
• Memory isolation
• Makefile for individual verification
• Perform all the verifications
• Collect memory-consumption results
• Collect execution-time results