IEEE - Institute of Electrical and Electronics Engineers, Inc. - Bounded Model Checking of an MITL Fragment for Timed Automata

2013 13th International Conference on Application of Concurrency to System Design (ACSD 2013)

Author(s): Roland Kindermann ; Tommi Junttila ; Ilkka Niemela
Publisher: IEEE - Institute of Electrical and Electronics Engineers, Inc.
Publication Date: 1 July 2013
Conference Location: Barcelona, Spain
Conference Date: 8 July 2013
Page(s): 216 - 225
ISBN (Electronic): 978-0-7695-5035-0
ISSN (Electronic): 1550-4808
DOI: 10.1109/ACSD.2013.25
Regular:

Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver.... View More

Advertisement