Refactoring design models for inductive verification

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

6 Scopus citations

Abstract

Systems composed of many identical processes can sometimes be verified inductively using a network invariant, but systems whose component, processes vary in some systematic way are not amenable to direct application of that method. We describe how variations in behavior can be "factored out" into additional processes, thus enabling induction over the number of processes. The process is semi-automatic: The designer must choose from among a set of idiomatic transformations, but each transformation is applied and checked automatically.

Original languageEnglish
Title of host publicationProceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis
EditorsP.G. Frankl
PublisherAssociation for Computing Machinery (ACM)
Pages164-168
Number of pages5
ISBN (Print)1581135629, 9781581135626
DOIs
StatePublished - 2002
EventISSTA 02 Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis - Roma, Italy
Duration: 22 Jul 200224 Jul 2002

Publication series

NameProceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis

Conference

ConferenceISSTA 02 Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis
Country/TerritoryItaly
CityRoma
Period22/07/0224/07/02

Keywords

  • Compositional Analysis
  • Concurrency
  • Network Invariants
  • Parameterized System
  • Refactoring

Cite this