A formal system-level synthesis model for the concurrent
object-oriented design of parallel computer systems, called Multi-token
Object-oriented Bi-directional net (MOBnet), is proposed. The MOBnet
model extends the standard Petri net by defining (1) multiple tokens to
represent different kinds of synthesis control information, (2)
object-oriented nodes (places) to denote the system parts under synthesis,
and (3) bi-directional arcs to model the design completion check and
synthesis rollback operations. In this paper, we first show that MOBnet
can serve as a pre-fabrication design methodology analysis tool in ways
such as class hierarchy construction, design specification comparison,
reachability analysis, and concurrent process management and analysis.
We then formally prove MOBnet to be a valid model for concurrent synthesis
and give experimental application examples to verify. Finally, solution
schemes for the design completion check and synthesis rollback problems are
formally validated by analyzing the dynamic behavior of MOBnet, and
experimentally illustrated through examples.