Verification of Software Requirements on Program Systems Represented by Attribute Transition Systems

Authors: Baranov S.N.¹; Volkov V.A.²; Godlevskii A.B.³; Kapitonova Y.V.⁴; Letichevsky A.A.⁵

Source: Cybernetics and Systems Analysis, Volume 39, Number 6, November 2003 , pp. 783-789(7)

Publisher: Springer

Buy & download fulltext article:

Price: $47.00 plus tax (Refund Policy)

Abstract:

An approach to the verification of requirements is presented. A formal requirement language is described and the properties to be checked are formulated. A scheme for proving some important dynamic properties is developed.

Keywords: consistency of requirements on programs; theorem proving; prover

Document Type: Research article

DOI: http://dx.doi.org/10.1023/B:CASA.0000020220.16822.36

Affiliations: 1: Closed Corporation "Motorola," St. Petersburg, Russia, Email: sergey.baranov@motorola.com 2: Cybernetics Institute, National Academy of Sciences of Ukraine, Kiev, Ukraine, Email: vlad@iss.org.ua 3: Cybernetics Institute, National Academy of Sciences of Ukraine, Kiev, Ukraine, Email: Alexander_Godlevsky@iss.org.ua 4: Cybernetics Institute, National Academy of Sciences of Ukraine, Kiev, Ukraine, Email: Julia_Kapitonova@iss.org.ua 5: Cybernetics Institute, National Academy of Sciences of Ukraine, Kiev, Ukraine, Email: let@iss.org.ua

Publication date: 2003-11-01