PostScript
Model Checking for Software Architectures
Radu Mateescu
Proceedings of the 1st European Workshop on Software Architecture
EWSA'2004 (St Andrews, Scotland), May 2004
Abstract:
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 | |
PostScript |
| Slides of R. Mateescu's lecture at EWSA'2004 | |