Integrating the verification of timing, performance and correctness properties of concurrent systems

摘要

Previous methods of verification tend to keep correctness, timing and performance separate. We present a process algebra based methodology for the integrated modelling and verification of correctness, performance and timing properties of concurrent systems. We have applied the method to the domain of asynchronous hardware and used an asynchronous micropipeline as an illustrative example.