Research Highlights | Technical Reports | CVS Staff | Access | Inquiry | Home | AIST | Japanese

Workshop on Simulation Based Development of Certified Embedded Systems
Last Updated : 2009/09/29

This workshop is organised jointly by CVS/AIST and FORMES INRIA/Tsinghua University. It is a closed, by invitation only workshop.
Embedded systems have become ubiquitous in our everyday life, ranging from simple sensors to complex systems such as mobile phones, network outers, airplane, aerospace and defense apparatus. As embedded devices include increasingly sophisticated hardware and software, the development of combined hardware and software has become a key to economic success.
There are often stringent time to market and quality requirements for embedded systems manufacturers. Safety and security requirements are satisfied by using strong validation tools and some form of formal methods, accompanied with certification processes such as IEC 61508, DO 178 or Common Criteria certification. These requirements for quality of service, safety and security imply to have formally proved the required properties of the system before it is deployed.
The above context requires addressing the challenges of embedded systems design with new approaches, combining fast hardware simulation techniques with advanced formal methods, in order to obtain a convincing and valid argument about qualitative and quantitative properties of the final system.
The goal of the present workshop is to discuss these issues in an informal, relaxed setting by gathering people involved in relevant projects all around the world.
Each participating site is expected to be represented by a limited number of researchers; talks may be either about recent research work or about the position for further work. After due refereeing, publication of the relevant contributions is planned in the International Journal for Software and Informatics.

Date: (Mon) 5 Oct. - (Wed) 7 Oct.

Contribution: This is an informal workshop and presentation of recent research work or about the position for further work is welcome. Each contributor should have a 3 pages or more abstract. We shall prepare electronic proceedings at this website.

Place: Awaji Yume-butai International Conference Center,Awaji island, Hyogo, Japan (AWAJI NAVI)
At the early stage of preparation, Senri (Osaka) was planned as the workshop site, but to gain better environment for discussions and communication at an isolated place, we have decided to hold the workshop at Awaji.

There is a limousine bus service from Kansai International airport (KIX) to Awaji Yumebutai International Conference Center: see

Accommodation:At the participation notice, participants will be asked whether he/she needs booking of The Westin hotel, next to the conference center, which is available at a special rate.


Mon. 5 October
  13:00-13:30 Greetings, and orientations (Y. Kinoshita)
  13:30-15:00 Self introductions (Every participant)
  15:00-15:30 Tea Break
  15:30-17:00 Tutorials
1) Vania Joloboff (FORMES INRIA-Tsinghua)
      Embedded Systems Simulation Concepts and Techniques Overview
2) Yoshiki Kinoshita (CVS/AIST)
      Basic Concepts of Formal Methods: Overview
  18:30- Dinner

Tue. 6 October
    9:00-10:30 Contributed Talks
3) Florence Maraninchi (VERIMAG/INPG)
     Runtime verification and simulations of systems-on-a-chip
4) Nguyen Van Tang (CVS/AIST)
     Formal Verification of A Train Fare Calculation System by The Agda Proof Assistant
  10:30-11:00 Tea Break
  11:00-12:30 Introductions of institutes
Florence Maraninchi (VERIMAG/INPG)
Junya Nakata (NICT-JAIST)
Jean-Pierre Jouannaud (FORMES INRIA-Tsinghua)
Hitoshi Ohsaki (CVS/AIST)
and others
  12:30-14:00 Lunch
  14:00-15:30 Contributed Talks
5) Jean-Pierre Jouannaud and Frederic Blanqui (FORMES INRIA-Tsinghua)
     Certification of Embedded Systems
6) Vania Joloboff (FORMES INRIA-Tsinghua)
     The SimSoc simulator a
  15:30-16:00 Tea Break
  16:00-17:30 Contributed Talks
7) Jyunya Nakata (NICT-JAIST)
     A Homenetwork Workbench for both real and cyber entities
8) Luca Ferro (TIMA)
     Using Temporal Assertions for Evaluating the Correctness and Safety of Embedded Systems
  18:30- Dinner

Wed. 7 October
    9:00-10:30 Contributed Talks
9) Shunsuke Yatabe (CVS/AIST)
     Specification check tool S3 and its mathematical model
10) Claude Helmstetter (INRIA-France) a SystemC/TLM Front-end for the CADP Verification Toolbox
  10:30-11:00 Tea Break
  11:00-12:00 Open discussion on testing of embedded systems
(lead by J.-P. Jouannaud)
  12:00-13:30 Lunch
  13:30-15:00 Contributed Talks
11) Makoto Takeyama (CVS/AIST)
      Formalization of System LSI Specification and Automatic Generation of Verification Items
12) Yoshiki Kinoshita (CVS/AIST)
      Cluster in the Loop Simulation Framework based on Formal Model-based Testing for Embedded Network Systems
  15:00-15:10 Closing (J.-P. Jouannaud)

    Participation Notice : 18 Sep.
    Title and abstract of talks: 18 Sep.


    Yoshiki Kinoshita (CVS/AIST)
    Jean-Pierre Jouannaud (FORMES INRIA-Tsinghua)
    Vania Joloboff, Tsinghua (FORMES INRIA-Tsinghua)

AIST > AIST organization > AIST laboratories > CVS
Copyrights (C) 2005-2009 AIST Research Center for Verification and Semantics, All Rights Reserved.