Currently, the SGM web page is being updated and reconstructed for the release of the new SGM v3.0.
Click HERE for SGM v2.0 web page
Brief History of SGM:
State-Graph Manipulators (SGM) was "born" in 1998 at the Academia Sinica, Taipei, Taiwan. Dr. Farn Wang was the principal investigator, who planned the design of this tool and Dr. Pao-Ann Hsiung was the developer of the tool in the C programming language. The basic idea of the tool originally was "user-friendliness", which means a user can use high level manipulators to generate state-graphs representing the parallel composition of two or more extended timed automata.Later, the tool "moved" to National Chung Cheng University, Chiayi, Taiwan in February 2001. Since then it has been maintained by Dr. Pao-Ann Hsiung along with a team of graduate students. SGM has gone through several upgradings and the reduction operators are no longer supported. However, the verification support for different modeling aspects has been enhanced considerably in the tool from 2001 to 2008. Thus during this period, SGM was used in the verification of several kinds of systems including:
- Systems-on-Chip (SoC),
- embedded software,
- hardware-software codesigns,
- real-time systems,
- prioritized timed systems,
- urgent timed systems, and
- safety-critical systems.
Following are the versions of the tool throughout history:
SGM v1.1 ~ v1.3 (released in 1999) had the following features:
- High-level manipulators such as TA composition (sequential merge)
- Reduction manipulators such as
- read-write reduction,
- symmetry-based reduction,
- clock shielding,
- variable shielding
- A Graphical User Interface (GUI)
SGM v1.4 ~ v1.9 developed from 2000 to 2006 were NOT released to the general public. However, it was used in several research work such as the following:
- Safecharts model checking (FORTE'2005, SEKE'2005, IEEE TC 2007),
- Priority handling (ATVA'2005, RTCSA'2005)
- Coverage estimation (ATVA'2004),
- VERTAF (IEEE TSE 2004, IEE CDT 2004, APLAS'2004, EUC'2004)
- FVP (IEEE SOCC'2003, ATVA'2003)
- AGR Assumption Generation (IEEE VLSI'2003, ICS'2002)
- Embedded Software Verification (JSA 2000)
- Scheduling System Verification (TACAS'1999)
SGM v2.0 (released in January 2007) has the following features:
- Verification Technologies
- Full CTL Model Checking,
- Accelerated Coverage Estimation,
- Dead State Checking,
- Modeling Support
- Transition Priority Handling,
- Transition Urgency Handling,
- Multiple Base-Reference Synchronizations,
- Tool Support
- Dot-based PDF generation.
- GUI is no longer supported
SGM v3.0 will be released within the second quarter of 2008. The new release will have the following enhancements:
- Verification Technologies
- Global composition of Extended Timed Automata
- Property-preserving abstraction
- Modeling Support
- Safecharts pre-processing
- Tool Support
- Task Migration modeling for Multiprocessor SoC
Current Project Investigator: Pao-Ann Hsiung
Team Members: (updated 2008/03)
Shang-Wei Lin, Yean-Ru Chen, Chun-Hsian Huang, Chao-Sheng Lin, Chih-Chieh Tsao, and Chih-Sheng Lin
Contact SGM Developers.
Maintained by:
Embedded Systems Lab,
Department of Computer Science and Information Engineering,
National Chung Cheng University,
168, University Road, Min-Hsiung, Chiayi, Taiwan, ROC-62102.