We present a novel component-based approach to hardware/software co-verification of embedded systems using model checking. Embedded systems are pervasive and often mission-critical, therefore, they must be highly trustworthy. Trustworthy embedded systems require extensive verification. The close interactions between hardware and software of embedded systems demand co-verification. Due to their diverse applications and often strict physical constraints, embedded systems are increasingly component-based and include only the necessary components for their missions. In our approach, a component model for embedded systems which unifies the concepts of hardware IPs (i.e., hardware components) and software components is defined. Hardware and software components are verified as they are developed bottom-up. Whole systems are co-verified as they are developed top-down. Interactions of bottom-up and top-down verification are exploited to reduce verification complexity by facilitating compositional reasoning and verification reuse. Case studies on a suite of networked sensors have shown that our approach facilitates major verification reuse and leads to order-of-magnitude reduction on verification complexity.

In this paper, terminal sliding mode control design is considered. A control method, different from many existing terminal sliding model control design methods, is proposed based on a new switching law and continuous finite-time control ideas. Then terminal sliding mode control laws are constructed for some classes of nonlinear systems.