On requirement verification for evolving Statecharts specifications.

Saved in:

Bibliographic Details
Title:	On requirement verification for evolving Statecharts specifications.
Authors:	Ghezzi, Carlo¹ ghezzi@elet.polimi.it, Menghi, Claudio¹ menghi@elet.polimi.it, Molzam Sharifloo, Amir¹ molzam@elet.polimi.it, Spoletini, Paola² paola.spoletini@uninsubria.it
Source:	Requirements Engineering. Sep2014, Vol. 19 Issue 3, p231-255. 25p.
Subjects:	Statecharts (Computer science), Computer software development, Software verification, Unified modeling language, Iterative methods (Mathematics)
Abstract:	Software development processes have been evolving from rigid, pre-specified, and sequential to incremental, and iterative. This evolution has been dictated by the need to accommodate evolving user requirements and reduce the delay between design decision and feedback from users. Formal verification techniques, however, have largely ignored this evolution and even when they made enormous improvements and found significant uses in practice, like in the case of model checking, they remained confined into the niches of safety-critical systems. Model checking verifies if a system's model $$\mathcal{M}$$ satisfies a set of requirements, formalized as a set of logic properties $$\Phi$$ . Current model-checking approaches, however, implicitly rely on the assumption that both the complete model $$\mathcal{M}$$ and the whole set of properties $$\Phi$$ are fully specified when verification takes place. Very often, however, $$\mathcal{M}$$ is subject to change because its development is iterative and its definition evolves through stages of incompleteness, where alternative design decisions are explored, typically to evaluate some quality trade-offs. Evolving systems specifications of this kind ask for novel verification approaches that tolerate incompleteness and support incremental analysis of alternative designs for certain functionalities. This is exactly the focus of this paper, which develops an incremental model-checking approach for evolving Statecharts. Statecharts have been chosen both because they are increasingly used in practice natively support model refinements. [ABSTRACT FROM AUTHOR]
	Copyright of Requirements Engineering is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	Software development processes have been evolving from rigid, pre-specified, and sequential to incremental, and iterative. This evolution has been dictated by the need to accommodate evolving user requirements and reduce the delay between design decision and feedback from users. Formal verification techniques, however, have largely ignored this evolution and even when they made enormous improvements and found significant uses in practice, like in the case of model checking, they remained confined into the niches of safety-critical systems. Model checking verifies if a system's model $$\mathcal{M}$$ satisfies a set of requirements, formalized as a set of logic properties $$\Phi$$ . Current model-checking approaches, however, implicitly rely on the assumption that both the complete model $$\mathcal{M}$$ and the whole set of properties $$\Phi$$ are fully specified when verification takes place. Very often, however, $$\mathcal{M}$$ is subject to change because its development is iterative and its definition evolves through stages of incompleteness, where alternative design decisions are explored, typically to evaluate some quality trade-offs. Evolving systems specifications of this kind ask for novel verification approaches that tolerate incompleteness and support incremental analysis of alternative designs for certain functionalities. This is exactly the focus of this paper, which develops an incremental model-checking approach for evolving Statecharts. Statecharts have been chosen both because they are increasingly used in practice natively support model refinements. [ABSTRACT FROM AUTHOR]
ISSN:	09473602
DOI:	10.1007/s00766-013-0198-z