research-article

Sysfier: Actor-based formal verification of SystemC

Authors:

Niloofar Razavi,

Razieh Behjati,

Hamideh Sabouri,

Ehsan Khamespanah,

Marjan SirjaniAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 10, Issue 2

Article No.: 19, Pages 1 - 35

https://doi.org/10.1145/1880050.1880055

Published: 07 January 2011 Publication History

Abstract

SystemC is a system-level modeling language that can be used effectively for hardware/software co-design. Since a major goal of SystemC is to enable verification at higher levels of abstraction, the tendency is now directing to introducing formal verification approaches for SystemC. In this article, we propose an approach for formal verification of SystemC designs, and provide the semantics of SystemC using Labeled Transition Systems (LTS) for this purpose. An actor-based language, Rebeca, is used as an intermediate language. SystemC designs are mapped to Rebeca models and then Rebeca verification toolset is used to verify LTL and CTL properties. To tackle the state-space explosion, Rebeca model checkers offer some reduction policies that make them appropriate for SystemC verification. The approach also benefits from the modular verification and program slicing techniques applied on Rebeca models. To show the applicability of our approach, we verified a single-cycle MIPS design and two hardware/software co-designs. The results show that our approach can effectively be used both in hardware and hardware/software co-verification.

References

[1]

Behjati, R., Sabouri, H., Razavi, N., and Sirjani, M. 2008. An effective approach for model checking SystemC designs. In Proceedings of the 8th International Conference on Application of Concurrency to System Design. IEEE, Los Alamitos, CA.

[2]

Black, D. and Donovan, J. 2004. SystemC: From the Ground Up. Springer Science+Business Media, New York.

Digital Library

[3]

Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in C. In Proceedings of the 25th International Conference on Software Engineering. IEEE, Los Alamitos, CA, 385--395.

Digital Library

[4]

Cortes, L. A., Eles, P., and Peng, Z. 2000. Verification of embedded systems using a petri net based representation. In Proceedings 13th International Symposium on System Synthesis. IEEE, Los Alamitos, CA, 149--155.

Digital Library

[5]

Drechsler, R. and Grosse, D. 2002. Reachability analysis for formal verification of SystemC. In Proceedings of the Euromicro Symposium on Digital Systems Design. IEEE, Los Alamitos, CA, 337--340.

Digital Library

[6]

Emerson, E. 1990. Temporal and modal logic. In J. van Leeuwen, ed., Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics. MIT Press, Cambridge, MA, 995--1072.

Digital Library

[7]

FZI -- Microelectronic System Design. 2006. KaSCPar. www.fzi.de/downloads/sim/archives/kascpar-documentation.pdf.

[8]

Gawanmeh, A., Habibi, A., and Tahar, S. 2004. Enabling SystemC verification using abstract state machines. In Proceedings of Forum on Specification and Design Languages, 19--22.

[9]

Ghenassia, F., ed. 2005. Transaction-Level Modeling with SystemC, TLM Concepts and Applications for Embedded Systems. Springer, Berlin.

Digital Library

[10]

Grosse, D. and Drechsler, R. 2003. Formal verification of LTL formulas for SystemC designs. In Proceedings of the International Symposium on Circuits and Systems. IEEE, Los Alamitos, CA, 245--248.

[11]

Habibi, A. and Tahar, S. 2005. On the transformation of SystemC to ASML using abstract interpretation. Electr. Notes Theor. Comput. Sci. 131, 39--49.

Digital Library

[12]

Habibi, A. and Tahar, S. 2006. Design and verification of SystemC transaction-level models. IEEE Trans. VLSI Syst. 14, 1, 57--68.

Digital Library

[13]

Hojjat, H., Mousavi, M. R., and Sirjani, M. 2008. Process algebraic verification of SystemC codes. In Proceed of the 8th International Conference on Application of Concurrency to System Design. IEEE, Los Alamitos, CA.

[14]

Jaghoori, M., Movaghar, A., and Sirjani, M. 2006. Modere: The model-checking engine of Rebeca. In Proceedings of the Symposium on Applied Computing—Software Verification Track. ACM, New York, 1810--1815.

Digital Library

[15]

Jaghoori, M., Sirjani, M., Mousavi, M., and Movaghar, A. 2005. Efficient symmetry reduction for an actor-based model. In Proceedings of the 2nd International Conference on Distributed Computing and Internet Technology. Springer-Verlag, Berlin, 494--507.

Digital Library

[16]

