Model Checking for Software Architectures

Radu Mateescu

Proceedings of the 1st European Workshop on Software Architecture EWSA'2004 (St Andrews, Scotland), May 2004


Software architectures are engineering artifacts which provide high-level descriptions of complex systems. Certain recent architecture description languages (ADLs) allow to represent a system's structure and behaviour together with its dynamic changes and evolutions. Model checking techniques offer a useful way for automatically verifying finite-state ADL descriptions w.r.t. their desired correctness requirements. In this position paper, we discuss several issues related to the application of model checking in the area of software architectures, underlining the aspects of interest for current and future research (construction of state spaces, expression and verification of requirements, state explosion).

6 pages


Slides of R. Mateescu's lecture at EWSA'2004