Formal Specification and Verification of Structural Views for Component and Connector Architectures

Speaker

Jan Oliver Ringert (Informatik 3)
Title Formal Specification and Verification of Structural Views for Component and Connector Architectures
When 19.09.2012, 10:00
Where Room 5052
Abstract We present a views specification language, which we call ArcV, for the structure of component and connector (C&C) architectures.  ArcV views are under-specified, partial models, which serve to represent the concerns of interest of and the incomplete knowledge about the structure of the system available to different stakeholders involved in the system development process.  As such, they provide several powerful means for abstraction and may cross-cut the hierarchical, implementation-oriented decomposition of systems to sub-systems. An ArcV specification consists of a Boolean expression over ArcV views, allowing one to specify, e.g., positive views, which should be satisfied, negative ones, which should not be satisfied, disjunctions, to allow one to express alternative designs, and implications, to allow one to express dependencies between design decisions.

As a primary application of ArcV, we provide a fully automatic formal verification technique that decides whether the structure of a given C&C architecture satisfies an ArcV specification.  In addition to deciding satisfaction, the technique outputs informative, minimal witnesses to justify satisfaction or non satisfaction, per view, as applicable. These generated witnesses are themselves ArcV views, that is, presented in the same language, and hence enable presentation, comprehension, and further analysis and manipulation with minimal additional learning effort.

We have defined ArcV on top of MontiArc, an architecture description language developed at RWTH Aachen. Examples and a prototype implementation demonstrate the usefulness of ArcV and its contribution to the state-of-the-art and practice in the formal specification and analysis of software architectures.
Slides