A Syntactic-Semantic Approach to Incremental Verification

Reference : A Syntactic-Semantic Approach to Incremental Verification


	Document type :	E-prints/Working papers : Already available on another site
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/10993/8383

Title :	A Syntactic-Semantic Approach to Incremental Verification
Language :	English
Author, co-author :	Bianculli, Domenico [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Filieri, Antonio [> >]
	Ghezzi, Carlo [> >]
	Mandrioli, Dino [> >]
Publication date :	2013
Publisher :	`
Number of pages :	22
Peer reviewed :	No
Abstract :	[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.
Permalink :	http://hdl.handle.net/10993/8383
source URL :	http://arxiv.org/abs/1304.8034

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	incremental-tr.pdf		Author postprint	335.45 kB	View/Open

All documents in ORBi^lu are protected by a user license.