Evaluating different processes of translating OCL to PVS using model transformation Conference Paper