High-Level Timed Petri Nets as a kernel for executable specifications