Exploring Architectural Model Checking with Declarative Specifications

Abstract

In this work we explore the FVS language in the context of architectural behavior model checking. FVS holds desirable characteristics for this particular domain. Its flexible notation enables the possibility of performing behavioral exploration when denoting the properties to be satisfied. In addition, FVS expressive power capable of denoting ω-regular properties is useful to denote behavior in a higher level of abstraction. These are two key activities when specifying and validating a system architecture. Given that FVS specifications can be translated into B¨uchi automata they can be used as input in a validation tool like model checkers. In this sense, we conducted industrial relevant case studies to apply our approach in concrete examples.