\contentsline {chapter}{\numberline {1}Pendahuluan}{5}
\contentsline {section}{\numberline {1.1}Latar Belakang}{6}
\contentsline {section}{\numberline {1.2}Kecelakaan akibat software atau hardware}{7}
\contentsline {section}{\numberline {1.3}Proses Desain}{9}
\contentsline {chapter}{\numberline {2}Formal Specification}{13}
\contentsline {section}{\numberline {2.1}Notasi formal}{14}
\contentsline {section}{\numberline {2.2}CSP}{15}
\contentsline {subsection}{\numberline {2.2.1}Input dan Output}{15}
\contentsline {section}{\numberline {2.3}PROMELA}{17}
\contentsline {section}{\numberline {2.4}Higher Order Logic}{17}
\contentsline {section}{\numberline {2.5}Petri nets}{17}
\contentsline {section}{\numberline {2.6}Synchronized Transition}{17}
\contentsline {section}{\numberline {2.7}Lain-lain: CCS, Estelle, Lotos, VDM, Z}{17}
\contentsline {chapter}{\numberline {3}Formal Synthesis}{19}
\contentsline {chapter}{\numberline {4}Formal Verification}{21}
\contentsline {section}{\numberline {4.1}Equivalence Checking}{21}
\contentsline {section}{\numberline {4.2}Model Checking}{22}
\contentsline {section}{\numberline {4.3}Theorem Proving}{22}
\contentsline {section}{\numberline {4.4}Binary Decision Diagram (BDD)}{23}
\contentsline {section}{\numberline {4.5}Verification Tools}{23}
\contentsline {chapter}{\numberline {5}Studi Kasus}{25}