2019/08/19 by Marius Bozga, Bozga, Marius, Radu Iosif +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.1908.11345
openalex publication_date 2019/08/19 · openalex created_date 2019/09/05 · openalex updated_date 2026/07/28
We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components can migrate at runtime on a physical map, whose shape and size may change. We describe such parametric and reconfigurable architectures using resource logics, close in spirit to Separation Logic, used to reason about dynamic pointer structures. These logics support the principle of local reasoning, which is the key for writing modular specifications and building scalable verification algorithms, that deal with large industrial-size systems.