Conventional formal verification techniques rely on the assumption that a system's specification is completely available so that the analysis can say whether or not a set of properties will be satisfied. On the contrary, modern development lifecycles call for agileincremental and iterativeapproaches to tame the boosting complexity of modern software systems and reduce development risks. We focus here on requirements verification performed in the early exploratory stages on high-level models and we discuss how this can be integrated into an agile approach. We present a new technique to model-check incomplete high-level specifications against formally specified requirements. We do this in the context of incomplete hierarchical Statecharts, verified against a variation of CTL properties. Our approach supports step-wise specification and refinement verification. Verification can be incremental, that is alternative refinements may be separately explored and verification is only replayed for the modified parts. The results are presented by introducing the formalisms, the model-checking algorithm, and the tool we have implemented. © 2013 IEEE.

(2013). On requirements verification for model refinements . Retrieved from https://hdl.handle.net/10446/237233

On requirements verification for model refinements

Menghi, Claudio;
2013-01-01

Abstract

Conventional formal verification techniques rely on the assumption that a system's specification is completely available so that the analysis can say whether or not a set of properties will be satisfied. On the contrary, modern development lifecycles call for agileincremental and iterativeapproaches to tame the boosting complexity of modern software systems and reduce development risks. We focus here on requirements verification performed in the early exploratory stages on high-level models and we discuss how this can be integrated into an agile approach. We present a new technique to model-check incomplete high-level specifications against formally specified requirements. We do this in the context of incomplete hierarchical Statecharts, verified against a variation of CTL properties. Our approach supports step-wise specification and refinement verification. Verification can be incremental, that is alternative refinements may be separately explored and verification is only replayed for the modified parts. The results are presented by introducing the formalisms, the model-checking algorithm, and the tool we have implemented. © 2013 IEEE.
2013
Ghezzi, Carlo; Menghi, Claudio; Sharifloo, Amir Molzam; Spoletini, Paola
File allegato/i alla scheda:
File Dimensione del file Formato  
RE.2013.6636706.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 1.15 MB
Formato Adobe PDF
1.15 MB Adobe PDF   Visualizza/Apri
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/237233
Citazioni
  • Scopus 15
  • ???jsp.display-item.citation.isi??? 7
social impact