View source for Publications:Formal analysis of systemc designs in process algebra

<div style='display: none'>
== Do not edit this section ==
</div>
{{PublicationSetupTemplate|Author=Hossein Hojjat, Mohammad Reza Mousavi, Marjan Sirjani
|PID=583421
|Name=Hojjat, Hossein (Ecole Polytechnique F́ed́erale de Lausanne, Station 14, CH-1015 Lausanne, Switzerland);Mousavi, Mohammad Reza [mohmou] (Eindhoven University of Technology, P.O. Box 513, NL-5600MB, Eindhoven, Netherlands);Sirjani, Marjan (Reykjavik University, Reykjavik, Iceland)
|Title=Formal analysis of systemc designs in process algebra
|PublicationType=Journal Paper
|ContentType=Refereegranskat
|Language=eng
|Journal=Fundamenta Informaticae
|JournalISSN=0169-2968
|Status=published
|Volume=107
|Issue=
|HostPublication=
|Conference=
|StartPage=19
|EndPage=42
|Year=2011
|Edition=
|Pages=
|City=Amsterdam
|Publisher=IOS Press
|Series=
|SeriesISSN=
|ISBN=
|Urls=
|ISRN=
|DOI=http://dx.doi.org/10.3233/FI-2011-391
|ISI=000294729300002
|PMID=
|ScopusId=2-s2.0-80052639615
|NBN=urn:nbn:se:hh:diva-20335
|LocalId=
|ArchiveNumber=
|Keywords=Formal Verification;mCRL2;Process Algebra;SystemC
|Categories=Data- och informationsvetenskap (102)
|ResearchSubjects=
|Projects=
|Notes=
|Abstract=<p>SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.</p>
|Opponents=
|Supervisors=
|Examiners=
|Patent=
|ThesisLevel=
|Credits=
|Programme=
|Subject=
|Uppsok=
|DefencePlace=
|DefenceLanguage=
|DefenceDate=
|CreatedDate=2013-01-08
|PublicationDate=2013-01-08
|LastUpdated=2013-01-17
|diva=http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:583421}}
<div style='display: none'>

== Keep all hand-made modifications below ==
</div>{{PublicationDisplayTemplate}}