Parallel Refinement Mechanisms

Refinement is a fundamental design technique that has often challenged the\"formal methods\" community. In most cases, mathematical elegance and proofmanageability have been chosen over flexibility and freedom, which are oftenneeded in practice to deal with unexpected or critical situations. The issueof refinement becomes even more critical when dealing with real-time systemswhere timing analysis is a crucial factor. In this case, the literatureexhibits only a few, fairly limited proposals. In this paper, we proposegeneral refinement mechanisms for real-time systems that allow several types ofimplementation strategies to be specified in a fairly natural way. Notsurprisingly, generality has a price in terms of complexity. In our approach,however, this price is paid only when necessary. Furthermore, the proof systemis amenable both for traditional hand-proofs, based on human ingenuity and onlypartially formalized, and for fully formalized, tool-supported proofs.