UC Irvine

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.