Formal Specification and Verification of Dynamic Parametrized Architectures
| Autor: | Stefano Tonetta, Alessandro Cimatti, Ivan Stojic |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Model checking
Theoretical computer science Computer science 010102 general mathematics Control reconfiguration 02 engineering and technology 01 natural sciences Reachability Adaptive system Formal specification Satisfiability modulo theories Transition system 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0101 mathematics |
| Zdroj: | Formal Methods ISBN: 9783319955810 FM |
| DOI: | 10.1007/978-3-319-95582-7_37 |
| Popis: | 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 a Satisfiability Modulo Theories (SMT)-based model checker to tackle a number of case studies. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|