Ticc-paradigm to build formally verified parallel software for multi-core chips

摘要: This invention teaches a way of implementing formally verified massively parallel programs, which run efficiently in distributed and shared-memory multi-core chips. It allows programs to be developed from an initial abstract statement interactions among software components, called cells, progressively refine them their final implementation. At each stage refinement formal description patterns events computations is derived automatically implementations. used for two purposes: One prove correctness, timings, progress, mutual exclusion, freedom deadlocks/livelocks, etc. The second incorporate into application Self-Monitoring System (SMS) that constantly monitors the parallel, with no interference its identify report errors performance, pending errors, critical behavior. also organizing multi-processors minimizes memory interference, protects data increases execution efficiency.