On requirement verification for evolving Statecharts specifications.
Saved in:
| Title: | On requirement verification for evolving Statecharts specifications. |
|---|---|
| Authors: | Ghezzi, Carlo1 ghezzi@elet.polimi.it, Menghi, Claudio1 menghi@elet.polimi.it, Molzam Sharifloo, Amir1 molzam@elet.polimi.it, Spoletini, Paola2 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 97444904 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: On requirement verification for evolving Statecharts specifications. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Ghezzi%2C+Carlo%22">Ghezzi, Carlo</searchLink><relatesTo>1</relatesTo><i> ghezzi@elet.polimi.it</i><br /><searchLink fieldCode="AR" term="%22Menghi%2C+Claudio%22">Menghi, Claudio</searchLink><relatesTo>1</relatesTo><i> menghi@elet.polimi.it</i><br /><searchLink fieldCode="AR" term="%22Molzam+Sharifloo%2C+Amir%22">Molzam Sharifloo, Amir</searchLink><relatesTo>1</relatesTo><i> molzam@elet.polimi.it</i><br /><searchLink fieldCode="AR" term="%22Spoletini%2C+Paola%22">Spoletini, Paola</searchLink><relatesTo>2</relatesTo><i> paola.spoletini@uninsubria.it</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Requirements+Engineering%22">Requirements Engineering</searchLink>. Sep2014, Vol. 19 Issue 3, p231-255. 25p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Statecharts+%28Computer+science%29%22">Statecharts (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+development%22">Computer software development</searchLink><br /><searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Unified+modeling+language%22">Unified modeling language</searchLink><br /><searchLink fieldCode="DE" term="%22Iterative+methods+%28Mathematics%29%22">Iterative methods (Mathematics)</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=97444904 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s00766-013-0198-z Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 25 StartPage: 231 Subjects: – SubjectFull: Statecharts (Computer science) Type: general – SubjectFull: Computer software development Type: general – SubjectFull: Software verification Type: general – SubjectFull: Unified modeling language Type: general – SubjectFull: Iterative methods (Mathematics) Type: general Titles: – TitleFull: On requirement verification for evolving Statecharts specifications. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Ghezzi, Carlo – PersonEntity: Name: NameFull: Menghi, Claudio – PersonEntity: Name: NameFull: Molzam Sharifloo, Amir – PersonEntity: Name: NameFull: Spoletini, Paola IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 09 Text: Sep2014 Type: published Y: 2014 Identifiers: – Type: issn-print Value: 09473602 Numbering: – Type: volume Value: 19 – Type: issue Value: 3 Titles: – TitleFull: Requirements Engineering Type: main |
| ResultId | 1 |
