Original scientific paper
A Formalism and a Verification Method for Bus-Based Systems
Felice Balarin
; Cadence Berkeley Laboratories, Berkeley, USA
Abstract
Bus-based systems consist of many similar components which communicate through a fixed channel. We propose a formal model for such systems, using finite-state automata to model behavior of components, and logic formulas to model bus arbitration. For this purpose, we define the indexed propositional logic, show that it has a small model property, and use that property to construct an abstraction of bus-based systems which does not depend on the actual number of components. We show that the proposed formalism can be used to model buses at various levels of abstraction.
Keywords
formal verification; automata; iterative arrays; abstraction
Hrčak ID:
150424
URI
Publication date:
30.9.1995.
Visits: 475 *