Reference : A Syntactic-Semantic Approach to Incremental Verification
E-prints/Working papers : Already available on another site
Engineering, computing & technology : Computer science
A Syntactic-Semantic Approach to Incremental Verification
Bianculli, Domenico mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Filieri, Antonio [> >]
Ghezzi, Carlo [> >]
Mandrioli, Dino [> >]
[en] 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.

File(s) associated to this reference

Fulltext file(s):

Open access
incremental-tr.pdfAuthor postprint335.45 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.