Name:  Che-Wei Chang

Date/Time:  Wednesday, January 28,2015, 9:00am

Location:  EH 3404

Committee Chair: Rainer Doemer

Committee Member: Daniel Gajski

Committee Member: Pai Chou


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 this issue, 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.