| For a system-level design which may be composed of multiple processing elements running in parallel, various kinds of unwanted consequences may happen if the system is constructed carelessly. For example, deadlock may happen if improper execution order and communication between processing elements is used in the system. Another problem which may be caused by the concurrent execution is race condition, as shared variables in the system-level model could be accessed by multiple concurrent threads in parallel. Those unwanted behaviors definitely have negative influence on the functionality of the system. Furthermore, the functionality is not the only concern in system design as timing constraints are critical as well. If the system cannot finish the job within timing constraints, it is still considered an unwanted design. To address these issues, we propose two formal analysis approaches in this dissertation to analyze three types of properties we discussed above, which are 1). liveness, 2). satisfiability of timing constraint, and 3). May-Happen-in-Parallel access. These two approaches are based on Satisfiability Modulo Theories (SMT) and UPPAAL automaton model respectively. We run these two approaches on our in-house system models, including a JPEG encoder, MP3 decoder, AMBA AHB and CAN bus protocol models. The experimental results show our approaches are capable of analyzing those properties meeting our expectation within reasonable analysis time. |
