Naslov
Verification of System Level Model Transformations

Autori
Abdi, S. ; Gajski, Danijel

Izvornik
International Journal of Parallel Programming (0885-7458) 34 (2006), 1; 29-59

Vrsta, podvrsta i kategorija rada
Radovi u časopisima, članak, znanstveni

Ključne riječi
design methodology; model transformations; system level modeling; verification

Sažetak
This paper presents Model Algebra (MA), a formalism for representing SoC designs at system level. We define the objects and composition rules of MA and show how system level models can be represented as expressions in this formalism. The formalism is applied to a system level design methodology, where design decisions are used to gradually transform the functional specification model of the system to a transaction level model with components and communication structure. Each transformation is represented as a manipulation of a model algebraic expression, and proven for correctness using the laws of model algebra. These laws are based on the well defined execution semantics and notion of functional equivalence for MA models. Our approach promises significant savings in the verification of system level models because only the first model needs to be verified using conventional techniques. All transformations of this model, derived using MA laws, are proven to be functionally equivalent.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA