Static checking of system behaviors using derived component assumptions
A critical challenge faced by the developer of a software system is to understand whether the system's components correctly integrate. While type theory has provided substantial help in detecting and preventing errors in mismatched static properties, much work remains in the area of dynamics. I...
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_1049331X_v9_n3_p239_Inverardi |
| Aporte de: |
| id |
todo:paper_1049331X_v9_n3_p239_Inverardi |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_1049331X_v9_n3_p239_Inverardi2023-10-03T15:58:38Z Static checking of system behaviors using derived component assumptions Inverardi, P. Wolf, A.L. Yankelevich, D. Assumptions Chemical Abstract Machine model Component-based systems Design Static analysis Theory Verification A critical challenge faced by the developer of a software system is to understand whether the system's components correctly integrate. While type theory has provided substantial help in detecting and preventing errors in mismatched static properties, much work remains in the area of dynamics. In particular, components make assumptions about their behavioral interaction with other components, but currently we have only limited ways in which to state those assumptions and to analyze those assumptions for correctness. We have formulated a method that begins to address this problem. The method operates at the architectural level so that behavioral integration errors, such as deadlock, can be revealed early and at a high level. For each component, a specification is given of its interaction behavior. From this specification, assumptions that the component makes about the corresponding interaction behavior of the external context are automatically derived. We have defined an algorithm that performs compatibility checks between finite representations of a component's context assumptions and the actual interaction behaviors of the components with which it is intended to interact. A configuration of a system is possible if and only if a successful way of matching actual behaviors with assumptions can be found. The state-space complexity of this algorithm is significantly less than that of comparable approaches, and in the worst case, the time complexity is comparable to the worst case of standard reachability analysis. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_1049331X_v9_n3_p239_Inverardi |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Assumptions Chemical Abstract Machine model Component-based systems Design Static analysis Theory Verification |
| spellingShingle |
Assumptions Chemical Abstract Machine model Component-based systems Design Static analysis Theory Verification Inverardi, P. Wolf, A.L. Yankelevich, D. Static checking of system behaviors using derived component assumptions |
| topic_facet |
Assumptions Chemical Abstract Machine model Component-based systems Design Static analysis Theory Verification |
| description |
A critical challenge faced by the developer of a software system is to understand whether the system's components correctly integrate. While type theory has provided substantial help in detecting and preventing errors in mismatched static properties, much work remains in the area of dynamics. In particular, components make assumptions about their behavioral interaction with other components, but currently we have only limited ways in which to state those assumptions and to analyze those assumptions for correctness. We have formulated a method that begins to address this problem. The method operates at the architectural level so that behavioral integration errors, such as deadlock, can be revealed early and at a high level. For each component, a specification is given of its interaction behavior. From this specification, assumptions that the component makes about the corresponding interaction behavior of the external context are automatically derived. We have defined an algorithm that performs compatibility checks between finite representations of a component's context assumptions and the actual interaction behaviors of the components with which it is intended to interact. A configuration of a system is possible if and only if a successful way of matching actual behaviors with assumptions can be found. The state-space complexity of this algorithm is significantly less than that of comparable approaches, and in the worst case, the time complexity is comparable to the worst case of standard reachability analysis. |
| format |
JOUR |
| author |
Inverardi, P. Wolf, A.L. Yankelevich, D. |
| author_facet |
Inverardi, P. Wolf, A.L. Yankelevich, D. |
| author_sort |
Inverardi, P. |
| title |
Static checking of system behaviors using derived component assumptions |
| title_short |
Static checking of system behaviors using derived component assumptions |
| title_full |
Static checking of system behaviors using derived component assumptions |
| title_fullStr |
Static checking of system behaviors using derived component assumptions |
| title_full_unstemmed |
Static checking of system behaviors using derived component assumptions |
| title_sort |
static checking of system behaviors using derived component assumptions |
| url |
http://hdl.handle.net/20.500.12110/paper_1049331X_v9_n3_p239_Inverardi |
| work_keys_str_mv |
AT inverardip staticcheckingofsystembehaviorsusingderivedcomponentassumptions AT wolfal staticcheckingofsystembehaviorsusingderivedcomponentassumptions AT yankelevichd staticcheckingofsystembehaviorsusingderivedcomponentassumptions |
| _version_ |
1782024220951183360 |