Aiding Modular Design and Verification of Safety-Critical Time-Triggered Systems by Use of Executable Formal Specifications