Linköping University: Students Alumni Trade and Industry/Society Internal Search

Specification and Verification of Heterogeneous Electronic Systems (SAVE)

Project Description

The SAVE Project aims at development of a formal approach to specification, implementation and verification of heterogeneous electronic systems. The functionality of such system is captured using a formalism based on a sound mathematical theory and amenable to formal methods for verification and transformation.

The link to implementation in HW and SW is provided by a set of transformations which preserves the semantics of the specification, but also allows changes in the semantics while introducing new information into the specification. SAVE addresses the area of electronic systems design at higher abstraction levels, assuming that established techniques for detailed HW synthesis and SW compilation can be used at lower levels with a seamless transfer of design information.

The results will be assessed and verified in industrial environments by Saab Bofors Dynamics AB, Linköping. Saab will, together with other companies in the Saab group, provide pilot applications where the SAVE methods and tools can be applied.

SAVE is a joint research project of ESDlab at the Royal Institute of Technology (KTH), Stockholm, and ESLAB at Linköping University (LiU), Linköping. The two groups perform the research with financial support from NUTEK and in cooperation with Saab Bofors Dynamics. The project is coordinated by Peter Lind.


Project Members at LiU

  •  Zebo Peng, contact person
  •  Petru Eles
  •  Luis Alejandro Cortés


    • Project Members at KTH

  •  Axel Jantsch, contact person
  •  Ingo Sander


    • Publications

  •  L. A. Cortés, P. Eles, and Z. Peng, From Haskell to PRES+: Basic Translation Procedures, SAVE Project Report, Dept. of Computer and Information Science, Linköping University, Linköping, April 2001.  [PDF]  [PS]
  •  L. A. Cortés, P. Eles, and Z. Peng, Hierarchies for the Modeling and Verification of Embedded Systems, SAVE Project Report, Dept. of Computer and Information Science, Linköping University, Linköping, February 2001.  [PDF]  [PS]
  •  L. A. Cortés, P. Eles, and Z. Peng, Verification of Embedded Systems using a Petri Net based Representation, in Proc. Intl. Symposium on System Synthesis (ISSS), Madrid, Spain, Sept. 20-22, 2000.  [PDF]   [PS]
  •  L. A. Cortés, P. Eles, and Z. Peng, Definitions of Equivalence for Transformational Synthesis of Embedded Systems, in Proc. Intl. Conference on Engineering of Complex Computer Systems (ICECCS), Tokyo, Japan, Sept. 11-15, 2000.  [PDF]   [PS]
  •  W. Wu, I. Sander, and A. Jantsch, Transformational System Design Based on a Formal Computational Model and Skeletons, in Proc. Forum on Design Languages (FDL), Tübingen, Germany, Sept. 4-8, 2000.  [PDF]
  •  L. A. Cortés, P. Eles, and Z. Peng, Formal Coverification of Embedded Systems using Model Checking, in Proc. EUROMICRO Conference (Digital Systems Design), Maastricht, The Netherlands, Sept. 5-7, 2000.  [PDF]   [PS]
  •  W. Wu, Report on the Visit to the Department of Computer Science, Yale University, Dept. of Electronics, Royal Institute of Technology, Stockholm, August 2000.  [PDF]
  •  L. A. Cortés, P. Eles, and Z. Peng, Verification of Heterogeneous Electronic Systems using Model Checking, SAVE Project Report, Dept. of Computer and Information Science, Linköping University, Linköping, July 2000.  [PDF]  [PS]
  •  L. A. Cortés, P. Eles, and Z. Peng, Verification Methodology for Heterogeneous Hardware/Software Systems, SAVE Project Report, Dept. of Computer and Information Science, Linköping University, Linköping, January 2000.  [PDF]   [PS]
  •  W. Wu and A. Jantsch, A System Design Methodology Based on a Formal Computational Model, SAVE Project Report, Dept. of Electronics, Royal Institute of Technology, Stockholm, January 2000.  [PDF]
  •  L. A. Cortés, P. Eles, and Z. Peng, A Petri Net based Model for Heterogeneous Embedded Systems, in Proc. NORCHIP Conference, Oslo, Norway, Nov. 8-9, 1999, pp. 248-255.  [PDF]   [PS]
  •  W. Wu and A. Jantsch, A Survey of Design Transformation Techniques, SAVE Project Report, Dept. of Electronics, Royal Institute of Technology, Stockholm, July 1999.  [PDF]
  •  L. A. Cortés, P. Eles, and Z. Peng, A Survey on Hardware/Software Codesign Representation Models, SAVE Project Report, Dept. of Computer and Information Science, Linköping University, Linköping, June 1999.  [PDF]   [PS]


    • Related Publications

  •  I. Sander and A. Jantsch, System Synthesis Utilizing a Layered Functional Model.  [PDF]
  •  I. Sander and A. Jantsch, System Synthesis Based on a Formal Computational Model and Skeletons.  [PS]
  •  I. Sander and A. Jantsch, Formal Design Based on the Synchronous Approach.  [PS]


    • Miscellanea

  •  Agenda of SAVE Workshop at Linköping University, on December 2, 1999.  [PDF]
  •  Minutes of University/Industry Meeting held at SAAB Dynamics, Linköping, on October 14, 1999.  [PDF]
  •  SAVE Workshop at Linköping University, on December 6, 2000:
        - Task 1 [PDF]
        - Task 2 [PDF]
        - Task 2.1 [PDF]
        - Task 3 [PDF]