Correctness by Construction for High-Integrity Real-Time Systems: A Metamodel-Driven Approach