Automata with Parameterized Arrays and Parameterized Networks of Automata

formal verification, parametric verification, automated verification, concurrent systems, extended automata

The goal of this study is to propose a common basis for describing a large class of systems with a somehow parameterized (process and/or data) structure. We propose automata working with generalized, parametric arrays to be used for this purpose. Indeed, entries of such arrays with parameterized bounds may hold control states and local data of processes whose parametric number appears in the modelled systems. Parameterized arrays may also directly correspond to parameterized memory structures (as, e.g., cache tables) present in the systems being investigated. In addition to the above, we further propose a concept of parametric networks of automata with arrays which can be viewed as a higher-level and in some situations easier to use modelling tool that may, however, be defined in the terms of the basic automata with arrays. In models based on the parametric networks of automata, we allow global as well as local parametric arrays to be used.