Istituto di Scienza e Tecnologie dell'Informazione     
Asirelli P., Gnesi S. Specification and verification of reactive systems using a deductive database. In: 2nd International Workshop on Verification, Model Checking and Abstract Interpretation (Pisa, Italy, 19 September 1998). Proceedings, A. Bossi, A. Cortesi, F. Levi (eds.). Universita' Ca' Foscari di Venezia, 1998.
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.
Subject Model checking
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional