Embedded systems are electronic devices that function in the context of a real environment, by sensing and reacting to a set of stimuli. Because of their close interaction with the environment, and to simplify their design, different parts of an embedded system are best described using different notations and different techniques. In this case, we say that the system is heterogeneous. We informally refer to the notation and the rules that are used to specify and verify the elements of heterogeneous system and their collective behavior as a model of computation. In this paper, we particular on abstraction and refinement relationships in the form of conservative approximations. We do so by constructing a framework, called Agent Algebra, where the different models reside and share a common algebraic structure. We compare our es to the well established notion of abstract interpretation. We show that, unlike abstract interpretations, conservative approxipreserve refinement verification ...
Roberto Passerone, Jerry R. Burch, Alberto L. Sang