|
Formal Verification of Embedded Systems based on CFSM Networks
Abstract:
Both timing and functional properties are essential to
characterize the correct behavior of an embedded system.
Verification is in general performed either by simulation, or
by bread-boarding. Given the safety requirements of such systems,
a formal proof that the properties are indeed satisfied is highly
desirable. In this paper, we present a formal verification
methodology for embedded systems. The formal model
for the behavior of the system used in POLIS is a
network of Codesign Finite State Machines. This model is
translated into automata, and verified using
automata-theoretic techniques.
An industrial embedded system is verified using the methodology.
We demonstrate that abstractions and separation of
timing and functionality is crucial for
the successful use of formal verification for
this example. We also show that in POLIS abstractions
and separation of timing and functionality can be done by simple syntactic
modification of the representation of the system.
UCB Design Technology Warehouse Homepage
|