Jaghoori, M., Sirjani, M., Mousavi, M., and Movaghar, A. 2007. Symmetry and partial order reduction techniques in model checking Rebeca. Tech. rep. SEN-R0704.

[17]

Kroening, D. and Sharygina, N. 2005. Formal verification of SystemC by automatic hardware/software partitioning. In Proceedings of Formal Methods and Models for Co-Design. IEEE, Los Alamitos, CA, 101--110.

Digital Library

[18]

Kundu, S., Ganai, M., and Gupta, R. 2008. Partial order reduction for scalable testing of systemC TLM designs. In Proceedings of the 45th Annual Design Automation Conference. ACM, New York, 936--941.

Digital Library

[19]

Moy, M., Maraninchi, F., and Maillet-Contoz, L. 2006. LusSy: An open tool for the analysis of Systems-on-a-Chip at the transaction level. Des. Autom. Embedded Syst. 10, 2-3, 73--104.

[20]

Mueller, W., Ruf, J., Hoffmann, D., Gerlach, J., Kropf, T., and Rosenstiehl, W. 2001. The simulation semantics of systemC. In Proceedings of the Design, Automation, and Test in Europe. IEEE, Los Alamitos, CA, 64--70.

Digital Library

[21]

Muller, W., Ruf, J., and Rosenstiel, W. 2003. SystemC—Methodologies and Applications. Kluwer Academic Publishers, Dordrecht, The Netherlands, 97--126.

Digital Library

[22]

Open SystemC Initiative. 2005. IEEE 1666: SystemC Language Reference Manual. Open SystemC Initiative. http://standards.ieee.org/getieee/1666/download/1666-2005.pdf.

[23]

Patel, H. D. and Shukla, S. K. 2007. Model-driven validation of systemC designs. In Proceedings of the 44th Annual Conference on Design Automation. ACM, New York, 29--34.

Digital Library

[24]

Pnueli, A. 1979. The temporal semantics of concurrent programs. In Proceedings of the International Symposium on Semantics of Concurrent Computation. Springer-Verlag, Berlin, 1--20.

Digital Library

[25]

Razavi, N. and Sirjani, M. 2006. Using Reo for formal specification and verification of system designs. In Proceedings of Formal Methods and Models for Codesign. IEEE, Los Alamitos, CA, 113--122.

[26]

Razavi, N. and Sirjani, M. 2007. Compositional semantics of system-level designs written in SystemC. In Proceedings of the International Symposium on Fundamentals of Software Engineering. Springer-Verlag, Berlin, 113--128.

Digital Library

[27]

Sabouri, H. and Sirjani, M. 2008. Slicing-based reductions for Rebeca. In Proceedings of the 5th International Workshop on Formal Aspect of Component Software. Elsevier, Cambridge, MA.

[28]

Salem, A. 2003. Formal semantics of synchronous systemc. In Proceedings of the Conference on Design, Automation and Test in Europe. IEEE, Los Alamitos, CA, 10376.

Digital Library

[29]

Savoiu, N., Shukla, S., and Gupta, R. 2005. Improving systemC simulation through petri net reductions. In Proceedings of the 2nd International Conference on Formal Methods and Models for Co-Design. IEEE, Los Alamitos, CA, 131--140.

Digital Library

[30]

Sirjani, M., de Boer, F. S., and Movaghar, A. 2005. Modular verification of a component-based actor language. J. Universal Comput. Sci. 11, 10, 1695--1717.

[31]

Sirjani, M., Movaghar, A., Shali, A., and de Boer, F. 2004. Modeling and verification of reactive systems using Rebeca. Fundamenta Informaticae 63, 4, 385--410.

Digital Library

[32]

Sirjani, M., Movaghar, A., Shali, A., and de Boer, F. S. 2005. Model checking, automated abstraction, and compositional verification of Rebeca models. J. Universal Comput. Sci. 11, 6, 1054--1082.

[33]

