Provably Correct Architecture Refinement
Samar Abdi, Daniel D. Gajski · 2003
data channels can be synthesized to system busses and bus interfaces on components through communication synthesis. The rest of the paper is organized as follows. Section 2 will cover system model semantics and the notion of model equivalence. Section 3 will introduce model algebra and its axiomatization. Section 4 will present the architecture refinement step and proof of its correctness in the context of model algebra. We will finally wind up with conclusions and future work.