Syntax and semantics of PRETSEL-a specification language for parallel real-time systems

For many real-time applications (e.g. command, control, and communications), parallel computers offer a natural computing platform. However, very little attention has been paid to the specification requirements of real-time systems implemented on parallel machines. Towards this end, we propose a specification language PRETSEL (Parallel Real-Time Specification Language). The PRETSEL specification language is based on a traditional two-level view of parallel computing whereby a parallel computation is viewed as a collection of interacting (data) parallel algorithms. This view is naturally reflected in PRETSEL syntax where at the lower level various constructs are provided for the specification of a data-parallel real-time algorithm (data-parallelism). At the upper level another set of constructs is provided to combine such tasks in a variety of way (task-parallelism). Furthermore, the PRETSEL language allows for the specification of performance requirements. PRETSEL is currently being evaluated for real-time avionics applications. We describe the syntax and operational semantics of PRETSEL and establish results relating the functional and the temporal behaviors