EE249, Fall 2006
Embedded System Design: Models, Validation and Synthesis
Embedded systems are electronics systems that sense physical quantities, elaborate the data and respond to the environment by sending commands to actuators. These computing systems appear everywhere in our everyday life. They occupy an important role in our homes, automobiles, and work place. The complexity of these systems is reaching levels that where not even conceivable a few years ago: There are more than 80 processors in a new generation car that control its function, and implement its entertainment and communication subsystems. Building automation system includes the heat, ventilation and air conditioning subsystem, elevator control, the fire alarm sub-system, and PBX. Several examples of serious design errors in automobiles and aerospace systems have caused recalls and expensive crashes. We need to develop methods that allow designing reliable and secure distributed systems quickly, inexpensively and with no errors. We need to bring closer together system theory and computer science. While computer science traditionally deals with abstractions where the physical world has been carefully and artfully hidden to facilitate the development of application software, system theory deals with the physical foundations of engineering where quantities such as time, power and size play a fundamental role in the models upon which this theory is based. The issue then is how to harmonize the physical view of systems with the abstractions that have been so useful in developing the CS intellectual agenda. We argue that a novel system theory is needed that at the same time is computational and physical. The basis of this theory cannot be but a set of novel abstractions that partially expose the physical reality to the higher levels and methods to manipulate the abstractions and link them in a coherent whole. This class is about teaching an approach to the new system science developed at the Berkeley Center for Hybrid and Embedded Software Systems (CHESS) and the Gigascale System Research Center (GSRC) where heterogeneity, concurrency, multiple levels of abstraction play an important role and where a set of correct-by-construction refinement techniques are introduced as a way of reducing substantially design time and errors.
A design methodology called Platform-Based Design (PBD) is an approach to the new system theory and is used as a way of organizing the course material. PBD calls for a successive refinement approach where functionality (what the system is supposed to do) of the design is captured at the highest level of abstraction possible and mapped to a set of predefined solutions (see Figure 1). Specifying a design includes identifying constraints such as latency, throughput, reliability, cost, and power consumption. The architecture is an interconnection of elements that are characterized by performance indexes coming from the abstraction of their implementation. The mapping process can be automated if both function and the architecture elements that form the platform are projected to a common semantic domain. Then, the mapping process can be cast as a constrained covering problem. The process repeats itself by interpreting the mapped design as a function at the next layer of abstraction and new architectural elements are introduced. This methodology has been used in a variety of industrial applications: from automotive design to communication systems and semiconductor chips.
Figure 1
The class is organized as in Table 1. In the first part, application examples are presented to motivate the need for a formal reasoning framework and Platform-Based Design is introduced. The second part is dedicated to the functional aspects of a design. Several models of computation are presented. The necessity of heterogeneous combination of models of computation leads to the introduction of two unifying framework: the Tagged Signal Model and Agent Algebras. The third part presents important aspects of architecture modeling including abstraction of performances. Architectures are usually resource-limited, therefore the concept of scheduling and real-time operating systems is explained in detail. The mapping problem is formally defined and synthesis techniques are explained for hardware, software and communication. The last part of the class presents a set of verification technique for embedded systems stressing further the need for formal models. The course is graded on assignments and on a final project. We expect a number of projects will be eventually published in Conference Proceedings. We will devote the afternoon sessions of the course to the presentation of important papers in the literature. The quality of class presentation on the papers is expected to be part of the grade. The student will gain experience on actual system designs through graded laboratories dealing with realistic design examples and case studies. During lab sessions, students will use and analyze various design academic and industrial tools. There are no pre-requisite for this course but some exposure to the basics of real-time embedded system and an inclination to formal reasoning is welcome. At the end of the course the student will have an understanding of the system-level design issues in the areas of specification, validation and HW/SW implementation.
Introduction
Design complexity, Example of embedded systems, traditional design flow, Platform-Based Design
Functional modeling, analysis and simulation
Mapping
Validation
Introduction to models of computation. Finite State Machines and Co-Design Finite State Machines, Kahn Process Networks, Data Flow, Petri Nets, Hybrid Systems. Unified frameworks: the Tagged Signal Model, Agent Algebra.
Definition of architecture, examples. Distributed architecture, coordination, communication. Real time operating systems, scheduling of computation and communication.
Architecture and performance abstraction
Definition of mapping and synthesis. Software synthesis, quasi static scheduling. Behavioral synthesis. Communication Synthesis and communication-based design.
Validation vs Simulation. Verification of hybrid system. Interface automata and assume guarantee reasoning.
Topic
Lectures
Table 1
