Active-passive deterministic parallel system specification using Z

摘要

Z is a powerful formal notation for system specification and modeling. However, Z does not model temporal information well. This is especially important for ractive concurrent systems. For other types of concurrent systems where system interactions occur in active-passive fashion, Z can be used effectively. The paper will first describe various parallel system types and then report on extending Z for reactive concurrent systems. Finally, it presents the concurrent systems. Finally, it presents the concurrent passive-active systems that do not use temporal notation and shows the example of the ripple counter logic specification in Z.