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.

This paper tackles linear symmetries of control systems. Precisely, the symmetry of affine nonlinear systems under the action of a sub-group of general linear group GL?n;R?: First of all, the structure of state space (briefly, ss) symmetry group and its Lie algebra for a given system is investigated. Secondly, the structure of systems, which are ss-symmetric under rotations, is revealed. Thirdly, a complete classification of ss-symmetric planar systems is presented. It is shown that for planar systems there are only four classes of systems which are ss-symmetric with respect to four linear groups. Fourthly, a set of algebraic equations are presented, whose solutions provide the Lie algebra of the largest connected ss-symmetry group. Finally, some controllability properties of systems with ss-symmetry group are studied. As an auxiliary tool for computation, the concept and some properties of semi-tensor product of matrices are included. Copyright