Behavioral compatibility without state explosion: Design and verification of a component-based elevator control system

Paul C. Attie, David H. Lorenz, Aleksandra Portnova, Hana Chockler

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Most methods for designing component-based systems and verifying their compatibility address only the syntactic compatibility of components; no analysis of run-time behavior is made. Those methods that do address run-time behavior suffer from state-explosion: the exponential increase of the number of global states, and hence the complexity of the analysis, with the number of components. We present a method for designing component-based systems and verifying their behavioral compatibility and temporal behavior that is not susceptible to state explosion. Our method is mostly automatic, with little manual deduction required, and does not analyze a large system of connected components at once, but instead analyzes components two-at-a-time. This pair-wise approach enables the automatic verification of temporal behavior, using model-checking, in time polynomial in the number and size of all components. Our method checks that behavior of a pair of interacting components conforms to given properties, specified in temporal logic. Interaction of the components is captured in a product of their behavioral automata, which are provided as a part of each component's interface. We demonstrate the effectiveness of our method by applying it to the design and verification of a component-based elevator control algorithm.

Original languageEnglish (US)
Title of host publicationComponent-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings
PublisherSpringer Verlag
Pages33-49
Number of pages17
ISBN (Print)3540356282, 9783540356288
DOIs
StatePublished - Jan 1 2006
Externally publishedYes
Event9th International Symposium on Component-Based Software Engineering, CBSE 2006 - Vasteras, Sweden
Duration: Jun 29 2006Jul 1 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4063 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Symposium on Component-Based Software Engineering, CBSE 2006
CountrySweden
CityVasteras
Period6/29/067/1/06

Fingerprint

Component-based Systems
Elevators
Explosion
Compatibility
Explosions
Control System
Control systems
Temporal logic
Model checking
Syntactics
Polynomials
Automatic Verification
Number of Components
Deduction
Temporal Logic
Design
Connected Components
Model Checking
Control Algorithm
Automata

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Attie, P. C., Lorenz, D. H., Portnova, A., & Chockler, H. (2006). Behavioral compatibility without state explosion: Design and verification of a component-based elevator control system. In Component-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings (pp. 33-49). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4063 LNCS). Springer Verlag. https://doi.org/10.1007/11783565_3

Behavioral compatibility without state explosion : Design and verification of a component-based elevator control system. / Attie, Paul C.; Lorenz, David H.; Portnova, Aleksandra; Chockler, Hana.

Component-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings. Springer Verlag, 2006. p. 33-49 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4063 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Attie, PC, Lorenz, DH, Portnova, A & Chockler, H 2006, Behavioral compatibility without state explosion: Design and verification of a component-based elevator control system. in Component-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4063 LNCS, Springer Verlag, pp. 33-49, 9th International Symposium on Component-Based Software Engineering, CBSE 2006, Vasteras, Sweden, 6/29/06. https://doi.org/10.1007/11783565_3
Attie PC, Lorenz DH, Portnova A, Chockler H. Behavioral compatibility without state explosion: Design and verification of a component-based elevator control system. In Component-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings. Springer Verlag. 2006. p. 33-49. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/11783565_3
Attie, Paul C. ; Lorenz, David H. ; Portnova, Aleksandra ; Chockler, Hana. / Behavioral compatibility without state explosion : Design and verification of a component-based elevator control system. Component-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings. Springer Verlag, 2006. pp. 33-49 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9f1a6efa6ab04f5284f655ab2cec9a28,
title = "Behavioral compatibility without state explosion: Design and verification of a component-based elevator control system",
abstract = "Most methods for designing component-based systems and verifying their compatibility address only the syntactic compatibility of components; no analysis of run-time behavior is made. Those methods that do address run-time behavior suffer from state-explosion: the exponential increase of the number of global states, and hence the complexity of the analysis, with the number of components. We present a method for designing component-based systems and verifying their behavioral compatibility and temporal behavior that is not susceptible to state explosion. Our method is mostly automatic, with little manual deduction required, and does not analyze a large system of connected components at once, but instead analyzes components two-at-a-time. This pair-wise approach enables the automatic verification of temporal behavior, using model-checking, in time polynomial in the number and size of all components. Our method checks that behavior of a pair of interacting components conforms to given properties, specified in temporal logic. Interaction of the components is captured in a product of their behavioral automata, which are provided as a part of each component's interface. We demonstrate the effectiveness of our method by applying it to the design and verification of a component-based elevator control algorithm.",
author = "Attie, {Paul C.} and Lorenz, {David H.} and Aleksandra Portnova and Hana Chockler",
year = "2006",
month = "1",
day = "1",
doi = "10.1007/11783565_3",
language = "English (US)",
isbn = "3540356282",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "33--49",
booktitle = "Component-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings",

}

TY - GEN

T1 - Behavioral compatibility without state explosion

T2 - Design and verification of a component-based elevator control system

AU - Attie, Paul C.

AU - Lorenz, David H.

AU - Portnova, Aleksandra

AU - Chockler, Hana

PY - 2006/1/1

Y1 - 2006/1/1

N2 - Most methods for designing component-based systems and verifying their compatibility address only the syntactic compatibility of components; no analysis of run-time behavior is made. Those methods that do address run-time behavior suffer from state-explosion: the exponential increase of the number of global states, and hence the complexity of the analysis, with the number of components. We present a method for designing component-based systems and verifying their behavioral compatibility and temporal behavior that is not susceptible to state explosion. Our method is mostly automatic, with little manual deduction required, and does not analyze a large system of connected components at once, but instead analyzes components two-at-a-time. This pair-wise approach enables the automatic verification of temporal behavior, using model-checking, in time polynomial in the number and size of all components. Our method checks that behavior of a pair of interacting components conforms to given properties, specified in temporal logic. Interaction of the components is captured in a product of their behavioral automata, which are provided as a part of each component's interface. We demonstrate the effectiveness of our method by applying it to the design and verification of a component-based elevator control algorithm.

AB - Most methods for designing component-based systems and verifying their compatibility address only the syntactic compatibility of components; no analysis of run-time behavior is made. Those methods that do address run-time behavior suffer from state-explosion: the exponential increase of the number of global states, and hence the complexity of the analysis, with the number of components. We present a method for designing component-based systems and verifying their behavioral compatibility and temporal behavior that is not susceptible to state explosion. Our method is mostly automatic, with little manual deduction required, and does not analyze a large system of connected components at once, but instead analyzes components two-at-a-time. This pair-wise approach enables the automatic verification of temporal behavior, using model-checking, in time polynomial in the number and size of all components. Our method checks that behavior of a pair of interacting components conforms to given properties, specified in temporal logic. Interaction of the components is captured in a product of their behavioral automata, which are provided as a part of each component's interface. We demonstrate the effectiveness of our method by applying it to the design and verification of a component-based elevator control algorithm.

UR - http://www.scopus.com/inward/record.url?scp=33746415276&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33746415276&partnerID=8YFLogxK

U2 - 10.1007/11783565_3

DO - 10.1007/11783565_3

M3 - Conference contribution

AN - SCOPUS:33746415276

SN - 3540356282

SN - 9783540356288

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 33

EP - 49

BT - Component-Based Software Engineering - 9th International Symposium, CBSE 2006, Proceedings

PB - Springer Verlag

ER -