Translation Validation of Transformations of Embedded System Specifications using Equivalence Checking

In the last two decades extensive research has been conducted addressing the design methodology of embedded systems and their verification. The initial behavioural specification of an embedded system goes through significant optimizing transformations, automated and also human-guided, before being mapped to an architecture. Establishing the validity of these transformations is crucial to ensure that the intended behaviour of a system has not been faultily altered during synthesis. State-of- the-art verification methods fail to cope with the complexity of the problem. So, we have devised some efficient translation validation methodologies to handle diverse code transformations; in the initial part of our work, we have worked with the Finite State Machine with Datapath (FSMD) model and its extension to validate various code motion techniques; in the latter part, we have designed an equivalence checking method around the Array Data-Dependence Graph (ADDG) model, which provides a more suitable framework to reason about index spaces of array variables, to verify loop transformations and arithmetic transformations in the presence of recurrences; we have also shown how to relate our path based equivalence checking mechanisms with that of bisimulation based verification techniques by deriving bisimulation relations from the outputs of our equivalence checkers.