Content area
Decomposition of tightly-coupled, communication-intensive and highly interprocess-dependent concurrent programs is very difficult, however, it is also very much in need. Existing Object-Oriented Design method enables the idea of "Programming/Design by Contract", where an object's behavior is locally defined in terms of obligations and benefits (contracts). However, in a concurrent program, these local contracts are not enough to capture cooperation among different objects. In the thesis, I extend the Communication-Closed Layer concept for distributed systems to the shared memory model and give the formal definitions and the theorem on which program verification is based. From this concept, I combine Concurrent Object-Oriented programming techniques with shared memory based CCL to generate a totally different view for concurrent programs from the traditional view. The TEAMWORK assertions, which can also be called as inter-object contracts and the CHESSBOARD representation are introduced to provide global logical checkpoints and views to concurrent programs. The TEAMWORK assertions actually serve as the proof compositions and global contracts for the verification of concurrent programs and the CHESSBOARD gives a two-dimensional picture for a concurrent program that represents both consistency within each object and cooperation among objects. In the thesis I also introduce the watchdog object, which can assist in fault-tolerant software systems design and development.