ON THE CORRECTNESS OF SOFTWARE ARCHITECTURES - Formal Specification of Correctness Properties using π-AAL

Flavio Oquendo

2009

Abstract

Software has become a critical part of a rapidly growing range of products and services. Key aspects of the development of such software-intensive systems are the description and analysis of their software architecture, encompassing both the formal model of the component-based architecture and the formal specification of the correctness properties that the modeled architecture must satisfy. Therefore, an Architecture Description Language (ADL) must be complemented by an Architecture Analysis Language (AAL) enabling the specification of architecture-related correctness properties. A major challenge for an AAL is to provide ade-quate expressive power to specify both structural and behavioral correctness properties, and to be well-suited for machine-automated processing for verification, at a time. This paper presents how π-AAL complements π-ADL (designed in the ArchWare European Project) for enabling the specification of architectural correctness properties based on the modal π-calculus. The toolset and its experimentation in industrial pilot projects are outlined.

Paper Citation

in Harvard Style

Oquendo F. (2009). ON THE CORRECTNESS OF SOFTWARE ARCHITECTURES - Formal Specification of Correctness Properties using π-AAL . In Proceedings of the 4th International Conference on Software and Data Technologies - Volume 1: ICSOFT, ISBN 978-989-674-009-2, pages 208-217. DOI: 10.5220/0002256302080217

in Bibtex Style

@conference{icsoft09,
author={Flavio Oquendo},
title={ON THE CORRECTNESS OF SOFTWARE ARCHITECTURES - Formal Specification of Correctness Properties using π-AAL},
booktitle={Proceedings of the 4th International Conference on Software and Data Technologies - Volume 1: ICSOFT,},
year={2009},
pages={208-217},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002256302080217},
isbn={978-989-674-009-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 4th International Conference on Software and Data Technologies - Volume 1: ICSOFT,
TI - ON THE CORRECTNESS OF SOFTWARE ARCHITECTURES - Formal Specification of Correctness Properties using π-AAL
SN - 978-989-674-009-2
AU - Oquendo F.
PY - 2009
SP - 208
EP - 217
DO - 10.5220/0002256302080217