A syntactic-semantic approach to incremental verification

File Description SizeFormat 
1304.8034v2.pdfPublished version205.25 kBAdobe PDFView/Open
Title: A syntactic-semantic approach to incremental verification
Authors: Bianculli, D
Filieri, A
Ghezzi, C
Mandrioli, D
Item Type: Working Paper
Abstract: Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices for evolving systems. Since changes in these systems are often local to restricted parts, an incremental verification approach could be beneficial. This paper introduces SiDECAR, a general framework for the definition of verification procedures, which are made incremental by the framework itself. Verification procedures are driven by the syntactic structure (defined by a grammar) of the system and encoded as semantic attributes associated with the grammar. Incrementality is achieved by coupling the evaluation of semantic attributes with an incremental parsing technique. We show the application of SiDECAR to the definition of two verification procedures: probabilistic verification of reliability requirements and verification of safety properties.
Issue Date: 30-Apr-2013
URI: http://hdl.handle.net/10044/1/33708
Copyright Statement: © The Author(s) 2013.
Keywords: cs.SE
D.2.4; D.3.4
Publication Status: Unpublished
Appears in Collections:Faculty of Engineering

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commonsx