  This paper further introduces and formalizes a novel concept of
self-forensics for automotive vehicles, specified in the Forensic Lucid
language. We argue that self-forensics, with the forensics taken out of the
cybercrime domain, is applicable to "self-dissection" of intelligent vehicles
and hardware systems for automated incident and anomaly analysis and event
reconstruction by the software with or without the aid of the engineering teams
in a variety of forensic scenarios. We propose a formal design, requirements,
and specification of the self-forensic enabled units (similar to blackboxes) in
vehicles that will help investigation of incidents and also automated reasoning
and verification of theories along with the events reconstruction in a formal
model. We argue such an analysis is beneficial to improve the safety of the
passengers and their vehicles, like the airline industry does for planes.
