"Whenever possible, the PCS on the called partition should allow for multiple tasks to call the RPC-receiver with different messages and should allow them to block until the corresponding subprogram body returns."
Followed by GLADE, a separately supplied PCS that can be used with GNAT.
"The Write operation on a stream of type Params_Stream_Type should raise Storage_Error if it runs out of space trying to write the Item into the stream."
Followed by GLADE, a separately supplied PCS that can be used with GNAT.