An Efficient Specification Method of Asynchronous Control Modules in Model Checking

摘要

System verification plays an important role in large scale and complex systems. However, it is very difficult for designers other than the specialist who is well versed in Temporal Logic to specify behaviors of the system. This article considers the case where designers of systems can specify temporal formulas easily in system verification. We propose a method by which temporal formulas can be obtained inductively for specifications in system verification. System designers can easily derive complex temporal formulas by using the specification method.