Specification and verification of reactive systems using a deductive database

We present an approach to the specification and verification of concurrent systems, by means of a deductive database management system. The approach is based on the synthesis of logic formulas: starting from a temporal logic formula (ACTL logic formula), that represents the requirements of a system, a general model for such formula, is derived. From this model, all the concurrent systems satisfying the formula can be generated. Moreover, we show that this model can be used to verify when a given system, obtained elsewhere, satisfies its requirements expressed by logical specifications.

Sommario non disponibile.