Model Checking for Software Architectures

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 finitestate 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).

• Type: Conference
• Year: 2004
• Where: EWSA
• Authors: Radu Mateescu
• Keywords: EWSA 2004, Model Checking, Model Checking Techniques, Software Architectures