949-824-9127
- This event has passed.
Formal Analysis of Electronic System Level Models using Satisfiability Modulo Theories and Automata Checking
February 2, 2015 @ 3:00 pm - 4:00 pm PST
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
Abstract:
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.