TY - GEN
T1 - SC2SCFL
T2 - 7th International Workshop on Embedded Computer Systems: Architectures, Modeling, and Simulation, SAMOS 2007
AU - Man, Ka Lok
AU - Fedeli, Andrea
AU - Mercaldi, Michele
AU - Boubekeur, Menouer
AU - Schellekens, Michel
PY - 2007
Y1 - 2007
N2 - SystemCdouble-struck F signdouble-struck L sign is the formalisation of a reasonable subset of SystemC based on classical process algebras. During the last few years, SystemC double-struck F signdouble-struck L sign has been successfully used to give formal specifications of SystemC designs. For formal analysis purposes, so far, users have been required to transform manually their SystemC codes into corresponding SystemCdouble-struck F signdouble-struck L sign specifications. To verify some desired properties of SystemC double-struck F signdouble-struck L sign specifications using existing formal verification tools (e.g. NuSMV and SPIN), similarly, manual translations have been needed for turning SystemC double-struck F signdouble-struck L sign specifications into corresponding terms of the input language (e.g. SMV and PROMELA) of the selected formal verification tool. Since manual transformation and translations between SystemC codes, SystemC specifications, and various formalisms are quite laborious and therefore error-prone, these translations have to be made as much automatic as possible. The first step of the research in these directions is to automate the transformation from SystemC codes to SystemC specifications. In this paper, we present SC2SCFL (an automatic translation tool), which converts SystemC codes into corresponding SystemC double-struck F signdouble-struck L sign specifications.
AB - SystemCdouble-struck F signdouble-struck L sign is the formalisation of a reasonable subset of SystemC based on classical process algebras. During the last few years, SystemC double-struck F signdouble-struck L sign has been successfully used to give formal specifications of SystemC designs. For formal analysis purposes, so far, users have been required to transform manually their SystemC codes into corresponding SystemCdouble-struck F signdouble-struck L sign specifications. To verify some desired properties of SystemC double-struck F signdouble-struck L sign specifications using existing formal verification tools (e.g. NuSMV and SPIN), similarly, manual translations have been needed for turning SystemC double-struck F signdouble-struck L sign specifications into corresponding terms of the input language (e.g. SMV and PROMELA) of the selected formal verification tool. Since manual transformation and translations between SystemC codes, SystemC specifications, and various formalisms are quite laborious and therefore error-prone, these translations have to be made as much automatic as possible. The first step of the research in these directions is to automate the transformation from SystemC codes to SystemC specifications. In this paper, we present SC2SCFL (an automatic translation tool), which converts SystemC codes into corresponding SystemC double-struck F signdouble-struck L sign specifications.
UR - http://www.scopus.com/inward/record.url?scp=38148999346&partnerID=8YFLogxK
M3 - Conference Proceeding
AN - SCOPUS:38148999346
SN - 9783540736226
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 34
EP - 45
BT - Embedded Computer Systems
Y2 - 16 July 2007 through 19 July 2007
ER -