Skoči na glavni sadržaj

Izvorni znanstveni članak

A Formalism and a Verification Method for Bus-Based Systems

Felice Balarin ; Cadence Berkeley Laboratories, Berkeley, USA


Puni tekst: engleski pdf 6.786 Kb

str. 157-168

preuzimanja: 151

citiraj


Sažetak

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.

Ključne riječi

formal verification; automata; iterative arrays; abstraction

Hrčak ID:

150424

URI

https://hrcak.srce.hr/150424

Datum izdavanja:

30.9.1995.

Posjeta: 447 *