hrcak mascot   Srce   HID

Izvorni znanstveni članak

A Formalism and a Verification Method for Bus-Based Systems

Felice Balarin ; Cadence Berkeley Laboratories, Berkeley, USA

Puni tekst: engleski, pdf (7 MB) str. 157-168 preuzimanja: 33* citiraj
APA 6th Edition
Balarin, F. (1995). A Formalism and a Verification Method for Bus-Based Systems. Journal of computing and information technology, 3 (3), 157-168. Preuzeto s https://hrcak.srce.hr/150424
MLA 8th Edition
Balarin, Felice. "A Formalism and a Verification Method for Bus-Based Systems." Journal of computing and information technology, vol. 3, br. 3, 1995, str. 157-168. https://hrcak.srce.hr/150424. Citirano 24.07.2019.
Chicago 17th Edition
Balarin, Felice. "A Formalism and a Verification Method for Bus-Based Systems." Journal of computing and information technology 3, br. 3 (1995): 157-168. https://hrcak.srce.hr/150424
Harvard
Balarin, F. (1995). 'A Formalism and a Verification Method for Bus-Based Systems', Journal of computing and information technology, 3(3), str. 157-168. Preuzeto s: https://hrcak.srce.hr/150424 (Datum pristupa: 24.07.2019.)
Vancouver
Balarin F. A Formalism and a Verification Method for Bus-Based Systems. Journal of computing and information technology [Internet]. 1995 [pristupljeno 24.07.2019.];3(3):157-168. Dostupno na: https://hrcak.srce.hr/150424
IEEE
F. Balarin, "A Formalism and a Verification Method for Bus-Based Systems", Journal of computing and information technology, vol.3, br. 3, str. 157-168, 1995. [Online]. Dostupno na: https://hrcak.srce.hr/150424. [Citirano: 24.07.2019.]

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

Posjeta: 58 *