Paper Info
Title
Formal Specification and Verification of Dynamic Parametrized 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 a Satisfiability Modulo Theories (SMT)-based model checker to tackle a number of case studies.
Year
DOI
Venue
2018
10.1007/978-3-319-95582-7_37
Lecture Notes in Computer Science
Field
DocType
Volume
Transition system,Information flow (information theory),Model checking,Adaptive system,Computer science,Formal specification,Reachability,Theoretical computer science,Control reconfiguration,Satisfiability modulo theories
Conference
10951
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
17
3
Name
Order
Citations
PageRank
Alessandro Cimatti15064323.15
Ivan Stojic200.68
Stefano Tonetta357341.61