For a system-level design which may be composed of multiple processing elements runningin parallel, various kinds of unwanted consequences may happen if the systemis constructed carelessly. For example, deadlock may happen if improper executionorder and communication between processing elements is used in the system. Anotherproblem which may be caused by the concurrent execution is race condition, asshared variables in the system-level model could be accessed by multiple concurrentthreads in parallel. Those unwanted behaviors definitely have negative influence onthe functionality of the system. Furthermore, the functionality is not the only concernin system design as timing constraints are critical as well. If the system cannotfinish the job within timing constraints, it is still considered an unwanted design. Toaddress these issues, we propose two formal analysis approaches in this dissertationto analyze three types of properties we discussed above, which are1). liveness,2). satisfiability of timing constraint, and3). May-Happen-in-Parallel access.These two approaches are based on Satisfiability Modulo Theories (SMT) and UPPAALautomaton model respectively. We run these two approaches on our in-housesystem models, including a JPEG encoder, MP3 decoder, AMBA AHB and CANbus protocol models. The experimental results show our approaches are capable ofanalyzing those properties meeting our expectation within reasonable analysis time.