Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems