CafeOBJ is an advanced algebraic specification language that can be used for writing formal specifications of various software systems and verifying properties of them. It implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and conduct proofs by executing the proof scores. Despite its usefulness, up to present, the application of CafeOBJ specifications to software development is very limited. Therefore, we would like to propose methods or techniques to make an observation transition system (OTS) in CafeOBJ more usable in both software development and testing. We focus on concurrent systems and how to write concurrent programs in Java based on OTSs. Java has been chosen as the implementation language because concurrency is strongly supported in this language and there are also many powerful testing frameworks in Java that can help us further verify properties of the programs.