VERIFICATION AND IMPLEMENTATION OF SHIFT MODELS
Sergio Yovine · 1998
This report documents work carried out directed at both verifying the correctness of SHIFT specifications and generating code to be executed on-board in real-time. SHIFT is a specification language oriented towards the modeling of hybrid systems that comprise both discrete and continuous behaviors over time. The report discusses the verification process and gives an overview of the code generation process.