HARDWARE-SOFTWARE CODESIGN OF EMBEDDED SYSTEMS

Designers generally implement embedded controllers for reactive real-t ime applications as mixed software-hardware systems. In our formal met hodology for specifying, modeling, automatically synthesizing, and ver ifying such systems, design takes place within a unified framework tha t prejudices neither hardware nor software implementation. After inter active partitioning, this approach automatically synthesizes the entir e design, including hardware-software interfaces. Maintaining a finite -state machine model throughout, it preserves the formal properties of the design. It also allows verification of both specification and imp lementation, as well as the use of specification refinement through fo rmal verification.