The MEMOCODE 2004 program includes three tutorials, each covering an important topic from research and practice. Each tutorial will be held on Tuesday, June 22, and will be one-half day in length. For more information about tutorials, please contact the presenter by e-mail. Please note that tutorial attendance does not increase the registration fee. Anyone registered for MEMOCODE 2004 may attend the tutorials.
Techniques for Component Composition in Hardware/Software Co-Design
Tuesday, June 22, 2004: 1:30 pm - 5:00 pm
Presenters: Rajesh Gupta, UC-San Diego; Jean-Pierre Talpin, IRISA/INRIA; Suhas Pai, Qualcomm; Sandeep Shukla, Virginia Tech
Email: shukla@vt.edu
As the design complexity of embedded hardware/software systems increases and verifiable design becomes an ever stronger requirement, IP component reuse methodologies are becoming more common in industry. On the one hand, reusable IP-based design provides designers with less flexibility in implementation, thereby constraining the design space; on the other hand, reuse of components reduces design time, and previously verified components reduce verification obligations if the composition of components is performed correctly.
Our recent research has focused on component composition and formal tools and techniques for proof of correctness of composition. Our methodology and techniques have been embedded in a component-composition framework named BALBOA. A multi-layer design environment has been constructed in which the topmost layer allows designers to compose existing IP components in a script-like language and users to build a simulation model of the composed system. Our formal approach ensures that the compositions are not only correct in terms of their interface data types but also with respect to behavioral properties. This leads to a type theory for interfaces of SystemC components, which is built on top of the theory of synchronous programming.
This tutorial will introduce the motivation for this formal approach to IP-composition, discuss certain standardization efforts such as VSIA efforts, and explain why standardization of interface specification may be insufficient. Tools and methodologies enabling correct component composition for co-design using reusable components will then be discussed, using examples from the BALBOA system and from our behavioral type system.
Intended Audience: The intended audience includes researchers from industry and academia interested in component composition frameworks, correct by construction co-design using re-usable components, and verification issues. No prior knowledge of SystemC, type theory, or synchronous programming is assumed. The tutorial will provide an overview of the area, familiarizing the audience with the basic problems, our solution strategy, and topics for future research.
Biographies:
Dr. Rajesh Gupta is the Qualcomm Chair Professor of Computer Science and Engineering at the University of California at San Diego. His expertise is in system level design languages, high level synthesis, networked embedded system design, and formal methods for system design. He is an IEEE Fellow and an NSF CAREER awardee.
Dr. Sandeep Shukla, an assistant professor of Electrical and Computer Engineering at Virginia Tech, is director of the FERMAT lab. His expertise is in formal methods applied to specification and verification of systems, embedded systems design methodologies, and tools and techniques for system design. Dr. Shukla is an NSF CAREER awardee.
Dr. Jean-Pierre Talpin is a research fellow at IRISA/INRIA in France and director of the Espresso project. His expertise is in synchronous programming; models, methods, and tools for GALS design; theories and principles of programming (type theory, etc.), embedded system design, and hardware/software co-design.
Dr. Suhas Pai, a Principal Engineer at Qualcomm, headed the systems verification and integration group and defined the post-silicon systems verification strategy for 1x/DO/UMTS/GPS standards. He designed the baseband and RF test stations which are currently used for all end-to-end systems testing at Qualcomm. He is currently focusing on pre-silicon verification strategy using transaction level bus cycle accurate verification models and their acceleration in hardware to detect system-level bugs early in design. Before joining Qualcomm in 1997, Suhas worked at Bell labs in DSP/communications area after earning his Ph.D. from the UT-Arlington in 1986.
T2
An Overview of the PVS Proof System
Tuesday, June 22, 2004: 9:00 am - 12:30 pm
Presenter: Myla Archer, Naval Research Laboratory
Email: archer@itd.nrl.navy.mil
In selecting a method for verifying a system, theorem proving is often avoided because it is perceived as requiring more user expertise and user guidance. However, although theorem provers can require user guidance during the reasoning phase, model checkers also require guidance prior to this phase because of the need to find a suitable abstraction. One advantage theorem provers have over model checkers is that they can be used to reason directly about models of systems with large or infinite state spaces without first abstracting the models. Among theorem provers, PVS, by being based on standard logic and incorporating decision procedures, provides a good combination of power and user-friendliness. Like other tactic-based theorem provers, PVS can be adapted to special domains through the definition of user tactics (called strategies in PVS). Users have applied PVS to verifying properties of both hardware and software, including microprocessors, real-time systems, and imperative programs.
This tutorial covers the basics of specification in PVS and describes commonly used standard PVS proof steps, with illustration of when they are appropriate. It also describes the basic features of the PVS system and user interaction with the system. Finally, the tutorial will provide an overview of how to adapt PVS to special domains.
Intended Audience: The intended audience includes researchers and practitioners from industry and academia interested in formal analysis of system and software specifications. The only prior knowledge assumed is basic understanding of standard logical notation involving quantification (i.e., "for all" and "there exists"). The tutorial will teach attendees how to represent systems and their properties in the language of PVS and how to interact with the PVS theorem prover. The tutorial will also provide a starting point for using the PVS theorem prover to prove properties of systems and, for the more ambitious, adapting PVS for use in special domains.
Biography:
Dr. Myla Archer is a research scientist in the Software Engineering Section of the Center for High Assurance Computer Systems at the Naval Research Laboratory in Washington, D.C. The chief designer of the TAME interface to PVS, Dr. Archer has published widely and presented numerous invited talks at universities on formal verification with PVS and TAME.
Rigorous Requirements for Safety-Critical Systems: Specification, Formal Analysis, and Validation with the SCR (Software Cost Reduction)
Tuesday, June 22, 2004: 1:30 pm - 5:00 pm
Presenter: Constance Heitmeyer, Naval Research Laboratory
Email: heitmeyer@itd.nrl.navy.mil
The Software Cost Reduction (SCR) method is a practical, industrial-strength method for constructing system and software specifications. The method has been shown to scale to large applications and to produce specifications that are both easy to understand and easy to change. Developed for use by engineers, the SCR method has been applied to a wide range of practical systems including avionics systems, telephone networks, submarine communications, space systems, and control systems for nuclear plants, such as the Darlington plant in Canada. Among the many organizations that have applied the SCR method to practical systems are Grumman, Lockheed, Ontario Hydro, Rockwell Aviation, and NASA.
Currently, more than 100 organizations in industry, government, and academia are experimenting with the SCR tools, a set of tools developed to support the SCR method. A number of companies in the U.S. are using SCR to develop software for systems they are developing. For example, several sites of Lockheed Martin currently use the SCR tools to support the development of software for autopilot logic, flight control, flight management, collision avoidance, and other avionics applications. Moreover, a number of universities in both the U.S. and Canada include material on the SCR method and tools in their software engineering courses. The tools include a specification editor, a consistency checker, a simulator, and an invariant generator. Various formal analysis tools, such as the Spin model checker and PVS theorem prover, may be used to evaluate properties, e.g., security and safety properties, of SCR specifications.
Intended Audience: The intended audience includes researchers and practitioners from industry and academia interested in system and software specification, requirements specification, formal analysis, specification-based testing, invariant generation, and specification-based simulation. No prior knowledge of formal specification and verification is assumed. The tutorial is intended to provide an overview of the area, familiarizing the audience with the basic problems, our solution strategy, and further research topics.
Biography:
Constance Heitmeyer heads the Software Engineering Section of the Center for High Assurance Computer Systems at the Naval Research Laboratory in Washington, D.C. The chief designer of the SCR tools, she has presented many short courses on the SCR tools and methods. She has published widely presented many invited talks at universities and conferences on tools supporting formal specification and analysis.