Analysis of Sequential Systems
The design of increasingly complex electronic systems makes it more and more difficult to verify their correct behavior. At the same time it becomes more and more important that the systems work correctly, as nowadays human lives seriously depend on them, e.g., in traffic or in medicine.
KeywordsImage Computation Finite State Machine Transition Relation Switching Function Sequential System
Unable to display preview. Download preview PDF.
- The analysis of sequential systems using symbolic OBDD techniques was established primarily by Coudert, Berthet, and Madre [CBM89] as well as by Burch, Clarke, Long, McMillan, and Dill [BCL+94]. The constrain operator and the restrict operator also go back to Coudert, Berthet, and Madre. A survey article on implicit set representations can be found in [CM95].Google Scholar
- The partitioning technique for image computation based on a transition relation is due to [BCL+94]. The presented heuristic for the arrangement of the partitions was proposed by Geist and Beer [GB94].Google Scholar
- Our presentation of reachability analysis follows the one in [Som96a].Google Scholar