We have studied various models extensively in the last chapter. We transformed real-world problems into different domains through appropriate models to analyze certain characteristics. We have adopted different types of models for analyzing different characteristics for the same problem. However, it is a theoretical representation. We should now explore methods to verify that the model will behave as expected. The models we studied are represented as diagrams. Manual analysis of this diagrammatic representation is possible for a smaller size of the problems. We need a concrete form to represent the model so that all possible characteristics can be analyzed. Mostly, it is done by a specification language that captures these models in a concrete form. The language captures the functionality of the model in a machine-readable form. Once transformed to a language, it can be executed like any programming language and obtain results for different inputs. These are executable specification languages (ESLs). In modern design and development, ESLs play a major role as you can totally analyze the proposed model of the real-world problem, analyze using the ESL, and verify your design for intended functionality before you implement it. The ESL becomes the synthesis tool for design. Section 4.2 discusses important characteristics needed for the ESL for the design of embedded systems. The language has to capture the concurrent and hierarchical behaviors as processes, procedures, or state machines. Every behavior must have a mechanism to indicate that the activity is completed. ESL should support resource and activity synchronization primitives. The ESL should be executable and verify the behavior in a simulated environment. Once the results are verified, the ESL construct should be synthesizable to the desired implementation platform. SystemC is an executable specification language (ESL) at the system level. Sections 4.3, 4.4, 4.5, 4.6, 4.7, 4.8, 4.9, 4.10 and 4.11 discuss the details of SystemC with example implementations.