Formalisation and Analysis of Component Dependencies
This work addresses the problem of efficient system verification for developers and engineers, but it appears incremental as it builds on existing formal methods without introducing a new paradigm.
The paper tackles the problem of analyzing data dependencies between components to determine which parts of a system are necessary for checking a given property, resulting in a formalisation in Isabelle/HOL+Isar that enables efficient system structure analysis.
This set of theories presents a formalisation in Isabelle/HOL+Isar of data dependencies between components. The approach allows to analyse system structure oriented towards efficient checking of system: it aims at elaborating for a concrete system, which parts of the system (or system model) are necessary to check a given property.