Abstract
The verification of the embedded systems would play an important role in its scenario of manufacturing. The SystemC language of the embedded systems material description became the basic language of most of industrial productions companies. This allows several research works to focus on the verification methods of the SystemC designs. The formal verification that bases on mathematical proofs is a powerful method to describe the existence or the absence of the designs errors. It is a combination of two parallel and in collaboration operations; the first one is the specification of the generic and specific properties of the system under a formal language, the second is the description of its behavior under state-transition representations. In spite of its mathematical power, it knows limitations in terms of the systems length. It enters in the type of the state explosion problems that effect on the speed of the check. In this paper, we represent a new approach of verifying the SystemC designs using SPIN Model Checker, based on the deduction method that extract the executions of equivalence “scenarios of equivalence” through which we can deduct the satisfaction or the non-satisfaction of the systems specification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Chen, X., Watanabe, Y.: Formal verification for embedded system designs. Des. Autom. Embed. Syst. 8, 139–153 (2003)
Grotker, T., Lio, S., Martin, G., Swan, S.: System Design with SystemC\(^{\rm TM}\). Kluwer Academic Publishers, Hingham (2002)
Maillet-Contoz, L., Ghenassia, F.: Transaction level modeling. In: Ghenassia, F. (ed.) Transaction Level Modeling with SystemC. Springer, Boston (2005). https://doi.org/10.1007/0-387-26233-4_2
McMillan, K.L.: Symbolic Model Checking. Carnegie Mellon University, Pittsburgh (1993)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal 4.0. (2006)
Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. -Spec. Issue Formal Methods Softw. Pract. 23(5), 279–295 (1997)
Sharma, A.: End to End Verification and Validation with SPIN (2013)
Moy, M., Maraninchi, F., Maillet-Contoz, L.: PINAPA: an extraction tool for SystemC descriptions of systems-on-a-chip. In: EMSOFT05. ACM (2005)
Moy, M., Maraninchi, F., Maillet-Contoz, L.: LusSy: an open tool for the analysis of systems-on-a-chip at the transaction level. Des. Autom. Embed. Syst. 10, 73–104 (2006). Springer Science+Business Media, LLC
Marquet, K., Moy, M.: PinaVM: a SystemC Front-End Based on an Executable Intermediate Representation (2010)
Marquet, K., Jeannet, B., Moy, M.: Efficient encoding of SystemC/TLM in Promela. In: The International MultiConference of Engineers and Computer Scientists, vol II (2011)
Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: A SystemC/TLM semantics in Promela and its possible applications. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 204–222. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73370-6_14
Herber, P., Fellmuth, J., Glesner, S.: Model checking SystemC designs using timed automata. In: International Conference on Hardware/Software Codesign and System Synthesis, pp. 131–136 (2008)
Garavel, H., Helmstetter, C., Ponsini, O., Serwe, W.: Verification of an industrial SystemC/TLM model using LOTOS ans CADP. In: 7th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE2009, Cambridge, MA, USA (2009)
Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., Moy, M.: Automatic generation of schedulings for improving the test coverage of systems-on-a-chip. In: FMCAD, pp. 171–178 (2006)
Pelanek, R.: Reduction and abstraction techniques for model checking. Masaryk University Faculty of Informatics (2006)
Chupilko, M., Kamkin, A.: Runtime verification based on executable models: on-the-fly matching of timed traces. In: Petrenko, A., Schlingloff, H. (eds.) Eighth Workshop on Model-Based Testing (MBT), pp. 67–68 (2013)
Essayad, I., Zakari, A., Sadik, M., Nahhal, T.: Modelling and and analysis of heterogenous architectures and application to SystemC. In: FSKKP Anjur Persidangan ICSECS 2013 (2013)
Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware/software partitioning. In: The Third ACM and IEEE International Conference on Formal Methods and Models for Co-Design. pp. 101–110 (2005)
Niemann, B., Haubelt, Ch.: Formalizing TLM with communicating state machines. In: Forum of Specification and Design languages (2006)
Moinudeen, H., Habibi, A., Tahar, S.: Generating finite state machines from SystemC. In: Gielen, G.G.E. (ed.), DATE DesignerForum, pp. 76–81 (2006)
Védrine, F., Zhang, Y., Monsuez, B.: SystemC waiting-state automata. In: First International Workshop on Verification and Evaluation of Computer and Communication Systems, pp. 5–6 (2007)
Harrath, N., Monsuez, B.: Timed SystemC waiting-state automata. In: Third International Workshop on Verification and Evaluation of Computer and Communication Systems (2009)
Karlsson, P., Eles, D., Peng, Z.: Formal verification of SystemC designs using a petri-net based representation. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 1128–1233 (2006)
Ruys, T.C.: SPIN tutorial: how to become a SPIN doctor. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 6–13. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46017-9_3
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Soumia, E., Ismail, A., Mohammed, S. (2017). Verification of SystemC Components Using the Method of Deduction. In: Sabir, E., García Armada, A., Ghogho, M., Debbah, M. (eds) Ubiquitous Networking. UNet 2017. Lecture Notes in Computer Science(), vol 10542. Springer, Cham. https://doi.org/10.1007/978-3-319-68179-5_52
Download citation
DOI: https://doi.org/10.1007/978-3-319-68179-5_52
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68178-8
Online ISBN: 978-3-319-68179-5
eBook Packages: Computer ScienceComputer Science (R0)