Tags:first-order logic, formal specification, formal verification, information flow, parametrized systems, SMT-based model checking and system architectures
Abstract:
We propose a novel approach to the formal specification and verification of dynamic architectures that are at the core of adaptive systems such as critical-infrastructure protection. Key features include run-time reconfiguration based on adding and removing components and connections, resulting in systems with unbounded number of components. We provide a logic-based specification of a Dynamic Parametrized Architecture (DPA), where parameters represent the infinite-state space of possible configurations, and first-order formulas represent the sets of initial configurations and reconfiguration transitions. We encode information flow properties as reachability problems of such DPAs, define a translation into an array-based transition system, and use an SMT-based model checker to tackle a number of case studies.
Formal Specification and Verification of Dynamic Parametrized Architectures