Somenzi, F. and Bloem, R. 2000. Efficient büchi automata from ltl formulae. In Proceedings of the 12th International Conference on Computer-Aided Verification (CAV '00). Springer-Verlag, Berlin, 248--263.

Digital Library

[34]

SyMon: SystemC Model-checking engine technical report. http://khorshid.ece.ut.ac.ir/_rebeca/afra/SyMon.pdf.

[35]

Traulsen, C., Cornet, J., Moy, M., and Maraninchi, F. 2007. A SystemC/TLM semantics in Promela and its possible applications. In Proceedings of the 14th Workshop on Model Checking Software SPIN. Springer-Verlag, Berlin.

Digital Library

[36]

Vardi, M. 2007. Formal techniques for SystemC verification; position paper. In Proceedings of the 44th Design Automation Conference. ACM, New York, 188--192.

Digital Library

[37]

Weiser, M. 1981. Program slicing. In Proceedings of the 5th International Conference on Software Engineering. IEEE, Los Alamitos, CA, 439--449.

Digital Library

Cited By

Khamespanah ESirjani MKhosravi R(2023)Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family ModelsFundamentals of Software Engineering10.1007/978-3-031-42441-0_6(72-87)Online publication date: 30-Aug-2023
https://doi.org/10.1007/978-3-031-42441-0_6
Karami FOwe ORamezanifarkhani T(2019)An evaluation of interaction paradigms for active objectsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2018.11.008103(154-183)Online publication date: Feb-2019
https://doi.org/10.1016/j.jlamp.2018.11.008
Sirjani M(2018)Power is Overrated, Go for Friendliness! Expressiveness, Faithfulness, and Usability in Modeling: The Actor ExperiencePrinciples of Modeling10.1007/978-3-319-95246-8_25(423-448)Online publication date: 20-Jul-2018
https://doi.org/10.1007/978-3-319-95246-8_25
Show More Cited By

Recommendations

Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
HW/SW co-verification of embedded systems using bounded model checking
GLSVLSI '06: Proceedings of the 16th ACM Great Lakes symposium on VLSI

Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 10, Issue 2

December 2010

457 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/1880050

Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 07 January 2011

Accepted: 01 June 2009

Revised: 01 March 2009

Received: 01 September 2008

Published in TECS Volume 10, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
491
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)1

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Khamespanah ESirjani MKhosravi R(2023)Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family ModelsFundamentals of Software Engineering10.1007/978-3-031-42441-0_6(72-87)Online publication date: 30-Aug-2023
https://doi.org/10.1007/978-3-031-42441-0_6
Karami FOwe ORamezanifarkhani T(2019)An evaluation of interaction paradigms for active objectsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2018.11.008103(154-183)Online publication date: Feb-2019
https://doi.org/10.1016/j.jlamp.2018.11.008
Sirjani M(2018)Power is Overrated, Go for Friendliness! Expressiveness, Faithfulness, and Usability in Modeling: The Actor ExperiencePrinciples of Modeling10.1007/978-3-319-95246-8_25(423-448)Online publication date: 20-Jul-2018
https://doi.org/10.1007/978-3-319-95246-8_25
Boer FSerbanescu VHähnle RHenrio LRochas JDin CJohnsen ESirjani MKhamespanah EFernandez-Reyes KYang A(2017)A Survey of Active Object LanguagesACM Computing Surveys10.1145/312284850:5(1-39)Online publication date: 5-Oct-2017
https://dl.acm.org/doi/10.1145/3122848
Herber PPockrandt MGlesner S(2015)STATE -- A SystemC to Timed Automata Transformation EngineProceedings of the 2015 IEEE 17th International Conference on High Performance Computing and Communications, 2015 IEEE 7th International Symposium on Cyberspace Safety and Security, and 2015 IEEE 12th International Conf on Embedded Software and Systems10.1109/HPCC-CSS-ICESS.2015.188(1074-1077)Online publication date: 24-Aug-2015
https://dl.acm.org/doi/10.1109/HPCC-CSS-ICESS.2015.188
Khamespanah ESirjani MSabahi Kaviani ZKhosravi RIzadi M(2015)Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition systemScience of Computer Programming10.1016/j.scico.2014.07.00598:P2(184-204)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.07.005
Herber PGlesner S(2015)Verification of Embedded Real-time SystemsFormal Modeling and Verification of Cyber-Physical Systems10.1007/978-3-658-09994-7_1(1-25)Online publication date: 6-Jun-2015
https://doi.org/10.1007/978-3-658-09994-7_1
Varshosaz MKhosravi R(2012)Modeling and verification of probabilistic actor systems using prebecaProceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineering10.1007/978-3-642-34281-3_12(135-150)Online publication date: 12-Nov-2012
https://dl.acm.org/doi/10.1007/978-3-642-34281-3_12
Hojjat HMousavi MSirjani M(2011)Formal Analysis of SystemC Designs in Process AlgebraFundamenta Informaticae10.5555/2351788.2351790107:1(19-42)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.5555/2351788.2351790
Sirjani MJaghoori M(2011)Ten years of analyzing actorsFormal modeling10.5555/2074591.2074596(20-56)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.5555/2074591.2074596
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents